[Agda] subst puzzle

[Jacques Carette]

On 2021-Mar.-03 10:30 , Nils Anders Danielsson wrote:
> 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: [...]

Oh, that is perfect, thank you! That will indeed simplify many things, 
even more than the current `cast` approach.

It would be really nice to collect the "wisdom of the masters" for doing 
dependently-typed programming somewhere. So I'll volunteer: if people 
want to send me nuggets (links to blogs, to pieces of code and a comment 
why the technique should be known, etc), I'll find a way to put them up 
somewhere. The Agda wiki?

Jacques