[Agda] subst puzzle

[Nils Anders Danielsson]

On 2021-03-02 21:35, Jacques Carette wrote:
>    infix 1 _≈r_
>    record _≈r_ (T₁ T₂ : foo A) : Set where
>      field
>        ≡len : proj₁ T₂ ≡ proj₁ T₁   -- note the flip
>        ≡Rtd : (x : Fin (proj₁ T₂)) → proj₂ T₁ (subst Fin ≡len x) ≡ proj₂ T₂ x

I guess that you do not want to rely on function extensionality. In this
setting there is still a split surjection from foo A to List A, so I
would suggest the following approach:

* Replace _≈r_ with equality under conversion to lists:

     to-list : foo A → List A

     xs ≈r ys = to-list xs ≡ to-list ys

* Define _+++_ by recursion on the left list's length.

* Prove that to-list is homomorphic using the same recursion pattern:

     to-list (xs +++ ys) ≡ to-list xs ++ to-list ys

* Now it is easy to turn things like the right identity law for lists
   into corresponding laws for foo.

There is no need to use subst for this.

-- 
/NAD