[Agda] Associativity for free!

[Nils Anders Danielsson]

On 2011-10-26 16:48, Alan Jeffrey wrote:
> The idea of using difference lists to represent lists is standard, but
> as far as I know, this use of irrelevant equalities to get structural
> recursion is new. Anyone know of any prior art?

I've used the two tricks independently, but I haven't seen them used
together.

One of the tricks (old code, hence Set1, forall and -> rather than Set₁,
∀ and →):

   -- I am using difference lists to get associativity "for free". This
   -- makes it possible to state the right-assoc lemma below without
   -- using any casts.

   record TypeList : Set1 where
     infixr 5 _⟶_
     field
       _⟶_    : Set -> Set
       map    : forall {a b} -> (a -> b) -> _⟶_ a -> _⟶_ b
       map-id : forall a -> map (id {A = a}) ≡ id
       map-∘  : forall {a b c} (f : b -> c) (g : a -> b) ->
                map (f ∘ g) ≡ map f ∘ map g

The other:

   -- Families of functions which, on the semantic side, correspond to
   -- the application of a given context morphism

   record [_⟶_] {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂)
                {Γ Δ : Ctxt} (ρ̂ : Γ ⇨̂ Δ) : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
     constructor _,_

     open Term-like T₁ renaming (_⊢_ to _⊢₁_; ⟦_⟧ to ⟦_⟧₁)
     open Term-like T₂ renaming (_⊢_ to _⊢₂_; ⟦_⟧ to ⟦_⟧₂)

     field
       function     : ∀ σ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂
       .corresponds :
          ∀ σ (t : Γ ⊢₁ σ) → ⟦ t ⟧₁ /̂Val ρ̂ ≅-Value ⟦ function σ t ⟧₂

In this case the identity and associativity laws hold by definition
(because they hold automatically for function composition/identity).
However, in the end I decided not to use this approach, because I didn't
want to rely on yet another not-universally-accepted feature of Agda.

-- 
/NAD