[Agda] Re: Associativity for free!

[Andrea Vezzosi]

On Fri, Nov 4, 2011 at 12:29 PM, James Chapman <james at cs.ioc.ee> wrote:
> [...] The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.

And yet, even without fancy representations, it can be trimmed down to
109 lines and many less intermediate constructions by working under a
context:

module WellTypedTerms where

-- Utilities
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
 refl : {a : A} → a ≅ a

trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
trans refl p = p

sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
sym refl = refl

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B x) → C x y)
          {a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b ≅ f a' b'
resp2 f refl refl = refl

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
     (∀ {a} b → C a b) → (g : (∀ (a : A) → B a)) → ∀ (a : A) → C a (g a)
f • g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

--Well type lambda terms

data Ty : Set where
 ι   : Ty
 _⇒_ : Ty → Ty → Ty

data Con : Set where
 ε   : Con
 _<_ : Con → Ty → Con


_<<_ : Con -> Con -> Con
Γ << ε = Γ
Γ << (Δ < τ) = (Γ << Δ) < τ

data Var : Con → Ty → Set where
 vz : ∀{Γ σ} → Var (Γ < σ) σ
 vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
 var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
 app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
 lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

-- Substitutions

Sub : Con → Con → Set
Sub Γ Δ = ∀ K {σ} → Var (Γ << K) σ → Tm (Δ << K) σ

sub : ∀{Γ Δ} → Sub Γ Δ → ∀ K {σ} → Tm (Γ << K) σ → Tm (Δ << K) σ
sub f K (var x)   = f K x
sub f K (app t u) = app (sub f K t) (sub f K u)
sub f K (lam t)   = lam (sub f (K < _) t)

subId : ∀{Γ} → Sub Γ Γ
subId = λ K x -> var x

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g K = sub f K • g K

-- first monad law, the second holds definitionally
subid : ∀{Γ}K{σ}(t : Tm (Γ << K) σ) → sub subId K t ≅ id t
subid K (var x)   = refl
subid K (app t u) = resp2 app (subid K t) (subid K u)
subid K (lam t)   = resp lam (subid (K < _) t)

-- Renaming

Ren : Con → Con → Set
Ren Γ Δ = ∀ K {σ} → Var (Γ << K) σ → Var (Δ << K) σ

renId : ∀{Γ} → Ren Γ Γ
renId = \ _ x -> x

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = \ K -> f K • g K

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ K {σ} → Tm (Γ << K) σ → Tm (Δ << K) σ
ren f K x = sub (λ K → subId K • f K) K x

renid : ∀{Γ} K {σ}(t : Tm (Γ << K) σ) → ren renId K t ≅ id t
renid = subid

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ) K {σ}(t : Tm (B << K) σ) →
           ren (renComp f g) K t ≅ (ren f K • ren g K) t
rencomp f g K (var x)   = refl
rencomp f g K (app t u) = resp2 app (rencomp f g K t) (rencomp f g K u)
rencomp {B}{Γ}{Δ} f g K (lam t) = resp lam (rencomp f g (K < _) t)

-- third monad law
subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ)K{σ}(t : Tm (B << K) σ) →
         sub (subComp f g) K t ≅ (sub f K • sub g K) t
subcomp f g K (var x)   = refl
subcomp f g K (app t u) = resp2 app (subcomp f g K t) (subcomp f g K u)
subcomp f g K (lam t)   = resp lam (subcomp f g (K < _) t)

-- these are now corollaries
rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ)K{σ}(t : Tm (B << K) σ) →
        (ren f K • sub g K) t ≅ sub (λ K -> ren f K • g K) K t
rensub f g K t = sym (subcomp (λ K → subId K • f K) g K t)

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ)K{σ}(t : Tm (B << K) σ) →
        (sub f K • ren g K) t ≅ sub (λ K -> f K • g K) K t
subren f g K x = sym (subcomp f (λ K' → subId K' • g K') K x)