-------------------------------------------------------------------------------- -- Copyright 2008 Chantal Keller -- School of Computer Science -- University of Nottingham -- This program is free software: you can redistribute it and/or modify -- it under the terms of the GNU General Public License as published by -- the Free Software Foundation, either version 3 of the License, or -- (at your option) any later version. -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -- GNU General Public License for more details. -- You should have received a copy of the GNU General Public License -- along with this program. If not, see . -------------------------------------------------------------------------------- module Lambda where open import Equality -- Simply-typed λ-calculus data Ty : Set where base : Ty _=>_ : Ty -> Ty -> Ty data Context : Set where empty : Context ext : Context -> Ty -> Context data Var : Context -> Ty -> Set where vlast : {Γ : Context} -> {τ : Ty} -> Var (ext Γ τ) τ weak : {σ : Ty} -> {Γ : Context} -> {τ : Ty} -> Var Γ τ -> Var (ext Γ σ) τ data Term : Context -> Ty -> Set where var : {Γ : Context} -> {σ : Ty} -> Var Γ σ -> Term Γ σ lam : {Γ : Context} -> {τ σ : Ty} -> Term (ext Γ τ) σ -> Term Γ (τ => σ) app : {Γ : Context} -> {τ σ : Ty} -> Term Γ (τ => σ) -> Term Γ τ -> Term Γ σ -- Substitution data Subst (T : Context -> Ty -> Set) : Context -> Context -> Set where substEmpty : {Γ : Context} -> Subst T Γ empty _,_ : {Γ Δ : Context} -> {σ : Ty} -> Subst T Γ Δ -> T Γ σ -> Subst T Γ (ext Δ σ) -- Kits for variables and terms record SubstKit (T : Context -> Ty -> Set) : Set where field vr : forall {Γ σ} -> Var Γ σ -> T Γ σ tm : forall {Γ σ} -> T Γ σ -> Term Γ σ wk : forall {Γ σ τ} -> T Γ σ -> T (ext Γ τ) σ record SubstKit+ (T : Context -> Ty -> Set) : Set where field kit : SubstKit T subst : forall {Γ Δ σ} -> T Δ σ -> Subst T Γ Δ -> T Γ σ -- Weakening a substitution _⁺_ : forall {σ T Γ Δ} -> Subst T Γ Δ -> SubstKit T -> Subst T (ext Γ σ) Δ substEmpty ⁺ _ = substEmpty (u , t) ⁺ k = (u ⁺ k) , ((SubstKit.wk k) t) -- Lifting a substitution _⁺⁺_ : forall {σ T Γ Δ} -> Subst T Γ Δ -> SubstKit T -> Subst T (ext Γ σ) (ext Δ σ) u ⁺⁺ k = (u ⁺ k) , ((SubstKit.vr k) vlast) -- Variable substitution substVar : forall {T Γ Δ σ} -> Subst T Γ Δ -> Var Δ σ -> T Γ σ substVar substEmpty () substVar (s , t) vlast = t substVar (s , t) (weak v) = substVar s v _[_] : forall {T Γ Δ σ} -> Var Δ σ -> Subst T Γ Δ -> T Γ σ v [ s ] = substVar s v -- Kits for variables vk : SubstKit Var vk = record { vr = (\a -> a) ; tm = var ; wk = weak } vk+ : SubstKit+ Var vk+ = record { kit = vk ; subst = _[_] } -- Term substitution substTerm : forall {T Γ Δ σ} -> SubstKit T -> Subst T Γ Δ -> Term Δ σ -> Term Γ σ substTerm k s (var v) = SubstKit.tm k (v [ s ]) substTerm k s (lam t) = lam (substTerm k (s ⁺⁺ k) t) substTerm k s (app t₁ t₂) = app (substTerm k s t₁) (substTerm k s t₂) -- The identity substitutions idSVar : {Γ : Context} -> Subst Var Γ Γ idSVar {empty} = substEmpty idSVar {ext Γ σ} = idSVar ⁺⁺ vk substTermOfSubstVar : forall {Γ Δ} -> Subst Var Γ Δ -> Subst Term Γ Δ substTermOfSubstVar substEmpty = substEmpty substTermOfSubstVar (s , v) = (substTermOfSubstVar s) , (var v) idSTerm : {Γ : Context} -> Subst Term Γ Γ idSTerm = substTermOfSubstVar idSVar -- Weakening a term termWeak : forall {τ Γ σ} -> Term Γ σ -> Term (ext Γ τ) σ termWeak t = substTerm vk (idSVar ⁺ vk) t -- Kits for terms tk : SubstKit Term tk = record { vr = var ; tm = (\a -> a) ; wk = termWeak } _[_]₁ : forall {Γ Δ σ} -> Term Δ σ -> Subst Var Γ Δ -> Term Γ σ t [ u ]₁ = substTerm vk u t _[_]₂ : forall {Γ Δ σ} -> Term Δ σ -> Subst Term Γ Δ -> Term Γ σ t [ u ]₂ = substTerm tk u t tk+ : SubstKit+ Term tk+ = record {kit = tk ; subst = _[_]₂ } -- Composition of substitutions compS : forall {T Γ Δ Θ} -> SubstKit+ T -> Subst T Γ Δ -> Subst T Δ Θ -> Subst T Γ Θ compS _ _ substEmpty = substEmpty compS k+ s (s' , t) = (compS k+ s s') , ((SubstKit+.subst k+) t s) _○₁_ : forall {Γ Δ Θ} -> Subst Var Γ Δ -> Subst Var Δ Θ -> Subst Var Γ Θ s ○₁ s' = compS vk+ s s' _○₂_ : forall {Γ Δ Θ} -> Subst Term Γ Δ -> Subst Term Δ Θ -> Subst Term Γ Θ s ○₂ s' = compS tk+ s s' _○₃_ : forall {Γ Δ Θ} -> Subst Var Γ Δ -> Subst Term Δ Θ -> Subst Term Γ Θ _ ○₃ substEmpty = substEmpty s ○₃ (s' , t) = (s ○₃ s') , (t [ s ]₁) _○₄_ : forall {Γ Δ Θ} -> Subst Term Γ Δ -> Subst Var Δ Θ -> Subst Term Γ Θ _ ○₄ substEmpty = substEmpty s ○₄ (s' , v) = (s ○₄ s') , (v [ s ]) -- Compatibility with constructors reflWeak : forall {Γ σ τ} -> {v₁ v₂ : Var Γ σ} -> v₁ ≡ v₂ -> weak {τ} v₁ ≡ weak v₂ reflWeak refl = refl reflVar : forall {Γ σ} -> {v₁ v₂ : Var Γ σ} -> v₁ ≡ v₂ -> var v₁ ≡ var v₂ reflVar refl = refl reflLam : forall {Γ σ τ} -> {t₁ t₂ : Term (ext Γ τ) σ} -> t₁ ≡ t₂ -> lam t₁ ≡ lam t₂ reflLam refl = refl reflApp : forall {Γ σ τ} -> {t₁ t₂ : Term Γ (σ => τ)} -> {u₁ u₂ : Term Γ σ} -> t₁ ≡ t₂ -> u₁ ≡ u₂ -> app t₁ u₁ ≡ app t₂ u₂ reflApp refl refl = refl reflSubstExt : forall {T Γ Δ σ} -> {s₁ s₂ : Subst T Γ Δ} -> {t₁ t₂ : T Γ σ} -> s₁ ≡ s₂ -> t₁ ≡ t₂ -> s₁ , t₁ ≡ s₂ , t₂ reflSubstExt refl refl = refl reflSubst : forall {Δ σ} -> {t₁ t₂ : Term Δ σ} -> forall {Γ} -> {s₁ s₂ : Subst Term Γ Δ} -> s₁ ≡ s₂ -> t₁ ≡ t₂ -> t₁ [ s₁ ]₂ ≡ t₂ [ s₂ ]₂ reflSubst refl refl = refl reflSubst2 : forall {Δ σ} -> {t₁ t₂ : Var Δ σ} -> forall {T Γ} -> {s₁ s₂ : Subst T Γ Δ} -> s₁ ≡ s₂ -> t₁ ≡ t₂ -> t₁ [ s₁ ] ≡ t₂ [ s₂ ] reflSubst2 refl refl = refl reflSubst3 : forall {Δ σ} -> {t₁ t₂ : Term Δ σ} -> forall {Γ} -> {s₁ s₂ : Subst Var Γ Δ} -> s₁ ≡ s₂ -> t₁ ≡ t₂ -> t₁ [ s₁ ]₁ ≡ t₂ [ s₂ ]₁ reflSubst3 refl refl = refl -- Proof that the variable substitutions form a category -- Applying a weakened substitution is weakening the result of the substitution eqWeak : forall {Γ Δ σ τ} -> (s : Subst Var Γ Δ) -> (v : Var Δ σ) -> v [ _⁺_ {τ} s vk ] ≡ weak (v [ s ]) eqWeak substEmpty () eqWeak (s , v₁) vlast = refl eqWeak (s , v₁) (weak v₂) = eqWeak s v₂ mutual -- The weakened identity weakens variables eqId : forall {Γ σ τ} -> (v : Var Γ σ) -> v [ _⁺_ {τ} idSVar vk ] ≡ weak v eqId v = trans (eqWeak idSVar v) (reflWeak (nLVar v)) -- The identity does not change variables nLVar : forall {Γ σ} -> (v : Var Γ σ) -> v [ idSVar ] ≡ v nLVar vlast = refl nLVar (weak v) = eqId v -- Identity is neutral on the left neutralLVar : forall {Γ Δ} -> (s : Subst Var Γ Δ) -> idSVar ○₁ s ≡ s neutralLVar substEmpty = refl neutralLVar (s , v) = reflSubstExt (neutralLVar s) (nLVar v) -- The composition of an extended substitution and a weakened substitution is the composition of the two initial compositions nRVar : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (s' : Subst Var Δ Θ) -> (v : Var Γ σ) -> (s , v) ○₁ (s' ⁺ vk) ≡ s ○₁ s' nRVar _ substEmpty _ = refl nRVar s (s' , _) v = reflSubstExt (nRVar s s' v) refl -- Identity is neutral on the right neutralRVar : forall {Γ Δ} -> (s : Subst Var Γ Δ) -> s ○₁ idSVar ≡ s neutralRVar substEmpty = refl neutralRVar (s , v) = reflSubstExt (trans (nRVar s idSVar v) (neutralRVar s)) refl -- Applying a composition is applying the first substitution then the second substitution aCSVar : forall {Γ Δ Θ σ} -> (u : Subst Var Γ Δ) -> (v : Subst Var Δ Θ) -> (v' : Var Θ σ) -> v' [ u ○₁ v ] ≡ (v' [ v ]) [ u ] aCSVar _ substEmpty () aCSVar _ (_ , _) vlast = refl aCSVar u (v , _) (weak v') = aCSVar u v v' -- The substitution composition is associative assoCompSVar : forall {Γ Δ Θ Ξ} -> (u : Subst Var Γ Δ) -> (v : Subst Var Δ Θ) -> (w : Subst Var Θ Ξ) -> (u ○₁ v) ○₁ w ≡ u ○₁ (v ○₁ w) assoCompSVar _ _ substEmpty = refl assoCompSVar u v (w , t) = reflSubstExt (assoCompSVar u v w) (aCSVar u v t) -- Proof that this category has finite products -- First projector π₁ : forall {Γ Δ σ} -> Subst Var Γ (ext Δ σ) -> Subst Var Γ Δ π₁ s = s ○₁ (idSVar ⁺ vk) p₁ : forall {Γ Δ σ} -> (s : Subst Var Γ Δ) -> (v : Var Γ σ) -> π₁ (s , v) ≡ s p₁ s v = trans (nRVar s idSVar v) (neutralRVar s) -- Second projector π₂ : forall {Γ Δ σ} -> Subst Var Γ (ext Δ σ) -> Var Γ σ π₂ s = vlast [ s ] p₂ : forall {Γ Δ σ} -> (s : Subst Var Γ Δ) -> (v : Var Γ σ) -> π₂ (s , v) ≡ v p₂ _ _ = refl -- Surjective pairing sp : forall {Γ Δ σ} -> (s : Subst Var Γ (ext Δ σ)) -> (π₁ s) , (π₂ s) ≡ s sp (s , v) = reflSubstExt (p₁ s v) (p₂ s v) -- Proof that the term substitutions form a category -- Weakening a substitution is commutative substWeakExchange : forall {Γ Δ σ} -> (s : Subst Var Γ Δ) -> _⁺_ {σ} (substTermOfSubstVar s) tk ≡ substTermOfSubstVar (s ⁺ vk) substWeakExchange substEmpty = refl substWeakExchange (s , v) = reflSubstExt (substWeakExchange s) (reflVar (eqId v)) -- Applying a lifted substitution is applying the substitution substTermAndVar : forall {Γ Δ σ} -> (s : Subst Var Γ Δ) -> (t : Term Δ σ) -> t [ substTermOfSubstVar s ]₂ ≡ t [ s ]₁ substTermAndVar substEmpty (var ()) substTermAndVar (_ , _) (var vlast) = refl substTermAndVar (s , _) (var (weak v')) = substTermAndVar s (var v') substTermAndVar s (lam t) = reflLam (trans (reflSubst {_} {_} {t} {t} (reflSubstExt (substWeakExchange s) refl) refl) (substTermAndVar (s ⁺⁺ vk) t)) substTermAndVar s (app t₁ t₂) = reflApp (substTermAndVar s t₁) (substTermAndVar s t₂) -- The identity does not change terms nLTerm2 : forall {Γ σ} -> (t : Term Γ σ) -> t [ idSVar ]₁ ≡ t nLTerm2 (var v) = reflVar (nLVar v) nLTerm2 (lam t) = reflLam (nLTerm2 t) nLTerm2 (app t₁ t₂) = reflApp (nLTerm2 t₁) (nLTerm2 t₂) nLTerm : forall {Γ σ} -> (t : Term Γ σ) -> t [ idSTerm ]₂ ≡ t nLTerm t = trans (substTermAndVar idSVar t) (nLTerm2 t) -- Identity is neutral on the left neutralLTerm : forall {Γ Δ} -> (u : Subst Term Γ Δ) -> idSTerm ○₂ u ≡ u neutralLTerm substEmpty = refl neutralLTerm (u , t) = reflSubstExt (neutralLTerm u) (nLTerm t) -- The composition of an extended substitution and a weakened substitution is the composition of the two initial compositions nRTerm : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (s : Subst Var Δ Θ) -> (t : Term Γ σ) -> (u , t) ○₂ (substTermOfSubstVar (s ⁺ vk)) ≡ u ○₂ (substTermOfSubstVar s) nRTerm _ substEmpty _ = refl nRTerm u (s , _) t = reflSubstExt (nRTerm u s t) refl -- Identity is neutral on the right neutralRTerm : forall {Γ Δ} -> (u : Subst Term Γ Δ) -> u ○₂ idSTerm ≡ u neutralRTerm substEmpty = refl neutralRTerm (u , t) = reflSubstExt (trans (nRTerm u idSVar t) (neutralRTerm u)) refl -- Composing with the weakened identity is like weakening aux2 : forall {Γ Δ Θ σ τ} -> (s : Subst Var Γ Δ) -> (s' : Subst Var Δ Θ) -> (v : Var Γ σ) -> (_⁺⁺_ {τ} s vk) ○₁ (s' ⁺ vk) ≡ (((s ⁺ vk) , (weak v)) , vlast) ○₁ ((s' ⁺ vk) ⁺ vk) aux2 _ substEmpty _ = refl aux2 s (s' , _) v = reflSubstExt (aux2 s s' v) refl aux : forall {Γ Δ Θ σ τ} -> (u : Subst Term Γ Δ) -> (s : Subst Var Δ Θ) -> (t : Term Γ σ) -> (_⁺⁺_ {τ} u tk) ○₄ (s ⁺ vk) ≡ (((u ⁺ tk) , (termWeak t)) , (var vlast)) ○₄ ((s ⁺ vk) ⁺ vk) aux _ substEmpty _ = refl aux u (s , _) t = reflSubstExt (aux u s t) refl weakOn1 : forall {Γ Δ σ} -> (s : Subst Var Γ Δ) -> (_⁺_ {σ} idSVar vk) ○₁ s ≡ s ⁺ vk weakOn1 substEmpty = refl weakOn1 (s , v) = reflSubstExt (weakOn1 s) (eqId v) weakOn2 : forall {Δ Γ σ} -> (s : Subst Var Γ Δ) -> _⁺_ {σ} s vk ≡ (s ⁺⁺ vk) ○₁ (idSVar ⁺ vk) weakOn2 substEmpty = refl weakOn2 (s , v) = reflSubstExt (trans (weakOn2 s) (aux2 s idSVar v)) refl weakOn : forall {Γ Δ σ} -> (s : Subst Var Γ Δ) -> (_⁺_ {σ} idSVar vk) ○₁ s ≡ (s ⁺⁺ vk) ○₁ (idSVar ⁺ vk) weakOn s = trans (weakOn1 s) (weakOn2 s) weakIn1 : forall {Γ Δ σ} -> (u : Subst Term Γ Δ) -> (_⁺_ {σ} idSVar vk) ○₃ u ≡ u ⁺ tk weakIn1 substEmpty = refl weakIn1 (u , _) = reflSubstExt (weakIn1 u) refl weakIn2 : forall {Γ Δ σ} -> (u : Subst Term Γ Δ) -> _⁺_ {σ} u tk ≡ (u ⁺⁺ tk) ○₄ (idSVar ⁺ vk) weakIn2 substEmpty = refl weakIn2 (u , t) = reflSubstExt (trans (weakIn2 u) (aux u idSVar t)) refl weakIn : forall {Γ Δ σ} -> (u : Subst Term Γ Δ) -> (_⁺_ {σ} idSVar vk) ○₃ u ≡ (u ⁺⁺ tk) ○₄ (idSVar ⁺ vk) weakIn u = trans (weakIn1 u) (weakIn2 u) -- Weakening the composition of substitutions is composing the weakened substitutions compWeakAux3 : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (s' : Subst Var Δ Θ) -> _⁺_ {σ} (s ○₁ s') vk ≡ (s ⁺⁺ vk) ○₁ (s' ⁺ vk) compWeakAux3 _ substEmpty = refl compWeakAux3 s (s' , v) = reflSubstExt (compWeakAux3 s s') (sym (eqWeak s v)) compWeak3 : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (s' : Subst Var Δ Θ) -> _⁺⁺_ {σ} (s ○₁ s') vk ≡ (s ⁺⁺ vk) ○₁ (s' ⁺⁺ vk) compWeak3 s s' = reflSubstExt (compWeakAux3 s s') refl -- Applying a composition is applying the first substitution then the second substitution aCSTerm3 : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (u : Subst Term Δ Θ) -> (v : Var Θ σ) -> (v [ u ]) [ s ]₁ ≡ v [ s ○₃ u ] aCSTerm3 _ substEmpty () aCSTerm3 _ (_ , _) vlast = refl aCSTerm3 s (u , _) (weak v) = aCSTerm3 s u v aCSTerm4 : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (s' : Subst Var Δ Θ) -> (t : Term Θ σ) -> (t [ s' ]₁) [ s ]₁ ≡ t [ s ○₁ s' ]₁ aCSTerm4 _ substEmpty (var ()) aCSTerm4 _ (_ , _) (var vlast) = refl aCSTerm4 s (s' , _) (var (weak v)) = aCSTerm4 s s' (var v) aCSTerm4 s s' (lam t) = reflLam (trans (aCSTerm4 (s ⁺⁺ vk) (s' ⁺⁺ vk) t) (reflSubst3 {_} {_} {t} {t} (sym (compWeak3 s s')) refl)) aCSTerm4 s s' (app t₁ t₂) = reflApp (aCSTerm4 s s' t₁) (aCSTerm4 s s' t₂) -- Weakening a substitued term is substituting the weakened substitution to the weakened term eqWeakTerm1 : forall {Γ Δ σ τ} -> (s : Subst Var Γ Δ) -> (t : Term Δ σ) -> termWeak {τ} (t [ s ]₁) ≡ (termWeak t) [ s ⁺⁺ vk ]₁ eqWeakTerm1 s t = trans (aCSTerm4 (idSVar ⁺ vk) s t) (trans (reflSubst3 {_} {_} {t} {t} (weakOn s) refl) (sym (aCSTerm4 (s ⁺⁺ vk) (idSVar ⁺ vk) t))) -- Weakening the composition of substitutions is composing the weakened substitutions compWeakAux2 : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (s : Subst Var Δ Θ) -> _⁺_ {σ} (u ○₄ s) tk ≡ (u ⁺⁺ tk) ○₄ (s ⁺ vk) compWeakAux2 _ substEmpty = refl compWeakAux2 u (s , v) = reflSubstExt (compWeakAux2 u s) (trans (aCSTerm3 (idSVar ⁺ vk) u v) (reflSubst2 {_} {_} {v} {v} (weakIn1 u) refl)) compWeak2 : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (s : Subst Var Δ Θ) -> _⁺⁺_ {σ} (u ○₄ s) tk ≡ (u ⁺⁺ tk) ○₄ (s ⁺⁺ vk) compWeak2 u s = reflSubstExt (compWeakAux2 u s) refl compWeakAux1 : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (u : Subst Term Δ Θ) -> _⁺_ {σ} (s ○₃ u) tk ≡ (s ⁺⁺ vk) ○₃ (u ⁺ tk) compWeakAux1 _ substEmpty = refl compWeakAux1 s (u , t) = reflSubstExt (compWeakAux1 s u) (eqWeakTerm1 s t) compWeak1 : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (u : Subst Term Δ Θ) -> _⁺⁺_ {σ} (s ○₃ u) tk ≡ (s ⁺⁺ vk) ○₃ (u ⁺⁺ tk) compWeak1 s u = reflSubstExt (compWeakAux1 s u) refl -- Applying a composition is applying the first substitution then the second substitution aCSTerm1 : forall {Γ Δ Θ σ} -> (s : Subst Var Γ Δ) -> (u : Subst Term Δ Θ) -> (t : Term Θ σ) -> (t [ u ]₂) [ s ]₁ ≡ t [ s ○₃ u ]₂ aCSTerm1 _ substEmpty (var ()) aCSTerm1 _ (_ , _) (var vlast) = refl aCSTerm1 s (u , _) (var (weak v)) = aCSTerm1 s u (var v) aCSTerm1 s u (lam t) = reflLam (trans (aCSTerm1 (s ⁺⁺ vk) (u ⁺⁺ tk) t) (reflSubst {_} {_} {t} {t} (sym (compWeak1 s u)) refl)) aCSTerm1 s u (app t₁ t₂) = reflApp (aCSTerm1 s u t₁) (aCSTerm1 s u t₂) aCSTerm2 : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (s : Subst Var Δ Θ) -> (t : Term Θ σ) -> t [ u ○₄ s ]₂ ≡ (t [ s ]₁) [ u ]₂ aCSTerm2 _ substEmpty (var ()) aCSTerm2 _ (_ , _) (var vlast) = refl aCSTerm2 u (s , _) (var (weak v)) = aCSTerm2 u s (var v) aCSTerm2 u s (lam t) = reflLam (trans (reflSubst {_} {_} {t} {t} (compWeak2 u s) refl) (aCSTerm2 (u ⁺⁺ tk) (s ⁺⁺ vk) t)) aCSTerm2 u s (app t₁ t₂) = reflApp (aCSTerm2 u s t₁) (aCSTerm2 u s t₂) -- Weakening a substitued term is substituting the weakened substitution to the weakened term eqWeakTerm : forall {Γ Δ σ τ} -> (u : Subst Term Γ Δ) -> (t : Term Δ σ) -> termWeak {τ} (t [ u ]₂) ≡ (termWeak t) [ u ⁺⁺ tk ]₂ eqWeakTerm u t = trans (aCSTerm1 (idSVar ⁺ vk) u t) (trans (reflSubst {_} {_} {t} {t} (weakIn u) refl) (aCSTerm2 (u ⁺⁺ tk) (idSVar ⁺ vk) t)) -- Weakening the composition of substitutions is composing the weakened substitutions compWeakAux : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (v : Subst Term Δ Θ) -> _⁺_ {σ} (u ○₂ v) tk ≡ (u ⁺⁺ tk) ○₂ (v ⁺ tk) compWeakAux u substEmpty = refl compWeakAux u (v , t) = reflSubstExt (compWeakAux u v) (eqWeakTerm u t) compWeak : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (v : Subst Term Δ Θ) -> _⁺⁺_ {σ} (u ○₂ v) tk ≡ (u ⁺⁺ tk) ○₂ (v ⁺⁺ tk) compWeak u v = reflSubstExt (compWeakAux u v) refl -- Applying a composition is applying the first substitution then the second substitution aCSTerm : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (v : Subst Term Δ Θ) -> (t : Term Θ σ) -> t [ u ○₂ v ]₂ ≡ (t [ v ]₂) [ u ]₂ aCSTerm u substEmpty (var ()) aCSTerm u (s , t) (var vlast) = refl aCSTerm u (s , t) (var (weak v)) = aCSTerm u s (var v) aCSTerm u s (lam t) = reflLam (trans (reflSubst {_} {_} {t} {t} (compWeak u s) refl) (aCSTerm (u ⁺⁺ tk) (s ⁺⁺ tk) t)) aCSTerm u s (app t₁ t₂) = reflApp (aCSTerm u s t₁) (aCSTerm u s t₂) -- The substitution composition is associative assoCompSTerm : forall {Γ Δ Θ Ξ} -> (u : Subst Term Γ Δ) -> (v : Subst Term Δ Θ) -> (w : Subst Term Θ Ξ) -> (u ○₂ v) ○₂ w ≡ u ○₂ (v ○₂ w) assoCompSTerm u v substEmpty = refl assoCompSTerm u v (w , t) = reflSubstExt (assoCompSTerm u v w) (aCSTerm u v t) -- Proof that this category has finite products mutual -- The identity substitution is neutral on the right neutralRTermVar : forall {Γ Δ} -> (u : Subst Term Γ Δ) -> u ○₄ idSVar ≡ u neutralRTermVar substEmpty = refl neutralRTermVar (u , t) = reflSubstExt (extWeakId u t) refl -- Composing an extended substitution with the weakened identity is the initial substitution extWeak : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (s : Subst Var Δ Θ) -> (t : Term Γ σ) -> (u , t) ○₄ (s ⁺ vk) ≡ u ○₄ s extWeak _ substEmpty _ = refl extWeak u (s , _) t = reflSubstExt (extWeak u s t) refl extWeakId : forall {Γ Δ σ} -> (u : Subst Term Γ Δ) -> (t : Term Γ σ) -> (u , t) ○₄ (idSVar ⁺ vk) ≡ u extWeakId u t = trans (extWeak u idSVar t) (neutralRTermVar u) -- First projector π'₁ : forall {Γ Δ σ} -> Subst Term Γ (ext Δ σ) -> Subst Term Γ Δ π'₁ u = u ○₂ (idSTerm ⁺ tk) weakExtTerm : forall {Γ Δ Θ σ} -> (u : Subst Term Γ Δ) -> (v : Subst Term Δ Θ) -> (t : Term Γ σ) -> (u , t) ○₂ (v ⁺ tk) ≡ u ○₂ v weakExtTerm _ substEmpty _ = refl weakExtTerm u (v , t') t = reflSubstExt (weakExtTerm u v t) (trans (sym (aCSTerm2 (u , t) (idSVar ⁺ vk) t')) (reflSubst {_} {_} {t'} {t'} (extWeakId u t) refl)) p'₁ : forall {Γ Δ σ} -> (u : Subst Term Γ Δ) -> (t : Term Γ σ) -> π'₁ (u , t) ≡ u p'₁ u t = trans (weakExtTerm u idSTerm t) (neutralRTerm u) -- Second projector π'₂ : forall {Γ Δ σ} -> Subst Term Γ (ext Δ σ) -> Term Γ σ π'₂ s = (var vlast) [ s ]₂ p'₂ : forall {Γ Δ σ} -> (u : Subst Term Γ Δ) -> (t : Term Γ σ) -> π'₂ (u , t) ≡ t p'₂ _ _ = refl -- Surjective pairing sp' : forall {Γ Δ σ} -> (u : Subst Term Γ (ext Δ σ)) -> (π'₁ u) , (π'₂ u) ≡ u sp' (u , t) = reflSubstExt (p'₁ u t) (p'₂ u t)