remove two more more outdated syntax files

formalizations/guarded-cubical/Syntax/Logic.agda

-{-# OPTIONS --cubical #-}
- -- to allow opening this module in other files while there are still holes
-{-# OPTIONS --allow-unsolved-metas #-}
-module Syntax.Logic  where
-
-open import Cubical.Foundations.Prelude renaming (comp to compose)
-open import Cubical.Data.Nat hiding (_·_)
-open import Cubical.Data.Sum
-open import Cubical.Relation.Nullary
-open import Cubical.Foundations.Function
-open import Cubical.Data.Prod hiding (map)
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Data.List hiding (nil)
-open import Cubical.Data.Empty renaming (rec to exFalso)
-
-open import Syntax.Types
-open import Syntax.Terms
-
-private
- variable
-   Δ Γ Θ Z Δ' Γ' Θ' Z' : Ctx
-   R S T U R' S' T' U' : Ty
-   B B' C C' D D' : Γ ⊑ctx Γ'
-   b b' c c' d d' : S ⊑ S'
-   γ γ' γ'' : Subst Δ Γ
-   δ δ' δ'' : Subst Θ Δ
-   V V' V'' : Val Γ S
-   M M' M'' N N' N'' : Comp Γ S
-   E E' E'' F F' F'' : EvCtx Γ S T
-
-open TyPrec
-open CtxPrec
-
-data Subst⊑ : (C : Δ ⊑ctx Δ') (D : Γ ⊑ctx Γ') (γ : Subst Δ Γ) (γ' : Subst Δ' Γ') → Type
-data Val⊑ : (C : Γ ⊑ctx Γ') (c : S ⊑ S') (V : Val Γ S) (V' : Val Γ' S') → Type
-data EvCtx⊑ : (C : Γ ⊑ctx Γ') (c : S ⊑ S') (d : T ⊑ T') (E : EvCtx Γ S T) (E' : EvCtx Γ' S' T') → Type
-data Comp⊑ : (C : Γ ⊑ctx Γ') (c : S ⊑ S') (M : Comp Γ S) (M' : Comp Γ' S') → Type
-
--- Three parts:
--- 1. Internalization to Preorders
---    - everything is monotone (including the actions of substitution/plugging)
---    - transitivity (reflexivity is admissible)
---    - propositionally truncate
--- 2. Errors are bottom
--- 3. Casts are LUBs/GLBs and retractions
-data Subst⊑ where
-  !s : Subst⊑ C [] !s !s
-  _,s_ : Subst⊑ C D γ γ' → Val⊑ C c V V' → Subst⊑ C (c ∷ D) (γ ,s V) (γ' ,s V')
-  _∘s_ : Subst⊑ C D γ γ' → Subst⊑ B C δ δ' → Subst⊑ B D (γ ∘s δ) (γ' ∘s δ')
-  _ids_ : Subst⊑ C C ids ids
-  -- in principle we could add βη equations instead but truncating is simpler
-  isProp⊑ : isProp (Subst⊑ C D γ γ')
-
-data Val⊑ where
-  _[_]v : Val⊑ C c V V' → Subst⊑ B C γ γ' → Val⊑ B c (V [ γ ]v) (V' [ γ' ]v)
-  var : Val⊑ (c ∷ C) c var var
-  zro : Val⊑ [] nat zro zro
-  suc : Val⊑ (nat ∷ []) nat suc suc
-
-  up-L : ∀ S⊑T → Val⊑ ((ty-prec S⊑T) ∷ []) (refl-⊑ (ty-right S⊑T)) (up S⊑T) var
-  up-R : ∀ S⊑T → Val⊑ ((refl-⊑ (ty-left S⊑T)) ∷ []) (ty-prec S⊑T) var (up S⊑T)
-
-  trans : Val⊑ C c V V' → Val⊑ D d V' V'' → Val⊑ (trans-⊑ctx C D) (trans-⊑ c d) V V''
-  isProp⊑ : isProp (Val⊑ C c V V')
-
-data EvCtx⊑ where
-  ∙E : EvCtx⊑ C c c ∙E ∙E
-  _∘E_ : EvCtx⊑ C c d E E' → EvCtx⊑ C b c F F' → EvCtx⊑ C b d (E ∘E F) (E' ∘E F')
-  _[_]e : EvCtx⊑ C c d E E' → Subst⊑ B C γ γ' → EvCtx⊑  B c d (E [ γ ]e) (E' [ γ' ]e)
-  -- bind : Comp⊑ (c ∷ C) d M M' → EvCtx⊑ C c d ? ?
-
-  dn-L : ∀ S⊑T → EvCtx⊑ [] (refl-⊑ (ty-right S⊑T)) (ty-prec S⊑T) (dn S⊑T) ∙E
-  dn-R : ∀ S⊑T → EvCtx⊑ [] (ty-prec S⊑T) (refl-⊑ (ty-left S⊑T)) ∙E (dn S⊑T)
-  retractionR : ∀ S⊑T → EvCtx⊑ [] (refl-⊑ (ty-right S⊑T)) (refl-⊑ (ty-right S⊑T)) ∙E (upE S⊑T ∘E dn S⊑T)
-
-  trans : EvCtx⊑ C b c E E' → EvCtx⊑ C' b' c' E' E'' → EvCtx⊑ (trans-⊑ctx C C') (trans-⊑ b b') (trans-⊑ c c') E E''
-  isProp⊑ : isProp (EvCtx⊑ C c d E E')
-
-data Comp⊑ where
-  _[_]∙ : EvCtx⊑ C c d E E' → Comp⊑ C c M M' → Comp⊑ C d (E [ M ]∙) (E' [ M' ]∙)
-  _[_]c : Comp⊑ C c M M' → Subst⊑ D C γ γ' → Comp⊑ D c (M [ γ ]c) (M' [ γ' ]c)
-  ret : Comp⊑ (c ∷ []) c ret ret
-  app : Comp⊑ (c ∷ c ⇀ d ∷ []) d app app
-  matchNat : ∀ {Kz Kz' Ks Ks'} → Comp⊑ C c Kz Kz' → Comp⊑ (nat ∷ C) c Ks Ks' → Comp⊑ (nat ∷ C) c (matchNat Kz Ks) (matchNat Kz' Ks')
-
-  err⊥ : Comp⊑ (refl-⊑ctx Γ) (refl-⊑ S) err' M
-
-  trans : Comp⊑ C c M M' → Comp⊑ D d M' M'' → Comp⊑ (trans-⊑ctx C D) (trans-⊑ c d) M M''
-  isProp⊑ : isProp (Comp⊑ C c M M')
-
-Subst⊑-homo : (γ γ' : Subst Δ Γ) → Type _
-Subst⊑-homo = Subst⊑ (refl-⊑ctx _) (refl-⊑ctx _)
-
-Val⊑-homo : (V V' : Val Γ S) → Type _
-Val⊑-homo = Val⊑ (refl-⊑ctx _) (refl-⊑ _)
-
-Comp⊑-homo : (M M' : Comp Γ S) → Type _
-Comp⊑-homo = Comp⊑ (refl-⊑ctx _) (refl-⊑ _)
-
-EvCtx⊑-homo : (E E' : EvCtx Γ S T) → Type _
-EvCtx⊑-homo = EvCtx⊑ (refl-⊑ctx _) (refl-⊑ _) (refl-⊑ _)
-
-_≈s_ : ∀ (γ γ' : Subst Δ Γ) → Type
-γ ≈s γ' = Subst⊑-homo γ γ' × Subst⊑-homo γ' γ
-
-_≈v_ : (V V' : Val Γ S) → Type _
-V ≈v V' = Val⊑-homo V V' × Val⊑-homo V' V
-
-_≈m_ : (M M' : Comp Γ S) → Type _
-M ≈m M' = Comp⊑-homo M M' × Comp⊑-homo M' M
-
-_≈e_ : (E E' : EvCtx Γ S T) → Type _
-E ≈e E' = EvCtx⊑-homo E E' × EvCtx⊑-homo E' E
-
-up-monotone : (S⊑S' : S ⊑ S')(S⊑T : S ⊑ T)(S'⊑T' : S' ⊑ T') (T⊑T' : T ⊑ T')
-            → Val⊑ (S⊑T ∷ []) S'⊑T' (up (mkTyPrec S⊑S')) (up (mkTyPrec T⊑T'))
-up-monotone {S}{S'}{T}{T'} S⊑S' S⊑T S'⊑T' T⊑T' =
-  transport (λ i → Val⊑ (split-dom (~ i) ∷ []) (split-cod (~ i)) (substId {V = up (mkTyPrec S⊑S')} i) (varβ {δ = !s}{V = (up (mkTyPrec T⊑T'))} i))
-  (trans (up-L (mkTyPrec (S⊑S'))) (var {C = []})
-  [ transport (λ i → Subst⊑ (trans-⊑ S⊑T (refl-⊑ T) ∷ []) (swap-middle i) (ids1-expand (~ i)) (!s ,s up (mkTyPrec T⊑T')))
-    (!s ,s trans ((var {C = []})) (up-R (mkTyPrec T⊑T'))) ]v)
-  where
-    split-cod : S'⊑T' ≡ trans-⊑ (refl-⊑ _) S'⊑T'
-    split-cod = isPropTy⊑ _ _
-
-    split-dom : S⊑T ≡ trans-⊑ S⊑T (refl-⊑ _)
-    split-dom = isPropTy⊑ _ _
-
-    swap-middle : Path ((S ∷ []) ⊑ctx (T' ∷ [])) (trans-⊑ S⊑T T⊑T' ∷ []) (trans-⊑ S⊑S' S'⊑T' ∷ [])
-    swap-middle i = (isPropTy⊑ (trans-⊑ S⊑T T⊑T') (trans-⊑ S⊑S' S'⊑T') i) ∷ []
-
--- TODO: show down is monotone
--- EXERCISE
-⇀-up-uniqueness : ∀ S⊑S' T⊑T' →
-  up (S⊑S' ⇀TP T⊑T')
-  ≈v lda (bind' (dn' S⊑S' (ret' var)) -- downcast the input
-         (bind' (app' var2 var) -- apply the original function
-         (ret' (up' T⊑T' var))) ) -- upcast the output
-⇀-up-uniqueness S⊑S' T⊑T' =
-  ( {!!}
-  , {!!})
-
-⇀-dn-uniqueness : ∀ S⊑S' T⊑T' →
-  dn (S⊑S' ⇀TP T⊑T')
-  ≈e bind (ret' (lda (dn' T⊑T' (app' var1 (up' S⊑S' var)))))
-⇀-dn-uniqueness = {!!}

formalizations/guarded-cubical/Syntax/Terms.agda

-{-# OPTIONS --cubical #-}
- -- to allow opening this module in other files while there are still holes
-{-# OPTIONS --allow-unsolved-metas #-}
-module Syntax.Terms  where
-
-open import Cubical.Foundations.Prelude renaming (comp to compose)
-open import Cubical.Data.Nat hiding (_·_)
-open import Cubical.Data.Sum
-open import Cubical.Relation.Nullary
-open import Cubical.Foundations.Function
-open import Cubical.Data.Prod hiding (map)
-open import Cubical.Foundations.Isomorphism
-open import Cubical.Data.List
-open import Cubical.Data.Empty renaming (rec to exFalso)
-
-open import Syntax.Types
-
-open TyPrec
-
-private
- variable
-   Δ Γ Θ Z : Ctx
-   R S T U : Ty
-
--- Values, Computations and Evaluation contexts,
--- quotiented by βη equivalence but *not* by order equivalence (i.e., up/dn laws)
-data Subst : (Δ : Ctx) (Γ : Ctx) → Type
-data Val : (Γ : Ctx) (S : Ty) → Type
-data EvCtx : (Γ : Ctx) (S : Ty) (T : Ty) → Type
-data Comp : (Γ : Ctx) (S : Ty) → Type
-
-private
-  variable
-    γ : Subst Δ Γ
-    δ : Subst Θ Δ
-    θ : Subst Z Θ
-
-    V V' : Val Γ S
-    M M' N N' : Comp Γ S
-    E E' F F' : EvCtx Γ S T
-
--- This isn't actually induction-recursion, this is just a hack to get
--- around limitations of Agda's mutual recursion for HITs
--- https://github.com/agda/agda/issues/5362
-_[_]vP : Val Γ S → Subst Δ Γ → Val Δ S
-_[_]cP : Comp Γ S → Subst Δ Γ → Comp Δ S
-_[_]∙P : EvCtx Γ S T → Comp Γ S → Comp Γ T
-varP : Val (S ∷ Γ) S
-retP : Comp [ S ] S
-appP : Comp (S ∷ (S ⇀ T) ∷ []) T
-
--- Explicit substitutions roughly following https://arxiv.org/pdf/1809.08646.pdf
--- but with some changes
--- Idea:
--- 1. Subst is a category
--- 2. Subst Γ (S ∷ Δ) ≅ Subst Γ Δ × Val Γ S
--- 3 Val - S , Comp - S, EvCtx - S T are Presheaves over Subst
--- 4. EvCtx Γ - = is a category enriched in Psh over Subst
--- 5. Comp Γ is a Psh(Subst)-enriched covariant presheaf over EvCtx Γ
-data Subst where
-  -- Subst is a cat
-  ids : Subst Γ Γ
-  _∘s_ : Subst Δ Θ → Subst Γ Δ → Subst Γ Θ
-  ∘IdL : ids ∘s γ ≡ γ
-  ∘IdR : γ ∘s ids ≡ γ
-  ∘Assoc : γ ∘s (δ ∘s θ) ≡ (γ ∘s δ) ∘s θ
-  isSetSubst : isSet (Subst Δ Γ)
-
-  -- [] is terminal
-  !s : Subst Γ []
-  []η : γ ≡ !s
-
-  -- universal property of S ∷ Γ
-  -- β (other one is in Val), η and naturality
-  _,s_ : Subst Γ Δ → Val Γ S → Subst Γ (S ∷ Δ)
-  wk : Subst (S ∷ Γ) Γ
-  wkβ : wk ∘s (δ ,s V) ≡ δ
-  ,sη : δ ≡ (wk ∘s δ ,s varP [ δ ]vP)
-
--- copied from similar operators
-infixl 4 _,s_
-infixr 9 _∘s_
-
-data Val where
-  -- values form a presheaf over substitutions
-  _[_]v : Val Γ S → Subst Δ Γ → Val Δ S
-  substId : V [ ids ]v ≡ V
-  substAssoc : V [ δ ∘s γ ]v ≡ (V [ δ ]v) [ γ ]v
-
-  -- with explicit substitutions we only need the one variable, which we can combine with weakening
-  var : Val (S ∷ Γ) S
-  varβ : var [ δ ,s V ]v ≡ V
-
-  -- by making these function symbols we avoid more substitution equations
-  zro : Val [] nat
-  suc : Val [ nat ] nat
-
-  lda : Comp (S ∷ Γ) T -> Val Γ (S ⇀ T) -- TODO: prove substitution under lambdas is admissible
-  -- V = λ x. V x
-  fun-η : V ≡ lda (appP [ (!s ,s (V [ wk ]v)) ,s var ]cP)
-
-  up : (S⊑T : TyPrec) -> Val [ ty-left S⊑T ] (ty-right S⊑T)
-
-  isSetVal : isSet (Val Γ S)
-
-_[_]vP = _[_]v
-varP = var
-
-data EvCtx where
-  ∙E : EvCtx Γ S S
-  _∘E_ : EvCtx Γ T U → EvCtx Γ S T → EvCtx Γ S U
-  ∘IdL : ∙E ∘E E ≡ E
-  ∘IdR : E ∘E ∙E ≡ E
-  ∘Assoc : E ∘E (F ∘E F') ≡ (E ∘E F) ∘E F'
-
-  _[_]e : EvCtx Γ S T → Subst Δ Γ → EvCtx Δ S T
-  substId : E [ ids ]e ≡ E
-  substAssoc : E [ γ ∘s δ ]e ≡ E [ γ ]e [ δ ]e
-
-  ∙substDist : ∙E {S = S} [ γ ]e ≡ ∙E
-  ∘substDist : (E ∘E F) [ γ ]e ≡ (E [ γ ]e) ∘E (F [ γ ]e)
-
-  bind : Comp (S ∷ Γ) T → EvCtx Γ S T
-  -- E[∙] ≡ x <- ∙; E[ret x]
-  ret-η : E ≡ bind (E [ wk ]e [ retP [ !s ,s var ]cP ]∙P)
-
-  dn : (S⊑T : TyPrec) → EvCtx [] (ty-right S⊑T) (ty-left S⊑T)
-
-  isSetEvCtx : isSet (EvCtx Γ S T)
-
-data Comp where
-  _[_]∙ : EvCtx Γ S T → Comp Γ S → Comp Γ T
-  plugId : ∙E [ M ]∙ ≡ M
-  plugAssoc : (F ∘E E) [ M ]∙ ≡ F [ E [ M ]∙ ]∙
-
-  _[_]c : Comp Δ S → Subst Γ Δ → Comp Γ S
-  -- presheaf
-  substId : M [ ids ]c ≡ M
-  substAssoc : M [ δ ∘s γ ]c ≡ (M [ δ ]c) [ γ ]c
-
-  -- Interchange law
-  substPlugDist : (E [ M ]∙) [ γ ]c ≡ (E [ γ ]e) [ M [ γ ]c ]∙
-
-  err : Comp [] S
-  -- E[err] ≡ err
-  strictness : E [ err [ !s ]c ]∙ ≡ err [ !s ]c
-
-  ret : Comp [ S ] S
-  -- x <- ret x; M ≡ M
-  ret-β : (bind M [ wk ]e [ ret [ !s ,s var ]c ]∙) ≡ M
-
-  app : Comp (S ∷ S ⇀ T ∷ []) T
-  -- (λ x. M) x ≡ M
-  fun-β : app [ (!s ,s ((lda M) [ wk ]v)) ,s var ]c ≡ M
-
-  matchNat : Comp Γ S → Comp (nat ∷ Γ) S → Comp (nat ∷ Γ) S
-  -- match 0 Kz (x . Ks) ≡ Kz
-  matchNatβz : (Kz : Comp Γ S)(Ks : Comp (nat ∷ Γ) S)
-             → matchNat Kz Ks [ ids ,s (zro [ !s ]v) ]c ≡ Kz
-  -- match (S V) Kz (x . Ks) ≡ Ks [ V / x ]
-  matchNatβs : (Kz : Comp Γ S)(Ks : Comp (nat ∷ Γ) S) (V : Val Γ nat)
-             → matchNat Kz Ks [ ids ,s (suc [ !s ,s V ]v) ]c ≡ (Ks [ ids ,s V ]c)
-  -- M[x] ≡ match x (M[0/x]) (x. M[S x/x])
-  matchNatη : M ≡ matchNat (M [ ids ,s (zro [ !s ]v) ]c) (M [ wk ,s (suc [ !s ,s var ]v) ]c)
-
-  isSetComp : isSet (Comp Γ S)
-appP = app
-retP = ret
-_[_]cP = _[_]c
-_[_]∙P = _[_]∙
-
--- More ordinary term constructors are admissible
--- up, dn, zro, suc, err, app, bind
-app' : (Vf : Val Γ (S ⇀ T)) (Va : Val Γ S) → Comp Γ T
-app' Vf Va = app [ !s ,s Vf ,s Va ]c
-
--- As well as substitution principles for them
-!s-nat : (γ : Subst Γ []) → !s ∘s γ ≡ !s
-!s-nat γ = []η
-
-!s-ext : {γ : Subst Γ []} → γ ≡ δ
-!s-ext = []η ∙ sym []η
-
-,s-nat : (γ ,s V) ∘s δ ≡ ((γ ∘s δ) ,s (V [ δ ]v))
-,s-nat =
-  ,sη ∙ cong₂ _,s_ (∘Assoc ∙ cong₂ (_∘s_) wkβ refl)
-               (substAssoc ∙ cong₂ _[_]v varβ refl)
-
-,s-ext : wk ∘s γ ≡ wk ∘s δ → (var [ γ ]v ≡ var [ δ ]v) → γ ≡ δ
-,s-ext wkp varp = ,sη ∙ cong₂ _,s_ wkp varp ∙ sym ,sη
-
--- Some examples for functions
-app'-nat : (γ : Subst Δ Γ) (Vf : Val Γ (S ⇀ T)) (Va : Val Γ S)
-         → app' Vf Va [ γ ]c ≡ app' (Vf [ γ ]v) (Va [ γ ]v)
-app'-nat γ Vf Va =
-  sym substAssoc
-  ∙ cong (app [_]c) (,s-nat ∙ cong₂ _,s_ (,s-nat  ∙ cong₂ _,s_ []η refl) refl)
-
-lda-nat : (γ : Subst Δ Γ) (M : Comp (S ∷ Γ) T)
-        → (lda M) [ γ ]v ≡ lda (M [ γ ∘s wk ,s var ]c)
-lda-nat {Δ = Δ}{Γ = Γ}{S = S} γ M =
-  fun-η
-  ∙ cong lda (cong (app [_]c) (cong₂ _,s_ (cong₂ _,s_ (sym ([]η)) (sym substAssoc
-                                                                                    ∙ cong (lda M [_]v) (sym wkβ)
-                                                                                    ∙ substAssoc))
-                                                      (sym varβ)
-                              ∙ cong (_,s (var [ the-subst ]v)) (sym ,s-nat)
-                              ∙ sym ,s-nat)
-             ∙ substAssoc
-             ∙ cong (_[ the-subst ]c) fun-β) where
-  the-subst : Subst (S ∷ Δ) (S ∷ Γ)
-  the-subst = γ ∘s wk ,s var
-
-fun-β' : (M : Comp (S ∷ Γ) T) (V : Val Γ S)
-       → app' (lda M) V ≡ M [ ids ,s V ]c
-fun-β' M V =
-  cong (app [_]c) (cong₂ _,s_ (cong₂ _,s_ (sym []η) ((sym substId ∙ cong (lda M [_]v) (sym wkβ)) ∙ substAssoc) ∙ sym ,s-nat)
-                              (sym varβ)
-                  ∙ sym ,s-nat)
-  ∙ substAssoc
-  ∙ cong (_[ ids ,s V ]c) fun-β
-
-fun-η' : V ≡ lda (app' (V [ wk ]v) var)
-fun-η' = fun-η
-
-err' : Comp Γ S
-err' = err [ !s ]c
-
-ret' : Val Γ S → Comp Γ S
-ret' V = ret [ !s ,s V ]c
-
-bind' : Comp Γ S → Comp (S ∷ Γ) T → Comp Γ T
-bind' M K = bind K [ M ]∙
-
-bind-nat : (bind M) [ γ ]e ≡ bind (M [ γ ∘s wk ,s var ]c)
-bind-nat {M = M} {γ = γ} = ret-η ∙ cong bind (cong (_[ ret [ !s ,s var ]c ]∙) (sym substAssoc)
-                             ∙ cong₂ _[_]∙ (cong (bind M [_]e) (sym wkβ) ∙ substAssoc)
-                                           (cong (ret [_]c) (cong₂ _,s_ !s-ext (sym varβ) ∙ sym ,s-nat) ∙ substAssoc)
-                             ∙ sym substPlugDist
-                             ∙ cong (_[ γ ∘s wk ,s var ]c) ret-β)
-
-bind'-nat : (bind' M N) [ γ ]c ≡ bind' (M [ γ ]c) (N [ γ ∘s wk ,s var ]c)
-bind'-nat = substPlugDist ∙ cong₂ _[_]∙ bind-nat refl
-
-ret-β' : bind' (ret' V) M ≡ (M [ ids ,s V ]c)
-ret-β' =
-  (cong₂ _[_]∙ ((sym substId ∙ cong₂ _[_]e refl (sym wkβ)) ∙ substAssoc)
-               (cong (ret [_]c) (,s-ext !s-ext (varβ ∙ (sym varβ ∙ sym varβ) ∙ cong (var [_]v) (sym ,s-nat))) ∙ substAssoc)
-  ∙ sym substPlugDist)
-  ∙ cong₂ _[_]c ret-β refl
-
-ret-η' : M ≡ bind' M (ret' var)
-ret-η' = sym plugId ∙ cong₂ _[_]∙ (ret-η ∙ cong bind (cong₂ _[_]∙ ∙substDist refl ∙ plugId)) refl
-
-up' : ∀ S⊑T → Val Γ (ty-left S⊑T) → Val Γ (ty-right S⊑T)
-up' S⊑T V = up S⊑T [ !s ,s V ]v
-
-upC : ∀ S⊑T → Val Γ (ty-left S⊑T) → Comp Γ (ty-right S⊑T)
-upC S⊑T V = ret' (up' S⊑T V)
-
-upE : ∀ S⊑T → EvCtx Γ (ty-left S⊑T) (ty-right S⊑T)
-upE S⊑T = bind (ret' (up' S⊑T var))
-
-dn' : ∀ S⊑T → Comp Γ (ty-right S⊑T) → Comp Γ (ty-left S⊑T)
-dn' S⊑T M = dn S⊑T [ !s ]e [ M ]∙
-
-ids1-expand : Path (Subst (S ∷ []) (S ∷ [])) ids (!s ,s var)
-ids1-expand = ,sη ∙ cong₂ _,s_ []η substId
-
-var0 : Val (S ∷ Γ) S
-var0 = var
-
-var1 : Val (S ∷ T ∷ Γ) T
-var1 = var [ wk ]v
-
-var2 : Val (S ∷ T ∷ U ∷ Γ) U
-var2 = var1 [ wk ]v
-
-wk-expand : Path (Subst (S ∷ T ∷ []) (T ∷ [])) wk (!s ,s var1)
-wk-expand = ,s-ext !s-ext (sym varβ)
-
-big-η-expand-fun : ∀ (V : Val [ U ] (S ⇀ T)) →
-  V ≡ lda (bind' (ret' var)
-          (bind' (app' (V [ !s ,s var2 ]v) var)
-          (ret' var)))
-big-η-expand-fun V =
-  fun-η ∙ cong lda ((ret-η'
-  ∙ cong₂ bind'
-    (cong (app [_]c) (cong₂ _,s_ (cong₂ _,s_ !s-ext (cong (V [_]v) (wk-expand ∙ ,s-ext !s-ext (varβ ∙ (((sym substId ∙ cong₂ _[_]v refl (sym wkβ)) ∙ substAssoc) ∙ cong₂ _[_]v (sym varβ) refl) ∙ sym substAssoc)) ∙ substAssoc) ∙ sym ,s-nat) (sym varβ) ∙ sym ,s-nat) ∙ substAssoc)
-    (cong (ret [_]c) (,s-ext !s-ext (((varβ ∙ sym varβ) ∙ cong₂ _[_]v (sym varβ) refl) ∙ sym substAssoc)) ∙ substAssoc) ∙ sym bind'-nat) ∙ sym ret-β')