From fa06358323ee7b72abfdb7bc3b0a0dda539ce01f Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 18 May 2023 17:43:38 -0400
Subject: [PATCH] work on new syntx

---
 .../guarded-cubical/Syntax/Context.agda       | 110 ++++++
 .../guarded-cubical/Syntax/SyntaxNew.agda     | 343 ++++++++++--------
 .../guarded-cubical/Syntax/Types.agda         |  14 +-
 3 files changed, 305 insertions(+), 162 deletions(-)
 create mode 100644 formalizations/guarded-cubical/Syntax/Context.agda

diff --git a/formalizations/guarded-cubical/Syntax/Context.agda b/formalizations/guarded-cubical/Syntax/Context.agda
new file mode 100644
index 0000000..06b92ed
--- /dev/null
+++ b/formalizations/guarded-cubical/Syntax/Context.agda
@@ -0,0 +1,110 @@
+module Syntax.Context where
+
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.HLevels
+open import Cubical.Relation.Nullary
+open import Cubical.Foundations.Prelude
+open import Cubical.Functions.FunExtEquiv
+open import Cubical.Functions.Embedding
+open import Cubical.Data.Nat
+-- open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum hiding (map)
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Unit
+-- open import Cubical.Data.Fin hiding (_/_)
+open import Cubical.Data.FinSet
+open import Cubical.Data.FinSet.Constructors
+
+private
+  variable
+    â„“ â„“' â„“'' : Level
+
+record Ctx (A : Type â„“) : Type (â„“-max â„“ (â„“-suc â„“-zero)) where
+  field
+    var : Type
+    isFinSetVar : isFinSet var
+    el : var → A
+
+  varFinSet : FinSet â„“-zero
+  varFinSet = var , isFinSetVar
+
+open Ctx
+
+module _ {A : Type â„“} where
+
+  Var : Ctx A → Type
+  Var Γ = Γ .var
+
+  Ctx≡ : (Γ Δ : Ctx A)
+       → (p : Var Γ ≡ Var Δ)
+       → PathP (λ i → p i → A) (Γ .el) (Δ .el)   
+       → Γ ≡ Δ
+  Ctx≡ Γ Δ p q i .var = p i
+  Ctx≡ Γ Δ p q i .isFinSetVar = lem i
+    where
+      lem : PathP (λ i → isFinSet (p i)) (Γ .isFinSetVar) (Δ .isFinSetVar)
+      lem = (isProp→PathP (λ i → isPropIsFinSet) (Γ .isFinSetVar) (Δ .isFinSetVar))
+  Ctx≡ Γ Δ p q i .el x = q i x
+
+  empty-ctx : Ctx A
+  empty-ctx .var         = ⊥
+  empty-ctx .isFinSetVar = isFinSetFin
+  empty-ctx .el          = λ ()
+
+  singleton : A → Ctx A
+  singleton a .var = Unit
+  singleton a .isFinSetVar = isFinSetUnit
+  singleton a .el = λ _ → a
+
+  -- the-var : (a : A) → singleton a .var
+  -- the-var a = tt
+
+  append : Ctx A → Ctx A → Ctx A
+  var (append Γ₁ Γ₂) = Γ₁ .var ⊎ Γ₂ .var
+  isFinSetVar (append Γ₁ Γ₂) = isFinSet⊎ (varFinSet Γ₁) (varFinSet Γ₂)
+  el (append Γ₁ Γ₂) (inl x₁) = Γ₁ .el x₁
+  el (append Γ₁ Γ₂) (inr x₂) = Γ₂ .el x₂
+
+  append-i₁-el : ∀ Γ₁ Γ₂ (x₁ : Γ₁ .var) → (append Γ₁ Γ₂) .el (inl x₁) ≡ Γ₁ .el x₁
+  append-i₁-el = λ Γ₁ Γ₂ x₁ → refl
+
+  cons : Ctx A → A → Ctx A
+  cons Γ a = append Γ (singleton a)
+
+  module _ (B : A → Type ℓ')  where
+    substitution : ∀ (Γ : Ctx A) → Type ℓ'
+    substitution Γ = ∀ (x : Γ . var) → B (Γ .el x)
+
+    singleton-subst : (x : A) → B x → substitution (singleton x)
+    singleton-subst x b tt = b
+
+    append-subst : ∀ {Γ₁ Γ₂} → substitution Γ₁ → substitution Γ₂ → substitution (append Γ₁ Γ₂)
+    append-subst γ₁ γ₂ (inl x) = γ₁ x
+    append-subst γ₁ γ₂ (inr x) = γ₂ x
+
+    append-subst-inl : {Γ₁ Γ₂ : Ctx A} → (γ₁ : substitution Γ₁) → (γ₂ : substitution Γ₂)
+                     → (x₁ : Var Γ₁)
+                     → (append-subst {Γ₁ = Γ₁}{Γ₂ = Γ₂} γ₁ γ₂ (inl x₁)) ≡ (γ₁ x₁)
+    append-subst-inl γ₁ Γ₂ x₁ = refl
+
+    cons-subst : ∀ {Γ x} → substitution Γ → B x → substitution (cons Γ x)
+    cons-subst γ v = append-subst γ (singleton-subst _ v)
+
+  finProd : (X : FinSet ℓ-zero) → (X .fst → Ctx A) → Ctx A
+  finProd X Γs .var = Σ[ x ∈ X .fst ] Γs x .var
+  finProd X Γs .isFinSetVar = isFinSetΣ X λ x → _ , (Γs x .isFinSetVar)
+  finProd X Γs .el (x , y) = Γs x .el y
+
+  append-inj-el : ∀ (X : FinSet ℓ-zero) (Γs : X .fst → Ctx A) (x : X .fst) (y : Γs x .var)
+                → finProd X Γs .el (x , y) ≡ Γs x .el y
+  append-inj-el X Γs x y = refl
+
+  module _ (B : A → Type ℓ') (X : FinSet ℓ-zero) (Γs : X .fst → Ctx A) where
+    finProdSubsts : (∀ (x : X .fst) → substitution B (Γs x)) → substitution B (finProd X Γs)
+    finProdSubsts γs (x , y) = γs x y
+
+map : ∀ {A : Type ℓ}{A' : Type ℓ'} → (A → A') → Ctx A → Ctx A'
+map f Γ .var = Γ .var
+map f Γ .isFinSetVar = Γ .isFinSetVar
+map f Γ .el x = f (Γ .el x)
diff --git a/formalizations/guarded-cubical/Syntax/SyntaxNew.agda b/formalizations/guarded-cubical/Syntax/SyntaxNew.agda
index cbffc05..41e59c7 100644
--- a/formalizations/guarded-cubical/Syntax/SyntaxNew.agda
+++ b/formalizations/guarded-cubical/Syntax/SyntaxNew.agda
@@ -9,10 +9,8 @@ open import Common.Later hiding (next)
 
 module Syntax.SyntaxNew  where
 
-
-
 open import Cubical.Foundations.Prelude renaming (comp to compose)
-open import Cubical.Data.Nat hiding (_·_) renaming (ℕ to Nat)
+open import Cubical.Data.Nat hiding (_·_)
 open import Cubical.Relation.Nullary
 open import Cubical.Foundations.Function
 open import Cubical.Data.Prod hiding (map)
@@ -23,33 +21,15 @@ open import Cubical.Data.List
 
 open import Cubical.Data.Empty renaming (rec to exFalso)
 
-
-import Syntax.DeBruijnCommon
-
+open import Syntax.Context
+-- import Syntax.DeBruijnCommon
 
 private
  variable
-   â„“ : Level
-
-
+   â„“ â„“' â„“'' : Level
 
 open import Syntax.Types
-
-
-
-
-private
-  variable
-    α : IntExt
-     
-
-
-
-
-
-
-
-
+open Ctx
 -- ############### Terms / Term Precision ###############
 
 -- All constructors below except for those for upcast and downcast are simultaneously
@@ -58,163 +38,220 @@ private
 -- This explains why Ξ is generic in all but the up and dn constructors,
 -- where it is Empty to indicate that we do not obtain term precision congruence rules.
 
-data PureImpure : Type where
-  Pure Impure : PureImpure
-
-data Tm : {v : PureImpure} -> {α : IntExt} -> {Ξ : iCtx} -> (Γ : Ctx {α} Ξ) -> Ty {α} Ξ -> Type ℓ-zero
-
--- data Val : {α : IntExt} -> {Ξ : iCtx} -> (Γ : Ctx {α} Ξ) -> Ty {α} Ξ -> Type ℓ-zero
-
-
-tm-endpt : ∀ {v} {α} (p : Interval) -> {Γ : Ctx {α} Full} -> {c : Ty {α} Full} ->
-  Tm {v} {α} {Full} Γ c ->
-  Tm {v} {α} {Empty} (ctx-endpt p Γ) (ty-endpt p c)
-
-
-
-_[_] : ∀ {α Γ A B}
-  → Tm {Impure} {α} {Empty} (B :: Γ) A
-  → Tm {Pure} {α} {Empty} Γ B
-  → Tm {Impure} {α} {Empty} Γ A
-_[_] = {!!}
-
-wk : ∀ {v α Γ A B} -> Tm {v} {α} {Empty} Γ A ->
-  Tm {v} {α} {Empty} (B :: Γ) A
-wk = {!!}
-
-
-
-
--- data Val where
- 
-
-data Tm where
-  var : ∀ {α Ξ Γ T} -> Γ ∋ T -> Tm {Pure} {α} {Ξ} Γ T
-  lda : ∀ {α Ξ Γ S T} -> (Tm {Impure} {α} {Ξ} (S :: Γ) T) -> Tm {Pure} Γ (S ⇀ T)
-  app : ∀ {α Ξ Γ S T} -> (Tm {Pure} {α} {Ξ} Γ (S ⇀ T)) -> (Tm {Pure} Γ S) -> (Tm {Impure} Γ T)
-  err : ∀ {α Ξ Γ A} -> Tm {Impure} {α} {Ξ} Γ A
-  zro : ∀ {α Ξ Γ} -> Tm {Pure} {α} {Ξ} Γ nat
-  suc : ∀ {α Ξ Γ} -> Tm {Pure} {α} {Ξ} Γ nat -> Tm {Pure} Γ nat
-  ret : ∀ {α Ξ Γ A} -> Tm {Pure} {α} {Ξ} Γ A -> Tm {Impure} Γ A
-  bind : ∀ {α Ξ Γ A B} -> Tm {Pure} {α} {Ξ} Γ A ->
-                          Tm {Impure} {α} {Ξ} (A :: Γ) B -> Tm {Impure} {α} {Ξ} Γ B
-
-  inj-nat : ∀ {α Ξ Γ} -> Tm {Pure} {α} {Ξ} Γ nat -> Tm {Pure} Γ dyn
-  inj-arr-ext : ∀ {Ξ Γ} -> Tm {Pure} {Ext} {Ξ} Γ (dyn ⇀ dyn)     -> Tm {Pure} {Ext} Γ dyn
-  inj-arr-int : ∀ {Ξ Γ} -> Tm {Pure} {Int} {Ξ} Γ (▹ (dyn ⇀ dyn)) -> Tm {Pure} {Int} Γ dyn
-  case-nat :     ∀ {α Ξ Γ B} -> Tm {Pure} {α}   {Ξ} Γ dyn ->
-                                Tm {Impure} {α}   {Ξ} (nat :: Γ) B             -> Tm {Impure} {α} Γ B 
-  case-arr-ext : ∀ {Ξ Γ B}   -> Tm {Pure} {Ext} {Ξ} Γ dyn ->
-                                Tm {Impure} {Ext} {Ξ} ((dyn ⇀ dyn) :: Γ) B     -> Tm {Impure} {Ext} Γ B 
-  case-arr-int : ∀ {Ξ Γ B}   -> Tm {Pure} {Int} {Ξ} Γ dyn ->
-                                Tm {Impure} {Int} {Ξ} ((▹ (dyn ⇀ dyn)) :: Γ) B -> Tm {Impure} {Int} Γ B 
-
-
-  -- Other term precision rules:
+data Val   : (Ξ : iCtx) -> (Γ : TyCtx Ξ) -> Ty Ξ -> Type (ℓ-suc ℓ-zero)
+data Comp  : (Ξ : iCtx) -> (Γ : TyCtx Ξ) -> Ty Ξ -> Type (ℓ-suc ℓ-zero)
+data EvCtx : (Ξ : iCtx) -> (Γ : TyCtx Ξ) -> Ty Ξ -> Ty Ξ -> Type (ℓ-suc ℓ-zero)
+val-endpt : ∀ (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} ->
+  Val Full Γ c ->
+  Val Empty (ctx-endpt p Γ) (ty-endpt p c)
+comp-endpt : ∀ (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} ->
+  Comp Full Γ c ->
+  Comp Empty (ctx-endpt p Γ) (ty-endpt p c)
+evctx-endpt : ∀ (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} {d : Ty Full} ->
+  EvCtx Full Γ c d ->
+  EvCtx Empty (ctx-endpt p Γ) (ty-endpt p c) (ty-endpt p d)
+
+-- TODO: strengthen the inductive hypothesis
+--
+-- Substitution : ∀ {Ξ} → TyCtx Ξ → TyCtx Ξ → Type (ℓ-suc ℓ-zero)
+
+_[_]v : ∀ {Δ Γ A}
+  → Val Empty Γ A
+  → substitution (Val Empty Δ) Γ
+  → Val Empty Δ A
+_[_]c : ∀ {Δ Γ A}
+  → Comp Empty Γ A
+  → substitution (Val Empty Δ) Γ
+  → Comp Empty Δ A
+_[_]c1 : ∀ {Γ A B}
+  → Comp Empty (cons Γ A) B
+  → (Val Empty Γ A)
+  → Comp Empty Γ B
+-- wk : ∀ {v α Γ A B} -> Tm {v} {Empty} Γ A ->
+--   Tm {v} {Empty} (B :: Γ) A
+-- wk = {!!}
+
+
+
+
+data Val where
+  varVal : ∀ {Ξ Γ} -> (x : Γ .var) -> Val Ξ Γ (Γ .el x)
+  lda : ∀ {Ξ Γ S T} -> (Comp Ξ (cons Γ S) T) -> Val Ξ Γ (S ⇀ T)
+  zro : ∀ {Ξ Γ} -> Val Ξ Γ nat
+  suc : ∀ {Ξ Γ} -> Val Ξ Γ nat -> Val Ξ Γ nat
+  up : ∀ {Γ} -> (S⊑T : Ty Full) -> Val Empty Γ (ty-left S⊑T) -> Val Empty Γ (ty-right S⊑T) 
+  up-UB  : ∀ {Γ} → (S⊑T : Ty Full) → Val Full Γ (ty-refl (ty-left S⊑T)) -> Val Full Γ S⊑T
+  up-LUB : ∀ {Γ} → (S⊑T : Ty Full) → Val Full Γ S⊑T -> Val Full Γ (ty-refl (ty-right S⊑T))
+
+  η-fun : ∀ {Γ A B} (Vf : Val Empty Γ (A ⇀ B)) ->
+    Vf ≡ lda (app ? ?)
+    -- lda (app (wk Vf) (var x)) ≡ Vf
+
+  trans : ∀ {Γ Δ : TyCtx Full} -> {A B : Ty Full} ->
+    (V : Val Full Γ A) -> (U : Val Full Δ B) ->
+    (ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
+    (ty-p : ty-endpt l B ≡ ty-endpt r A)
+    (tm-p : PathP (λ i → Val Empty (ctx-p i) (ty-p i))
+                  (val-endpt l {Δ} {B} U)
+                  (val-endpt r {Γ} {A} V)) ->
+    Val Full (CompCtx Δ Γ ctx-p) (comp B A ty-p)
+  ord-squash : ∀ {Γ c} (leq leq' : Val Full Γ c) ->
+    (val-endpt l leq ≡ val-endpt l leq') →
+    (val-endpt r leq ≡ val-endpt r leq') ->
+    leq ≡ leq'
+  isSetVal : ∀ {Γ S} → isSet (Val Empty Γ S)
+
+data Comp where
+  app : ∀ {Ξ Γ S T} → Val Ξ Γ (S ⇀ T) → Val Ξ Γ S → Comp Ξ Γ T
+  err : ∀ {Ξ Γ S} → Comp Ξ Γ S
+  ret : ∀ {Ξ Γ S} → Val Ξ Γ S → Comp Ξ Γ S
+  bind : ∀ {Ξ Γ S T} → Comp Ξ Γ S → Comp Ξ (cons Γ S) T → Comp Ξ Γ T
+  matchNat : ∀ {Ξ Γ S} → Val Ξ Γ nat → Comp Ξ Γ S → Comp Ξ (cons Γ nat) S → Comp Ξ Γ S
+  dn : ∀ {Γ} → (S⊑T : Ty Full) → Comp Empty Γ (ty-right S⊑T) → Comp Empty Γ (ty-left S⊑T)
+  dn-LB  : ∀ {Γ} → (S⊑T : Ty Full) → Comp Full Γ (ty-refl (ty-right S⊑T)) -> Comp Full Γ S⊑T
+  dn-GLB : ∀ {Γ} → (S⊑T : Ty Full) → Comp Full Γ S⊑T -> Comp Full Γ (ty-refl (ty-left S⊑T))
+
+  -- effect rules
+  err-bot : ∀ {Γ} (B : Ty Empty) (M : Comp Empty Γ B) -> Comp Full (ctx-refl Γ) (ty-refl B)
+  -- TODO: strictness
+
+  -- βη
+  
+  β-fun : ∀ {Γ A B} (M : Comp Empty (cons Γ A) B) (V : Val Empty Γ A) ->
+    app (lda M) V ≡ (M [ V ]c1)
+  
+  trans : ∀ {Γ Δ : TyCtx Full} -> {A B : Ty Full} ->
+    (M : Comp Full Γ A) -> (N : Comp Full Δ B) ->
+    (ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
+    (ty-p : ty-endpt l B ≡ ty-endpt r A)
+    (tm-p : PathP (λ i → Comp Empty (ctx-p i) (ty-p i))
+                  (comp-endpt l {Δ} {B} N)
+                  (comp-endpt r {Γ} {A} M)) ->
+    Comp Full (CompCtx Δ Γ ctx-p) (comp B A ty-p)
+  
+  ord-squash : ∀ {Γ c} (leq leq' : Comp Full Γ c) ->
+    (comp-endpt l leq ≡ comp-endpt l leq') →
+    (comp-endpt r leq ≡ comp-endpt r leq') ->
+    leq ≡ leq'
+  isSetComp : ∀ {Γ S} → isSet (Comp Empty Γ S)
+data EvCtx where
+
+val-endpt = {!!}
+comp-endpt = {!!}
+evctx-endpt = {!!}
+
+_[_]v = {!!}
+_[_]c = {!!}
+M [ V ]c1 = M [ cons-subst (Val Empty _) varVal V ]c
+
+-- data Tm where
+--   app : ∀ {α Ξ Γ S T} -> (Tm {Pure} {Ξ} Γ (S ⇀ T)) -> (Tm {Pure} Γ S) -> (Tm {Impure} Γ T)
+--   err : ∀ {α Ξ Γ A} -> Tm {Impure} {Ξ} Γ A
+--   ret : ∀ {α Ξ Γ A} -> Tm {Pure} {Ξ} Γ A -> Tm {Impure} Γ A
+--   bind : ∀ {α Ξ Γ A B} -> Tm {Pure} {Ξ} Γ A ->
+--                           Tm {Impure} {Ξ} (A :: Γ) B -> Tm {Impure} {Ξ} Γ B
+
+--   inj-nat : ∀ {α Ξ Γ} -> Tm {Pure} {Ξ} Γ nat -> Tm {Pure} Γ dyn
+--   inj-arr-ext : ∀ {Ξ Γ} -> Tm {Pure} {Ext} {Ξ} Γ (dyn ⇀ dyn)     -> Tm {Pure} {Ext} Γ dyn
+--   inj-arr-int : ∀ {Ξ Γ} -> Tm {Pure} {Int} {Ξ} Γ (▹ (dyn ⇀ dyn)) -> Tm {Pure} {Int} Γ dyn
+--   case-nat :     ∀ {α Ξ Γ B} -> Tm {Pure}   {Ξ} Γ dyn ->
+--                                 Tm {Impure}   {Ξ} (nat :: Γ) B             -> Tm {Impure} Γ B 
+--   case-arr-ext : ∀ {Ξ Γ B}   -> Tm {Pure} {Ext} {Ξ} Γ dyn ->
+--                                 Tm {Impure} {Ext} {Ξ} ((dyn ⇀ dyn) :: Γ) B     -> Tm {Impure} {Ext} Γ B 
+--   case-arr-int : ∀ {Ξ Γ B}   -> Tm {Pure} {Int} {Ξ} Γ dyn ->
+--                                 Tm {Impure} {Int} {Ξ} ((▹ (dyn ⇀ dyn)) :: Γ) B -> Tm {Impure} {Int} Γ B 
+
+
+--   -- Other term precision rules:
  
-  err-bot : ∀ {α Γ} (B : Ty {α} Empty) (M : Tm {Impure} {α} {Empty} Γ B) -> Tm {Impure} {α} {Full} (ctx-refl Γ) (ty-refl B)
-  --err-bot : ∀ {α} {Γ : Ctx Full} (c : Ty Full)
-  --  (M : Tm {Impure} {α} {Empty} (ctx-endpt r Γ) (ty-right c)) -> Tm {Impure} {α} {Full} Γ c
-  -- TODO do we need to restrict the left endpoint of Γ?
+--   err-bot : ∀ {α Γ} (B : Ty Empty) (M : Tm {Impure} {Empty} Γ B) -> Tm {Impure} {Full} (ctx-refl Γ) (ty-refl B)
+--   --err-bot : ∀ {Γ : TyCtx Full} (c : Ty Full)
+--   --  (M : Tm {Impure} {Empty} (ctx-endpt r Γ) (ty-right c)) -> Tm {Impure} {Full} Γ c
+--   -- TODO do we need to restrict the left endpoint of Γ?
 
-  trans : ∀ {v : PureImpure} {Γ Δ : Ctx {α} Full} -> {A B : Ty Full} ->
-    (M : Tm {v} Γ A) -> (N : Tm {v} Δ B) ->
-    (ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
-    (ty-p :  ty-endpt l B ≡ ty-endpt r A)
-    (tm-p : PathP (λ i → Tm {v} (ctx-p i) (ty-p i)) (tm-endpt l {Δ} {B} N) (tm-endpt r {Γ} {A} M)) ->
-    Tm {v} (CompCtx Δ Γ ctx-p) (comp B A ty-p)
+--   trans : ∀ {v : PureImpure} {Γ Δ : TyCtx Full} -> {A B : Ty Full} ->
+--     (M : Tm {v} Γ A) -> (N : Tm {v} Δ B) ->
+--     (ctx-p : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
+--     (ty-p :  ty-endpt l B ≡ ty-endpt r A)
+--     (tm-p : PathP (λ i → Tm {v} (ctx-p i) (ty-p i)) (tm-endpt l {Δ} {B} N) (tm-endpt r {Γ} {A} M)) ->
+--     Tm {v} (CompCtx Δ Γ ctx-p) (comp B A ty-p)
 
-  -- Cast rules
+--   -- Cast rules
 
 
 
-  -- Equational theory:
+--   -- Equational theory:
   
-  β-fun : ∀ {α Γ A B} {M : Tm {Impure} {α} {Empty} (A :: Γ) B} {V : Tm {Pure} {α} {Empty} Γ A} ->
-    app (lda M) V ≡ M [ V ]
-
-
-  η-fun : ∀ {α Γ A B} {Vf : Tm {Pure} {α} {Empty} Γ (A ⇀ B)} {x : (A :: Γ) ∋ A} ->
-    lda (app (wk Vf) (var x)) ≡ Vf
+-- {-
+--   β-case :
 
-{-
-  β-case :
-
-  η-case :
+--   η-case :
 
-  β-ret :
+--   β-ret :
 
-  η-ret :
--}
+--   η-ret :
+-- -}
 
-  -- Propositional truncation:
+--   -- Propositional truncation:
   
-  -- squash : ∀ {v α Ξ Γ A} -> (M N : Tm {v} {α} {Ξ} Γ A) -> (p q : M ≡ N) -> p ≡ q
-  squash : ∀ {v α Ξ Γ A} -> isSet (Tm {v} {α} {Ξ} Γ A)
+--   -- squash : ∀ {v α Ξ Γ A} -> (M N : Tm {v} {Ξ} Γ A) -> (p q : M ≡ N) -> p ≡ q
+--   squash : ∀ {v α Ξ Γ A} -> isSet (Tm {v} {Ξ} Γ A)
 
-  -- Quotient the ordering:
+--   -- Quotient the ordering:
   
-  ord-squash : ∀ {v α Γ c}
-    (M : Tm {v} {α} {Empty} (ctx-endpt l Γ) (ty-left c))
-    (N : Tm {v} {α} {Empty} (ctx-endpt r Γ) (ty-right c)) ->
-    (leq leq' : Tm {v} {α} {Full} Γ c) ->
-    (tm-endpt l {Γ} {c} leq  ≡ M) -> (tm-endpt r {Γ} {c} leq  ≡ N) ->
-    (tm-endpt l {Γ} {c} leq' ≡ M) -> (tm-endpt r {Γ} {c} leq' ≡ N) ->
-    leq ≡ leq'
 
 
-_⊑tm_ : ∀ {v α Γ A B} {c : A ⊑ B} ->
-  Tm {v} {α} {Empty} (ctx-endpt l Γ) A -> Tm {v} {α} {Empty} (ctx-endpt r Γ) B -> Type
+-- _⊑tm_ : ∀ {v α Γ A B} {c : A ⊑ B} ->
+--   Tm {v} {Empty} (ctx-endpt l Γ) A -> Tm {v} {Empty} (ctx-endpt r Γ) B -> Type
 
 
-_⊑tm_ {v} {α} {Γ} {A} {B} {c , eq1 , eq2} M N = Σ[ M⊑N ∈ Tm {v} {α} {Full} Γ c ]
-  ((tm-endpt l {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt l Γ)) (sym eq1) M) ×
-   (tm-endpt r {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt r Γ)) (sym eq2) N))
+-- _⊑tm_ {v} {Γ} {A} {B} {c , eq1 , eq2} M N = Σ[ M⊑N ∈ Tm {v} {Full} Γ c ]
+--   ((tm-endpt l {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt l Γ)) (sym eq1) M) ×
+--    (tm-endpt r {Γ} {c} M⊑N ≡ subst (Tm (ctx-endpt r Γ)) (sym eq2) N))
 
 
 -- Recall:
--- tm-endpt : (p : Interval) -> {Γ : Ctx Full} -> {c : Ty Full} ->
+-- tm-endpt : (p : Interval) -> {Γ : TyCtx Full} -> {c : Ty Full} ->
 --   Tm {Full} Γ c ->
 --   Tm {Empty} (ctx-endpt p Γ) (ty-endpt p c)
 
+-- tm-endpt = ?
+-- tm-endpt p {Γ} {c} (var x) = var (∋-ctx-endpt p x)
+-- tm-endpt p {Γ} {(_ ⇀ cout)} (lda M1⊑M2) = lda (tm-endpt p {(_ ::  Γ)} {cout} M1⊑M2)
+-- tm-endpt p {Γ} {cout} (app {S = cin} M1⊑M2 N1⊑N2) =
+--   app (tm-endpt p {Γ} {(cin ⇀ cout)} M1⊑M2) (tm-endpt p {Γ} {cin} N1⊑N2)
 
-tm-endpt p {Γ} {c} (var x) = var (∋-ctx-endpt p x)
-
-tm-endpt p {Γ} {(_ ⇀ cout)} (lda M1⊑M2) = lda (tm-endpt p {(_ ::  Γ)} {cout} M1⊑M2)
-tm-endpt p {Γ} {cout} (app {S = cin} M1⊑M2 N1⊑N2) =
-  app (tm-endpt p {Γ} {(cin ⇀ cout)} M1⊑M2) (tm-endpt p {Γ} {cin} N1⊑N2)
-
-tm-endpt p {Γ} {c} err = err
-tm-endpt p {Γ} zro = zro
-tm-endpt p {Γ} (suc M1⊑M2) = suc (tm-endpt p {Γ} {nat} M1⊑M2)
+-- tm-endpt p {Γ} {c} err = err
+-- tm-endpt p {Γ} zro = zro
+-- tm-endpt p {Γ} (suc M1⊑M2) = suc (tm-endpt p {Γ} {nat} M1⊑M2)
 
--- Term-precision-only rules
---tm-endpt l .(ctx-refl _) c (err-bot .c N) = err
---tm-endpt r .(ctx-refl _) c (err-bot {Γ} .c N) =
---  transport (sym (λ i → Tm (ctx-endpt-refl {Γ} r i) (ty-right c))) N
--- Goal:  Tm Γ (ty-right c) ≡ Tm (ctx-endpt r (ctx-refl Γ)) (ty-right c)
+-- -- Term-precision-only rules
+-- --tm-endpt l .(ctx-refl _) c (err-bot .c N) = err
+-- --tm-endpt r .(ctx-refl _) c (err-bot {Γ} .c N) =
+-- --  transport (sym (λ i → Tm (ctx-endpt-refl {Γ} r i) (ty-right c))) N
+-- -- Goal:  Tm Γ (ty-right c) ≡ Tm (ctx-endpt r (ctx-refl Γ)) (ty-right c)
 
-tm-endpt p (err-bot B x) = {!!}
+-- tm-endpt p (err-bot B x) = {!!}
 
 
 
-tm-endpt l {Γ} (trans c _ _ _ _) = {!!}
-tm-endpt r {Γ} (trans c _ _ _ _) = {!!}
+-- tm-endpt l {Γ} (trans c _ _ _ _) = {!!}
+-- tm-endpt r {Γ} (trans c _ _ _ _) = {!!}
 
--- Truncation
-tm-endpt p {Γ} {c} (squash M1⊑M2 M1'⊑M2' eq eq' i j) =
-  squash (tm-endpt p {Γ} {c} M1⊑M2) (tm-endpt p {Γ} {c} M1'⊑M2')
-    (λ k → tm-endpt p {Γ} {c} (eq k)) (λ k → tm-endpt p {Γ} {c} (eq' k)) i j
+-- -- Truncation
+-- tm-endpt p {Γ} {c} (squash M1⊑M2 M1'⊑M2' eq eq' i j) =
+--   squash (tm-endpt p {Γ} {c} M1⊑M2) (tm-endpt p {Γ} {c} M1'⊑M2')
+--     (λ k → tm-endpt p {Γ} {c} (eq k)) (λ k → tm-endpt p {Γ} {c} (eq' k)) i j
 
-tm-endpt p (ret x) = {!!}
-tm-endpt p (bind x x₁) = {!!}
-tm-endpt p (inj-nat x) = {!!}
-tm-endpt p (inj-arr-ext x) = {!!}
-tm-endpt p (inj-arr-int x) = {!!}
-tm-endpt p (case-nat x x₁) = {!!}
-tm-endpt p (case-arr-ext x x₁) = {!!}
-tm-endpt p (case-arr-int x x₁) = {!!}
-tm-endpt p (ord-squash x x₁ x₂ x₃ x₄ x₅ x₆ x₇ i) = {!!}
+-- tm-endpt p (ret x) = {!!}
+-- tm-endpt p (bind x x₁) = {!!}
+-- tm-endpt p (inj-nat x) = {!!}
+-- tm-endpt p (inj-arr-ext x) = {!!}
+-- tm-endpt p (inj-arr-int x) = {!!}
+-- tm-endpt p (case-nat x x₁) = {!!}
+-- tm-endpt p (case-arr-ext x x₁) = {!!}
+-- tm-endpt p (case-arr-int x x₁) = {!!}
+-- tm-endpt p (ord-squash x x₁ x₂ x₃ x₄ x₅ x₆ x₇ i) = {!!}
 
 
 
@@ -224,13 +261,13 @@ tm-endpt p (ord-squash x x₁ x₂ x₃ x₄ x₅ x₆ x₇ i) = {!!}
 {-
 
 -- Substitution and Renaming using De Bruijn framework
-module DB_Base = Syntax.DeBruijnCommon (Ty Empty) (Ctx Empty) · (_::_) _∋_ vz vs (Tm Ext {Empty})
+module DB_Base = Syntax.DeBruijnCommon (Ty Empty) (TyCtx Empty) · (_::_) _∋_ vz vs (Tm Ext {Empty})
 open DB_Base -- Brings in definitions of ProofT, Kit, Subst
 
 
 -- Lift function --
 
-lft : {Δ Γ : Ctx Empty} {S : Ty Empty} {_◈_ : ProofT}
+lft : {Δ Γ : TyCtx Empty} {S : Ty Empty} {_◈_ : ProofT}
        (K : Kit _◈_) (τ : Subst Δ Γ _◈_) {T : Ty Empty} (h : (Γ :: S) ∋ T) -> (Δ :: S) ◈ T       
 lft (kit vr tm wk) Ï„ vz = vr vz
 lft (kit vr tm wk) Ï„ (vs x) = wk (Ï„ x)
@@ -238,7 +275,7 @@ lft (kit vr tm wk) Ï„ (vs x) = wk (Ï„ x)
 
 -- Traversal function --
 
-trav : {Δ Γ : Ctx Empty} {T : Ty Empty} {_◈_ : ProofT} (K : Kit _◈_)
+trav : {Δ Γ : TyCtx Empty} {T : Ty Empty} {_◈_ : ProofT} (K : Kit _◈_)
          (τ : Subst Δ Γ _◈_) (t : Tm Ext Γ T) -> Tm Ext Δ T
 trav (kit vr tm wk) Ï„ (var x) = tm (Ï„ x)
 trav K Ï„ (lda t') = (lda (trav K (lft K Ï„) t'))
diff --git a/formalizations/guarded-cubical/Syntax/Types.agda b/formalizations/guarded-cubical/Syntax/Types.agda
index 610c547..50648ec 100644
--- a/formalizations/guarded-cubical/Syntax/Types.agda
+++ b/formalizations/guarded-cubical/Syntax/Types.agda
@@ -10,14 +10,10 @@ open import Common.Later hiding (next)
 module Syntax.Types  where
 
 open import Cubical.Foundations.Prelude renaming (comp to compose)
-open import Cubical.Data.Nat hiding (_·_) renaming (ℕ to Nat)
+open import Cubical.Data.Nat
 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
-  using (List ; length ; map ; _++_ ; cons-inj₁ ; cons-inj₂)
-  renaming ([] to · ; _∷_ to _::_)
 open import Cubical.Data.Empty renaming (rec to exFalso)
 
 open import Syntax.Context as Context
@@ -36,10 +32,12 @@ data iCtx : Type where
   Empty : iCtx
   Full : iCtx
 
+endpt-fun : ∀ {ℓ} → (iCtx → Type ℓ) → Type ℓ
+endpt-fun {ℓ} A = Interval → A Full → A Empty
 
 data Ty : iCtx -> Type
 
-ty-endpt : Interval -> Ty Full -> Ty Empty
+ty-endpt : endpt-fun Ty
 
 _⊑_ : Ty Empty -> Ty Empty -> Type
 A ⊑ B = Σ[ c ∈ Ty Full ] ((ty-endpt l c ≡ A) × (ty-endpt r c ≡ B))
@@ -108,7 +106,7 @@ TyCtx : iCtx → Type (ℓ-suc ℓ-zero)
 TyCtx Ξ = Ctx (Ty Ξ)
 
 -- Endpoints of a full context
-ctx-endpt : (p : Interval) -> TyCtx Full -> TyCtx Empty
+ctx-endpt : endpt-fun TyCtx
 ctx-endpt p = Context.map (ty-endpt p)
 
 CompCtx : (Δ Γ : TyCtx Full)
@@ -143,5 +141,3 @@ ctx-refl = Context.map ty-refl
 -- context are the typing context itself.
 ctx-endpt-refl : {Γ : TyCtx Empty} -> (p : Interval) -> ctx-endpt p (ctx-refl Γ) ≡ Γ
 ctx-endpt-refl {Γ} p = Ctx≡ _ _ refl (funExt λ x → ty-endpt-refl {A = Γ .el x} p)
-
-
-- 
GitLab