[Agda] subst puzzle

[Jacques Carette]

On 2021-Mar.-02 07:15 , Nils Anders Danielsson wrote:
> On 2021-03-01 21:54, Jacques Carette wrote:
>> Here is a self-contained puzzle that has me stumped.
>
> Why do you want to prove this?
>
An excellent question indeed.  Here's a small, self-contained version.

The rhs of`foo` is really from `Data.Vec.Functional`.  The real goal is 
to prove the IsMonoid at the end. I have now done it, replacing the 
`subst Fin` below with `cast` from Data.Fin (thanks @gallais!), with 
less pain.  I was stuck on the right-identity law.

The motivation is a generalization of the "Big Operators" of 
https://hal.inria.fr/inria-00331193.

Because `foo A` is definitely dependent, I know of no ways to avoid 
doing some kind of patching of the rhs type when defining equivalence.

Jacques

open import Data.Nat using (ℕ; _+_; zero)
open import Data.Fin using (Fin; splitAt)
open import Relation.Binary.PropositionalEquality using (_≡_; subst)
open import Data.Sum using (inj₁; [_,_])
open import Data.Product
open import Algebra using (IsMonoid)

foo : Set₀ → Set₀
foo A = Σ ℕ (λ n → Fin n → A)

module _ {A : Set₀} where
   infix 5 _+++_
   _+++_ : foo A → foo A → foo A
   t₁ +++ t₂ = (proj₁ t₁ + proj₁ t₂) ,  λ n → [ proj₂ t₁ , proj₂ t₂ ] 
(splitAt (proj₁ t₁) n)

   0foo : foo A
   0foo = 0 , λ ()

   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

   goal : IsMonoid _≈r_ _+++_ 0foo
   goal = {!!}