From a010b77bf800a4e4e3748fa6e40fa5afeff43163 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 3 Oct 2023 11:55:57 -0400
Subject: [PATCH] Remove outdated syntax files

---
 .../Syntax/DeBruijnCommon.agda                | 228 -------------
 .../guarded-cubical/Syntax/Displayed.agda     | 256 ---------------
 .../guarded-cubical/Syntax/ExplicitSubst.agda | 241 --------------
 .../guarded-cubical/Syntax/Extensional.agda   |  89 -----
 .../guarded-cubical/Syntax/GSTLC.agda         | 278 ----------------
 .../guarded-cubical/Syntax/GSTLCCollapse.agda |  66 ----
 .../guarded-cubical/Syntax/Intensional.agda   | 266 ---------------
 .../guarded-cubical/Syntax/SyntaxNew.agda     | 307 ------------------
 8 files changed, 1731 deletions(-)
 delete mode 100644 formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda
 delete mode 100644 formalizations/guarded-cubical/Syntax/Displayed.agda
 delete mode 100644 formalizations/guarded-cubical/Syntax/ExplicitSubst.agda
 delete mode 100644 formalizations/guarded-cubical/Syntax/Extensional.agda
 delete mode 100644 formalizations/guarded-cubical/Syntax/GSTLC.agda
 delete mode 100644 formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda
 delete mode 100644 formalizations/guarded-cubical/Syntax/Intensional.agda
 delete mode 100644 formalizations/guarded-cubical/Syntax/SyntaxNew.agda

diff --git a/formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda b/formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda
deleted file mode 100644
index 21950d7..0000000
--- a/formalizations/guarded-cubical/Syntax/DeBruijnCommon.agda
+++ /dev/null
@@ -1,228 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded #-}
-
-open import Cubical.Foundations.Prelude
-
-
-module Syntax.DeBruijnCommon
-  (Ty : Type)
-  (Ctx : Type)
-  ( · : Ctx)
-  (_::_ : Ctx -> Ty -> Ctx)
-  (let infixr 5 _::_ ; _::_ = _::_)
-  (_∋_ : Ctx -> Ty -> Type)
-  (let infixr 4 _∋_ ; _∋_ = _∋_)
-  (vz : ∀ {Γ S} -> Γ :: S ∋ S)
-  (vs : ∀ {Γ S T} (x : Γ ∋ T) -> (Γ :: S ∋ T))
-  (Tm : Ctx -> Ty -> Type)
-  where
-
-
-
-open import Cubical.Data.Nat
-open import Cubical.Relation.Nullary
-
--- Types --
-
-{-
-data Ty : Set where
-  nat : Ty
-  dyn : Ty
-  _=>_ : Ty -> Ty -> Ty
-
-infixr 5 _=>_
-
-data _⊑_ : Ty -> Ty -> Set where
-  dyn : dyn ⊑ dyn
-  _=>_ : {A A' B B' : Ty} ->
-    A ⊑ A' -> B ⊑ B' -> (A => B) ⊑ (A' => B')
-  nat : nat ⊑ nat
-  inj-nat : nat ⊑ dyn
-  inj-arrow : {A : Ty} ->
-    A ⊑ (dyn => dyn) -> A ⊑ dyn
-  -- inj-arrow : {A A' : Ty} ->
-  --   (A => A') ⊑ (dyn => dyn) -> (A => A') ⊑ dyn
-  
-  -- inj-arrow could be made more compositional by having a
-  -- case for composition of EP pairs and a case for
-  -- dyn => dyn ⊑ dyn
-
-⊑ref : (A : Ty) -> A ⊑ A
-⊑ref nat = nat
-⊑ref dyn = dyn
-⊑ref (A1 => A2) = (⊑ref A1) => (⊑ref A2)
-
-⊑comp : {A B C : Ty} ->
-  A ⊑ B -> B ⊑ C -> A ⊑ C
-⊑comp dyn dyn = dyn
-⊑comp {Ai => Ao} {Bi => Bo} {Ci => Co} (cin => cout) (din => dout) =
-  (⊑comp cin din) => (⊑comp cout dout)
-⊑comp {Ai => Ao} {Bi => Bo} (cin => cout) (inj-arrow (cin' => cout')) =
-  inj-arrow ((⊑comp cin cin') => (⊑comp cout cout'))
-⊑comp nat nat = nat
-⊑comp nat inj-nat = inj-nat
-⊑comp inj-nat dyn = inj-nat
-⊑comp (inj-arrow c) dyn = inj-arrow c
-
-
-
-module ⊑-properties where
-  -- experiment with modules
-  ⊑-prop : ∀ A B → isProp (A ⊑ B)
-  ⊑-prop .dyn .dyn dyn dyn = refl
-  ⊑-prop .(_ => _) .(_ => _) (p1 => p3) (p2 => p4) = λ i → (⊑-prop _ _ p1 p2 i) => (⊑-prop _ _ p3 p4 i)
-  ⊑-prop .nat .nat nat nat = refl
-  ⊑-prop .nat .dyn inj-nat inj-nat = refl
-  ⊑-prop A .dyn (inj-arrow p1) (inj-arrow p2) = λ i → inj-arrow (⊑-prop _ _ p1 p2 i)
-
-  dyn-⊤ : ∀ A → A ⊑ dyn
-  dyn-⊤ nat = inj-nat
-  dyn-⊤ dyn = dyn
-  dyn-⊤ (A => B) = inj-arrow (dyn-⊤ A => dyn-⊤ B)
-
-  ⊑-dec : ∀ A B → Dec (A ⊑ B)
-  ⊑-dec A dyn = yes (dyn-⊤ A)
-  ⊑-dec nat nat = yes nat
-  ⊑-dec nat (B => B₁) = no (λ ())
-  ⊑-dec dyn nat = no (λ ())
-  ⊑-dec dyn (B => B₁) = no (λ ())
-  ⊑-dec (A => A₁) nat = no ((λ ()))
-  ⊑-dec (A => B) (A' => B') with (⊑-dec A A') | (⊑-dec B B')
-  ... | yes p | yes q = yes (p => q)
-  ... | yes p | no ¬p = no (refute ¬p)
-    where refute : ∀ {A A' B B'} → (¬ (B ⊑ B')) → ¬ ((A => B) ⊑ (A' => B'))
-          refute ¬p (_ => p) = ¬p p
-  ... | no ¬p | _ = no (refute ¬p)
-    where refute : ∀ {A A' B B'} → (¬ (A ⊑ A')) → ¬ ((A => B) ⊑ (A' => B'))
-          refute ¬p (p => _) = ¬p p
-    
-  
--- Contexts --
-
-data Ctx : Set where
-  · : Ctx
-  _::_ : Ctx -> Ty -> Ctx
-
-infixr 5 _::_
-
-
-
--- "Contains" relation stating that a context Γ contains a type T
-
-data _∋_ : Ctx -> Ty -> Set where
-  vz : ∀ {Γ S} -> Γ :: S ∋ S
-  vs : ∀ {Γ S T} (x : Γ ∋ T) -> (Γ :: S ∋ T)
-
-infix 4 _∋_
-
-
--- Simply-typed terms, presented via their typing rules
-
-data Tm : Ctx -> Ty -> Set where
-  var : ∀ {Γ T}   -> Γ ∋ T -> Tm Γ T
-  lda : ∀ {Γ S T} -> (Tm (Γ :: S) T) -> Tm Γ (S => T)
-  app : ∀ {Γ S T} -> (Tm Γ (S => T)) -> (Tm Γ S) -> (Tm Γ T)
-  err : ∀ {Γ A} -> Tm Γ A
-  up  : ∀ {Γ A B} -> A ⊑ B -> Tm Γ A -> Tm Γ B
-  dn  : ∀ {Γ A B} -> A ⊑ B -> Tm Γ B -> Tm Γ A
-  zro : ∀ {Γ} -> Tm Γ nat
-  suc : ∀ {Γ} -> Tm Γ nat -> Tm Γ nat
-
--- infix 4 _â–¸_
-
--}
-
-
---  ================================================================= --
-
-
--- Type of "proofs", i.e., relations between contexts and types --
-
-ProofT = Ctx -> Ty -> Set
-
-
--- Kits --
-
-VarToProof : ProofT -> Set
-VarToProof _◆_ = ∀ {Γ T} -> (Γ ∋ T) -> (Γ ◆ T)
--- The diamond is a function, and the underscores around it allow us to use it in infix
-
-ProofToTm : ProofT -> Set
-ProofToTm _◆_ = ∀ {Γ T} -> (Γ ◆ T) -> (Tm Γ T)
-
-WeakeningMap : ProofT -> Set
-WeakeningMap _◆_ = ∀ {Γ S T} -> (Γ ◆ T) -> ((Γ :: S) ◆ T)
-
-data Kit (â—† : ProofT) : Set where
-  kit : ∀ (vr : VarToProof ◆) (tm : ProofToTm ◆) (wk : WeakeningMap ◆) -> Kit ◆
-
-
--- Substitutions --
-
-Subst : Ctx -> Ctx -> ProofT -> Set
-Subst Δ Γ _◈_ = ∀ {T} -> (Γ ∋ T) -> (Δ ◈ T)
-
-
-module DeBruijn
-  (trav : {Δ Γ : Ctx} {T : Ty} {_◈_ : ProofT} (K : Kit _◈_)
-       (τ : Subst Δ Γ _◈_) (t : Tm Γ T) -> Tm Δ T)
-  (var : ∀ {Γ T}   -> Γ ∋ T -> Tm Γ T)
-    where
-
-
-
-  -- Lift function --
-
-{-
-lft : {Δ Γ : Ctx} {S : Ty} {_◈_ : ProofT}
-       (K : Kit _◈_) (τ : Subst Δ Γ _◈_) {T : Ty} (h : (Γ :: S) ∋ T) -> (Δ :: S) ◈ T       
-lft (kit vr tm wk) Ï„ vz = vr vz
-lft (kit vr tm wk) Ï„ (vs x) = wk (Ï„ x)
--}
-
--- Note that the type of lft can also be written as (Subst Δ Γ _◈_) -> (Subst (Δ ∷ S) (Γ ∷ S) _◈_)
-
-
-{-
--- Traversal function --
-
-trav : {Δ Γ : Ctx} {T : Ty} {_◈_ : ProofT} (K : Kit _◈_)
-       (τ : Subst Δ Γ _◈_) (t : Tm Γ T) -> Tm Δ T
-trav (kit vr tm wk) Ï„ (var x) = tm (Ï„ x)
-trav K Ï„ (lda t') = lda (trav K (lft K Ï„) t')
-trav K Ï„ (app f s) = app (trav K Ï„ f) (trav K Ï„ s)
-trav K Ï„ (up deriv t') = up deriv (trav K Ï„ t')
-trav K Ï„ (dn deriv t') = dn deriv (trav K Ï„ t')
-trav K Ï„ err = err
-trav K Ï„ zro = zro
-trav K Ï„ (suc t') = suc (trav K Ï„ t')
--}
-
-
-
-  -- Renaming --
-
-  idContains : {Γ : Ctx} {T : Ty} (t : Γ ∋ T) -> Γ ∋ T
-  idContains t = t
-
-  varKit : Kit _∋_
-  varKit = kit idContains var vs
-
-  rename : {Γ Δ : Ctx} {T : Ty} (ρ : Subst Δ Γ _∋_) (t : Tm Γ T) -> Tm Δ T
-  rename ρ t = trav varKit ρ t
-
-
-
-  -- Substitution --
-
-  idTerm : {Γ : Ctx} {T : Ty} (t : Tm Γ T) -> Tm Γ T
-  idTerm t = t
-
-  weakenTerm : WeakeningMap Tm
-  weakenTerm = rename vs
-
-  termKit : Kit Tm
-  termKit = kit var idTerm weakenTerm
-
-  sub : (Δ Γ : Ctx) (σ : Subst Δ Γ Tm) (T : Ty) (t : Tm Γ T) -> Tm Δ T
-  sub Δ Γ σ T t = trav termKit σ t
-
diff --git a/formalizations/guarded-cubical/Syntax/Displayed.agda b/formalizations/guarded-cubical/Syntax/Displayed.agda
deleted file mode 100644
index ad17703..0000000
--- a/formalizations/guarded-cubical/Syntax/Displayed.agda
+++ /dev/null
@@ -1,256 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded -W noUnsupportedIndexedMatch #-}
-
- -- to allow opening this module in other files while there are still holes
-{-# OPTIONS --allow-unsolved-metas #-}
-{-# OPTIONS --lossy-unification #-}
-
-
-open import Common.Later hiding (next)
-
-module Syntax.Displayed  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
-  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 hiding (Renaming)
--- import Syntax.DeBruijnCommon
-
-private
- variable
-   â„“ â„“' â„“'' : Level
-
-open import Syntax.Types
-open Ctx
-
-SynType = Ty Empty
-TyPrec = Ty Full
-
-TypeCtx = TyCtx Empty
-PrecCtx = TyCtx Full
-
--- A renaming is a mapping of names that preserves the typing
-Renaming = Context.Renaming {A = SynType}
-
-wk-ren : ∀ {Γ Δ T} → Renaming Γ Δ → Renaming (cons Γ T) (cons Δ T)
-wk-ren ρ (inl x) .fst = inl (ρ x .fst)
-wk-ren ρ (inl x) .snd = ρ x .snd
-wk-ren ρ (inr x) .fst = inr x
-wk-ren ρ (inr x) .snd = refl
-
--- Values, Computations and Evaluation contexts,
--- quotiented by βη equivalence but *not* by order equivalence (i.e., up/dn laws)
-data Val : (Γ : TypeCtx) (A : SynType) → Type (ℓ-suc ℓ-zero)
-data Comp : (Γ : TypeCtx) (A : SynType) → Type (ℓ-suc ℓ-zero)
-data EvCtx : (Γ : TypeCtx) (A : SynType) (B : SynType) → Type (ℓ-suc ℓ-zero)
-
-Substitution : TypeCtx → TypeCtx → Type _
-Substitution Δ Γ = substitution (Val Δ) Γ
-
-cons-Subst : ∀ {Δ Γ S} → Substitution Δ Γ → Val Δ S → Substitution Δ (cons Γ S)
-cons-Subst {Δ} γ V = cons-subst (Val Δ) γ V
-
-idSubst : ∀ Γ → Substitution Γ Γ
-compSubst : ∀ {Γ Δ Ξ} → Substitution Δ Ξ → Substitution Γ Δ → Substitution Γ Ξ
-renToSubst : ∀ {Γ Δ} → Renaming Γ Δ → Substitution Γ Δ
-
-app' : ∀ {Γ S T} → Val Γ (S ⇀ T) → Val Γ S → Comp Γ T
-varV' : ∀ {Γ} → (x : Γ .var) → Val Γ (Γ .el x)
-
-_[_]vr : ∀ {Δ Γ A}
-  → Val Γ A
-  → Renaming Δ Γ
-  → Val Δ A
-
-_[_]cr : ∀ {Δ Γ A}
-  → Comp Γ A
-  → Renaming Δ Γ
-  → Comp Δ A
-
-_[_]er : ∀ {Δ Γ A B}
-  → EvCtx Γ A B
-  → Renaming Δ Γ
-  → EvCtx Δ A B
-
-ρWk : ∀ {Γ A} -> Renaming (cons Γ A) Γ
-ρWk x = inl x , refl
-wkV : ∀ {Γ A B} -> Val Γ A -> Val (cons Γ B) A
-wkV v = v [ ρWk ]vr
-wkC : ∀ {Γ A B} -> Comp Γ A -> Comp (cons Γ B) A
-wkC M = M [ ρWk ]cr
-wkE : ∀ {Γ A B C} -> EvCtx Γ A B -> EvCtx (cons Γ C) A B
-wkE E = E [ ρWk ]er
-wkS : ∀ {Γ Δ S} → Substitution Γ Δ → Substitution (cons Γ S) Δ
-wkS {Γ} {Δ} {S} γ x = wkV (γ x)
-
-_[_]v : ∀ {Δ Γ A}
-  → Val Γ A
-  → Substitution Δ Γ
-  → Val Δ A
-_[_]c : ∀ {Δ Γ A}
-  → Comp Γ A
-  → Substitution Δ Γ
-  → Comp Δ A
-_[_]c1 : ∀ {Γ A B}
-  → Comp (cons Γ A) B
-  → (Val Γ A)
-  → Comp Γ B
-
-_[_]eγ : ∀ {Δ Γ A B}
-  → EvCtx Γ A B
-  → Substitution Δ Γ
-  → EvCtx Δ A B
-_[_]e1 : ∀ {Γ A B C}
-  → EvCtx (cons Γ A) B C
-  → (Val Γ A)
-  → EvCtx Γ B C
-
--- Should there be a single combined plug and chug operations?
-_[_]e∙ : ∀ {Γ A B}
-  → EvCtx Γ A B
-  → Comp Γ A
-  → Comp Γ B
-
-data Val where
-  -- a way to avoid "green slime" in McBride's terminology
-  varV : ∀ {Γ A} → (x : Γ .var) → (Γ .el x ≡ A) → Val Γ A
-  lda : ∀ {Γ S T} -> (Comp (cons Γ S) T) -> Val Γ (S ⇀ T)
-  zro : ∀ {Γ} -> Val Γ nat
-  suc : ∀ {Γ} -> Val Γ nat -> Val Γ nat
-  up : ∀ {Γ} -> (S⊑T : TyPrec) -> Val Γ (ty-left S⊑T) -> Val Γ (ty-right S⊑T)
-  -- as written the following rule is not stable under renaming, or is it?
-  ⇀-ext : ∀ {Γ A B} (Vf Vf' : Val Γ (A ⇀ B))
-    → app' (wkV Vf) (varV' (inr _)) ≡ app' (wkV Vf') (varV' (inr _))
-    → Vf ≡ Vf'
-  -- | Should we make these admissible or postulate them?
-  -- ren≡ : ∀ {Δ Γ S} → (ρ : Renaming Δ Γ) (V V' : Val Γ S)
-  --        → V ≡ V' → _[_]vr {Δ}{Γ} V ρ ≡ V' [ ρ ]vr
-  -- subst≡ : ∀ {Δ Γ S} → (γ : Substitution Δ Γ) (V V' : Val Γ S)
-  --        → V ≡ V' → V [ γ ]v ≡ V' [ γ ]v
-  isSetVal : ∀ {Γ S} → isSet (Val Γ S)
-data Comp where
-  err : ∀ {Γ S} → Comp Γ S
-  ret : ∀ {Γ S} → Val Γ S → Comp Γ S
-  bind : ∀ {Γ S T} → Comp Γ S → Comp (cons Γ S) T → Comp Γ T
-  app : ∀ {Γ S T} → Val Γ (S ⇀ T) → Val Γ S → Comp Γ T
-  matchNat : ∀ {Γ S} → Val Γ nat → Comp Γ S → Comp (cons Γ nat) S → Comp Γ S
-  dn : ∀ {Γ} → (S⊑T : TyPrec) → Comp Γ (ty-right S⊑T) → Comp Γ (ty-left S⊑T)
-
-  -- Strictness of all evaluation contexts
-  strictness : ∀ {Γ S T} → (E : EvCtx Γ S T) → E [ err ]e∙ ≡ err
-  ret-β : ∀ {Γ S T} → (V : Val Γ S) → (K : Comp (cons Γ S) T) → bind (ret V) K ≡ K [ V ]c1
-  fun-β : ∀ {Γ S T} → (M : Comp (cons Γ S) T) → (V : Val Γ S) → app (lda M) V ≡ M [ V ]c1
-  nat-βz : ∀ {Γ S} → (Kz : Comp Γ S) (Ks : Comp (cons Γ nat) S) → matchNat zro Kz Ks ≡ Kz
-  nat-βs : ∀ {Γ S} → (V : Val Γ nat) (Kz : Comp Γ S) (Ks : Comp (cons Γ nat) S) → matchNat (suc V) Kz Ks ≡ Ks [ V ]c1
-  -- η for matchNat
-  -- some notation would probably help here...
-  nat-η : ∀ {Γ S} → (M : Comp (cons Γ nat) S)
-          → M ≡
-            (matchNat (varV' (inr _))
-                      (M [ cons-subst (Val (cons Γ nat)) (λ x → varV' (inl x)) zro ]c)
-                      (M [ cons-subst ((Val (cons (cons Γ nat) nat))) (λ x → varV' (inl (inl x))) (suc (varV' (inr _))) ]c))
-  -- this allows cong wrt plugging be admissible
-  ret-η : ∀ {Γ S T} → (E : EvCtx Γ S T) (M : Comp Γ S) → E [ M ]e∙ ≡ bind M (wkE E [ ret (varV' (inr _)) ]e∙)
-  isSetComp : ∀ {Γ A} → isSet (Comp Γ A)
-
-data EvCtx where
-  ∙E : ∀ {Γ S} → EvCtx Γ S S
-  bind : ∀ {Γ S T U} → EvCtx Γ S T → Comp (cons Γ T) U → EvCtx Γ S U
-  dn : ∀ {Γ} (S⊑T : TyPrec) {U} → EvCtx Γ U (ty-right S⊑T) → EvCtx Γ U (ty-left S⊑T)
-
-  ret-η : ∀ {Γ S T} → (E : EvCtx Γ S T) → E ≡ bind ∙E (wkE E [ ret (varV' (inr _)) ]e∙)
-  isSetEvCtx : ∀ {Γ A B} → isSet (EvCtx Γ A B)
-
-varV' x = varV x refl
-app' = app
-idSubst Γ = varV'
-compSubst δ γ x = δ x [ γ ]v
-renToSubst ρ x = varV (ρ x .fst) (ρ x .snd)
-
-_[_]c1 {Γ} M V = M [ cons-subst (Val Γ) varV' V ]c
-_[_]e1 {Γ} E V = E [ cons-subst (Val Γ) varV' V ]eγ
-
-_[_]vr {Γ}{Δ} (varV x p) ρ = varV (ρ x .fst) (ρ x .snd ∙ p)
-_[_]vr {Γ}{Δ} (lda {S}{T} M) ρ = lda (M [ wk-ren ρ ]cr)
-zro [ ρ ]vr = zro
-suc V [ ρ ]vr = suc (V [ ρ ]vr)
-up S⊑T V [ ρ ]vr = up S⊑T (V [ ρ ]vr)
-⇀-ext V V' x i [ ρ ]vr = {!!} -- needs equivariance of renaming to prove
--- _[_]vr {Γ}{Δ} (ren≡ {Δ} ρ' V V' p i) ρ = ren≡ {Γ}{Δ} ρ (V [ ρ' ]vr) (V' [ ρ' ]vr) (ren≡ ρ' V V' p) i
-isSetVal V V' x y i j [ ρ ]vr = isSetVal (V [ ρ ]vr) (V' [ ρ ]vr) (λ i → x i [ ρ ]vr) ((λ i → y i [ ρ ]vr)) i j
-
-err [ ρ ]cr = err
-ret V [ ρ ]cr = ret (V [ ρ ]vr)
-bind M K [ ρ ]cr = bind (M [ ρ ]cr) (K [ wk-ren ρ ]cr)
-app V V' [ ρ ]cr = app (V [ ρ ]vr) (V' [ ρ ]vr)
-matchNat V Kz Ks [ ρ ]cr = matchNat (V [ ρ ]vr) (Kz [ ρ ]cr) (Ks [ wk-ren ρ ]cr)
-dn S⊑T M [ ρ ]cr = dn S⊑T (M [ ρ ]cr)
--- rest are tedious but straightforward
-strictness E i [ ρ ]cr = {!!}
-ret-β V M i [ ρ ]cr = {!!}
-fun-β M V i [ ρ ]cr = {!!}
-nat-βz M M₁ i [ ρ ]cr = {!!}
-nat-βs V M M₁ i [ ρ ]cr = {!!}
-nat-η M i [ ρ ]cr = {!!}
-ret-η E M i [ ρ ]cr = {!!}
-isSetComp M M' p q i j [ ρ ]cr = isSetComp (M [ ρ ]cr) (M' [ ρ ]cr) ((cong (_[ ρ ]cr)) p) ((cong (_[ ρ ]cr)) q) i j
-
-∙E [ ρ ]er = ∙E
-bind E K [ ρ ]er = bind (E [ ρ ]er) (K [ wk-ren ρ ]cr)
-dn S⊑T E [ ρ ]er = dn S⊑T (E [ ρ ]er)
-ret-η E i [ ρ ]er = {!!}
-isSetEvCtx E E' p q i j [ ρ ]er = isSetEvCtx (E [ ρ ]er) (E' [ ρ ]er) (λ i → p i [ ρ ]er) ((λ i → q i [ ρ ]er)) i j
-
-_[_]v {Δ} (varV x p) γ = transport (cong (Val Δ) p) (γ x)
-_[_]v {Δ}{Γ} (lda M) γ = lda (M [ cons-Subst (wkS {Δ}{Γ} γ) (varV' (inr _)) ]c)
-zro [ γ ]v = zro
-suc V [ γ ]v = suc (V [ γ ]v)
-up S⊑T V [ γ ]v = up S⊑T (V [ γ ]v)
-⇀-ext V V₁ x i [ γ ]v = {!!}
-isSetVal V V₁ x y i i₁ [ γ ]v = {!!}
-
-err [ γ ]c = err
-ret V [ γ ]c = ret (V [ γ ]v)
-bind M K [ γ ]c = bind (M [ γ ]c) {!K [ cons-Subst (wkS {Δ}{Γ} γ) (varV' (inr _)) ]c!}
-app Vf Va [ γ ]c = app (Vf [ γ ]v) (Va [ γ ]v)
-matchNat V Kz Ks [ γ ]c = matchNat (V [ γ ]v) (Kz [ γ ]c) {!!}
-dn S⊑T M [ γ ]c = dn S⊑T (M [ γ ]c)
-strictness E i [ γ ]c = {!!}
-ret-β V M i [ γ ]c = {!!}
-fun-β M V i [ γ ]c = {!!}
-nat-βz M M₁ i [ γ ]c = {!!}
-nat-βs V M M₁ i [ γ ]c = {!!}
-nat-η M i [ γ ]c = {!!}
-ret-η E M i [ γ ]c = {!!}
-isSetComp M M' p q i j [ γ ]c = {!!}
-
-∙E [ γ ]eγ = ∙E
-bind E M [ γ ]eγ = bind (E [ γ ]eγ) {!!}
-dn S⊑T E [ γ ]eγ = dn S⊑T (E [ γ ]eγ)
-ret-η E i [ γ ]eγ = {!!}
-isSetEvCtx E E' p q i j [ γ ]eγ = {!!}
-
-∙E [ M ]e∙ = M
-bind E K [ M ]e∙ = bind (E [ M ]e∙) K
-dn S⊑T E [ M ]e∙ = dn S⊑T (E [ M ]e∙)
-ret-η E i [ M ]e∙ = ret-η E M i
-isSetEvCtx E E' p q i j [ M ]e∙ = isSetComp (E [ M ]e∙) (E' [ M ]e∙) (λ i → p i [ M ]e∙) ((λ i → q i [ M ]e∙)) i j
-
-data ValPrec : (Γ : PrecCtx) (A : TyPrec) (V : Val (ctx-endpt l Γ) (ty-endpt l A)) (V' : Val (ctx-endpt r Γ) (ty-endpt r A)) → Type (ℓ-suc ℓ-zero)
-data CompPrec : (Γ : PrecCtx) (A : TyPrec) (M : Comp (ctx-endpt l Γ) (ty-endpt l A)) (M' : Comp (ctx-endpt r Γ) (ty-endpt r A)) → Type (ℓ-suc ℓ-zero)
-data EvCtxPrec : (Γ : PrecCtx) (A : TyPrec) (B : TyPrec) (E : EvCtx (ctx-endpt l Γ) (ty-endpt l A) (ty-endpt l B)) (E' : EvCtx (ctx-endpt r Γ) (ty-endpt r A) (ty-endpt r B)) → Type (ℓ-suc ℓ-zero)
-
-data ValPrec where
-data CompPrec where
-data EvCtxPrec where
-
-
diff --git a/formalizations/guarded-cubical/Syntax/ExplicitSubst.agda b/formalizations/guarded-cubical/Syntax/ExplicitSubst.agda
deleted file mode 100644
index 785d4b7..0000000
--- a/formalizations/guarded-cubical/Syntax/ExplicitSubst.agda
+++ /dev/null
@@ -1,241 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded -W noUnsupportedIndexedMatch #-}
-
- -- to allow opening this module in other files while there are still holes
-{-# OPTIONS --allow-unsolved-metas #-}
-{-# OPTIONS --lossy-unification #-}
-
-
-module Syntax.ExplicitSubst  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
-  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 hiding (Renaming)
--- import Syntax.DeBruijnCommon
-
-private
- variable
-   â„“ â„“' â„“'' : Level
-
-open import Syntax.Types
-open Ctx
-
-SynType = Ty Empty
-TyPrec = Ty Full
-
-TypeCtx = TyCtx Empty
-PrecCtx = TyCtx Full
-
--- Values, Computations and Evaluation contexts,
--- quotiented by βη equivalence but *not* by order equivalence (i.e., up/dn laws)
-data Subst : (Δ : TypeCtx) (Γ : TypeCtx) → Type (ℓ-suc ℓ-zero)
-data Val : (Γ : TypeCtx) (A : SynType) → Type (ℓ-suc ℓ-zero)
-data Comp : (Γ : TypeCtx) (A : SynType) → Type (ℓ-suc ℓ-zero)
-data EvCtx : (Γ : TypeCtx) (A : SynType) (B : SynType) → Type (ℓ-suc ℓ-zero)
-
--- idSubst : ∀ Γ → Substitution Γ Γ
--- compSubst : ∀ {Γ Δ Ξ} → Substitution Δ Ξ → Substitution Γ Δ → Substitution Γ Ξ
-
--- app' : ∀ {Γ S T} → Val Γ (S ⇀ T) → Val Γ S → Comp Γ T
--- varV' : ∀ {Γ} → (x : Γ .var) → Val Γ (Γ .el x)
-
--- _[_]cr : ∀ {Δ Γ A}
---   → Comp Γ A
---   → Renaming Δ Γ
---   → Comp Δ A
-
--- _[_]er : ∀ {Δ Γ A B}
---   → EvCtx Γ A B
---   → Renaming Δ Γ
---   → EvCtx Δ A B
-
--- ρWk : ∀ {Γ A} -> Renaming (cons Γ A) Γ
--- ρWk x = inl x , refl
--- wkV : ∀ {Γ A B} -> Val Γ A -> Val (cons Γ B) A
--- wkV v = v [ ρWk ]vr
--- wkC : ∀ {Γ A B} -> Comp Γ A -> Comp (cons Γ B) A
--- wkC M = M [ ρWk ]cr
--- wkE : ∀ {Γ A B C} -> EvCtx Γ A B -> EvCtx (cons Γ C) A B
--- wkE E = E [ ρWk ]er
--- wkS : ∀ {Γ Δ S} → Substitution Γ Δ → Substitution (cons Γ S) Δ
--- wkS {Γ} {Δ} {S} γ x = wkV (γ x)
-
--- _[_]v : ∀ {Δ Γ A}
---   → Val Γ A
---   → Substitution Δ Γ
---   → Val Δ A
--- _[_]c : ∀ {Δ Γ A}
---   → Comp Γ A
---   → Substitution Δ Γ
---   → Comp Δ A
--- _[_]c1 : ∀ {Γ A B}
---   → Comp (cons Γ A) B
---   → (Val Γ A)
---   → Comp Γ B
-
--- _[_]eγ : ∀ {Δ Γ A B}
---   → EvCtx Γ A B
---   → Substitution Δ Γ
---   → EvCtx Δ A B
--- _[_]e1 : ∀ {Γ A B C}
---   → EvCtx (cons Γ A) B C
---   → (Val Γ A)
---   → EvCtx Γ B C
-
--- -- Should there be a single combined plug and chug operations?
--- _[_]e∙ : ∀ {Γ A B}
---   → EvCtx Γ A B
---   → Comp Γ A
---   → Comp Γ B
-data Subst where
-  ids : ∀ {Γ} → Subst Γ Γ
-  _∘s_ : ∀ {Γ Δ Θ} → Subst Δ Θ → Subst Γ Δ → Subst Γ Θ
-  _/x : ∀ {Γ S} → Val Γ S → Subst Γ (singleton S)
-
-data Val where
-  -- a way to avoid "green slime" in McBride's terminology
-  varV : ∀ {Γ A} → (x : Γ .var) → (Γ .el x ≡ A) → Val Γ A
-  lda : ∀ {Γ S T} -> (Comp (cons Γ S) T) -> Val Γ (S ⇀ T)
-  zro : ∀ {Γ} -> Val Γ nat
-  suc : ∀ {Γ} -> Val Γ nat -> Val Γ nat
-  up : ∀ {Γ} -> (S⊑T : TyPrec) -> Val Γ (ty-left S⊑T) -> Val Γ (ty-right S⊑T)
-
-  _[_] : ∀ {Δ Γ S} → Val Γ S → Subst Δ Γ → Val Δ S
-  -- as written the following rule is not stable under renaming, or is it?
-  -- ⇀-ext : ∀ {Γ A B} (Vf Vf' : Val Γ (A ⇀ B))
-  --   → app' (wkV Vf) (varV' (inr _)) ≡ app' (wkV Vf') (varV' (inr _))
-  --   → Vf ≡ Vf'
-  -- | Should we make these admissible or postulate them?
-  -- ren≡ : ∀ {Δ Γ S} → (ρ : Renaming Δ Γ) (V V' : Val Γ S)
-  --        → V ≡ V' → _[_]vr {Δ}{Γ} V ρ ≡ V' [ ρ ]vr
-  -- subst≡ : ∀ {Δ Γ S} → (γ : Substitution Δ Γ) (V V' : Val Γ S)
-  --        → V ≡ V' → V [ γ ]v ≡ V' [ γ ]v
-  isSetVal : ∀ {Γ S} → isSet (Val Γ S)
-
-data Comp where
-  err : ∀ {Γ S} → Comp Γ S
-  ret : ∀ {Γ S} → Val Γ S → Comp Γ S
-  bind : ∀ {Γ S T} → Comp Γ S → Comp (cons Γ S) T → Comp Γ T
-  app : ∀ {Γ S T} → Val Γ (S ⇀ T) → Val Γ S → Comp Γ T
-  matchNat : ∀ {Γ S} → Val Γ nat → Comp Γ S → Comp (cons Γ nat) S → Comp Γ S
-  dn : ∀ {Γ} → (S⊑T : TyPrec) → Comp Γ (ty-right S⊑T) → Comp Γ (ty-left S⊑T)
-
-  -- Strictness of all evaluation contexts
-  -- strictness : ∀ {Γ S T} → (E : EvCtx Γ S T) → E [ err ]e∙ ≡ err
-  -- ret-β : ∀ {Γ S T} → (V : Val Γ S) → (K : Comp (cons Γ S) T) → bind (ret V) K ≡ K [ V ]c1
-  -- fun-β : ∀ {Γ S T} → (M : Comp (cons Γ S) T) → (V : Val Γ S) → app (lda M) V ≡ M [ V ]c1
-  nat-βz : ∀ {Γ S} → (Kz : Comp Γ S) (Ks : Comp (cons Γ nat) S) → matchNat zro Kz Ks ≡ Kz
-  -- nat-βs : ∀ {Γ S} → (V : Val Γ nat) (Kz : Comp Γ S) (Ks : Comp (cons Γ nat) S) → matchNat (suc V) Kz Ks ≡ Ks [ V ]c1
-  -- η for matchNat
-  -- some notation would probably help here...
-  -- nat-η : ∀ {Γ S} → (M : Comp (cons Γ nat) S)
-  --         → M ≡
-  --           (matchNat (varV' (inr _))
-  --                     (M [ cons-subst (Val (cons Γ nat)) (λ x → varV' (inl x)) zro ]c)
-  --                     (M [ cons-subst ((Val (cons (cons Γ nat) nat))) (λ x → varV' (inl (inl x))) (suc (varV' (inr _))) ]c))
-  -- this allows cong wrt plugging be admissible
-  -- ret-η : ∀ {Γ S T} → (E : EvCtx Γ S T) (M : Comp Γ S) → E [ M ]e∙ ≡ bind M (wkE E [ ret (varV' (inr _)) ]e∙)
-  isSetComp : ∀ {Γ A} → isSet (Comp Γ A)
-
-data EvCtx where
-  ∙E : ∀ {Γ S} → EvCtx Γ S S
-  bind : ∀ {Γ S T U} → EvCtx Γ S T → Comp (cons Γ T) U → EvCtx Γ S U
-  dn : ∀ {Γ} (S⊑T : TyPrec) {U} → EvCtx Γ U (ty-right S⊑T) → EvCtx Γ U (ty-left S⊑T)
-
-  -- ret-η : ∀ {Γ S T} → (E : EvCtx Γ S T) → E ≡ bind ∙E (wkE E [ ret (varV' (inr _)) ]e∙)
-  isSetEvCtx : ∀ {Γ A B} → isSet (EvCtx Γ A B)
-
--- varV' x = varV x refl
--- app' = app
--- idSubst Γ = varV'
--- compSubst δ γ x = δ x [ γ ]v
--- renToSubst ρ x = varV (ρ x .fst) (ρ x .snd)
-
--- _[_]c1 {Γ} M V = M [ cons-subst (Val Γ) varV' V ]c
--- _[_]e1 {Γ} E V = E [ cons-subst (Val Γ) varV' V ]eγ
-
--- _[_]vr {Γ}{Δ} (varV x p) ρ = varV (ρ x .fst) (ρ x .snd ∙ p)
--- _[_]vr {Γ}{Δ} (lda {S}{T} M) ρ = lda (M [ wk-ren ρ ]cr)
--- zro [ ρ ]vr = zro
--- suc V [ ρ ]vr = suc (V [ ρ ]vr)
--- up S⊑T V [ ρ ]vr = up S⊑T (V [ ρ ]vr)
--- ⇀-ext V V' x i [ ρ ]vr = {!!} -- needs equivariance of renaming to prove
--- -- _[_]vr {Γ}{Δ} (ren≡ {Δ} ρ' V V' p i) ρ = ren≡ {Γ}{Δ} ρ (V [ ρ' ]vr) (V' [ ρ' ]vr) (ren≡ ρ' V V' p) i
--- isSetVal V V' x y i j [ ρ ]vr = isSetVal (V [ ρ ]vr) (V' [ ρ ]vr) (λ i → x i [ ρ ]vr) ((λ i → y i [ ρ ]vr)) i j
-
--- err [ ρ ]cr = err
--- ret V [ ρ ]cr = ret (V [ ρ ]vr)
--- bind M K [ ρ ]cr = bind (M [ ρ ]cr) (K [ wk-ren ρ ]cr)
--- app V V' [ ρ ]cr = app (V [ ρ ]vr) (V' [ ρ ]vr)
--- matchNat V Kz Ks [ ρ ]cr = matchNat (V [ ρ ]vr) (Kz [ ρ ]cr) (Ks [ wk-ren ρ ]cr)
--- dn S⊑T M [ ρ ]cr = dn S⊑T (M [ ρ ]cr)
--- -- rest are tedious but straightforward
--- strictness E i [ ρ ]cr = {!!}
--- ret-β V M i [ ρ ]cr = {!!}
--- fun-β M V i [ ρ ]cr = {!!}
--- nat-βz M M₁ i [ ρ ]cr = {!!}
--- nat-βs V M M₁ i [ ρ ]cr = {!!}
--- nat-η M i [ ρ ]cr = {!!}
--- ret-η E M i [ ρ ]cr = {!!}
--- isSetComp M M' p q i j [ ρ ]cr = isSetComp (M [ ρ ]cr) (M' [ ρ ]cr) ((cong (_[ ρ ]cr)) p) ((cong (_[ ρ ]cr)) q) i j
-
--- ∙E [ ρ ]er = ∙E
--- bind E K [ ρ ]er = bind (E [ ρ ]er) (K [ wk-ren ρ ]cr)
--- dn S⊑T E [ ρ ]er = dn S⊑T (E [ ρ ]er)
--- ret-η E i [ ρ ]er = {!!}
--- isSetEvCtx E E' p q i j [ ρ ]er = isSetEvCtx (E [ ρ ]er) (E' [ ρ ]er) (λ i → p i [ ρ ]er) ((λ i → q i [ ρ ]er)) i j
-
--- _[_]v {Δ} (varV x p) γ = transport (cong (Val Δ) p) (γ x)
--- _[_]v {Δ}{Γ} (lda M) γ = lda (M [ cons-Subst (wkS {Δ}{Γ} γ) (varV' (inr _)) ]c)
--- zro [ γ ]v = zro
--- suc V [ γ ]v = suc (V [ γ ]v)
--- up S⊑T V [ γ ]v = up S⊑T (V [ γ ]v)
--- ⇀-ext V V₁ x i [ γ ]v = {!!}
--- isSetVal V V₁ x y i i₁ [ γ ]v = {!!}
-
--- err [ γ ]c = err
--- ret V [ γ ]c = ret (V [ γ ]v)
--- bind M K [ γ ]c = bind (M [ γ ]c) {!K [ cons-Subst (wkS {Δ}{Γ} γ) (varV' (inr _)) ]c!}
--- app Vf Va [ γ ]c = app (Vf [ γ ]v) (Va [ γ ]v)
--- matchNat V Kz Ks [ γ ]c = matchNat (V [ γ ]v) (Kz [ γ ]c) {!!}
--- dn S⊑T M [ γ ]c = dn S⊑T (M [ γ ]c)
--- strictness E i [ γ ]c = {!!}
--- ret-β V M i [ γ ]c = {!!}
--- fun-β M V i [ γ ]c = {!!}
--- nat-βz M M₁ i [ γ ]c = {!!}
--- nat-βs V M M₁ i [ γ ]c = {!!}
--- nat-η M i [ γ ]c = {!!}
--- ret-η E M i [ γ ]c = {!!}
--- isSetComp M M' p q i j [ γ ]c = {!!}
-
--- ∙E [ γ ]eγ = ∙E
--- bind E M [ γ ]eγ = bind (E [ γ ]eγ) {!!}
--- dn S⊑T E [ γ ]eγ = dn S⊑T (E [ γ ]eγ)
--- ret-η E i [ γ ]eγ = {!!}
--- isSetEvCtx E E' p q i j [ γ ]eγ = {!!}
-
--- ∙E [ M ]e∙ = M
--- bind E K [ M ]e∙ = bind (E [ M ]e∙) K
--- dn S⊑T E [ M ]e∙ = dn S⊑T (E [ M ]e∙)
--- ret-η E i [ M ]e∙ = ret-η E M i
--- isSetEvCtx E E' p q i j [ M ]e∙ = isSetComp (E [ M ]e∙) (E' [ M ]e∙) (λ i → p i [ M ]e∙) ((λ i → q i [ M ]e∙)) i j
-
-data ValPrec : (Γ : PrecCtx) (A : TyPrec) (V : Val (ctx-endpt l Γ) (ty-endpt l A)) (V' : Val (ctx-endpt r Γ) (ty-endpt r A)) → Type (ℓ-suc ℓ-zero)
-data CompPrec : (Γ : PrecCtx) (A : TyPrec) (M : Comp (ctx-endpt l Γ) (ty-endpt l A)) (M' : Comp (ctx-endpt r Γ) (ty-endpt r A)) → Type (ℓ-suc ℓ-zero)
-data EvCtxPrec : (Γ : PrecCtx) (A : TyPrec) (B : TyPrec) (E : EvCtx (ctx-endpt l Γ) (ty-endpt l A) (ty-endpt l B)) (E' : EvCtx (ctx-endpt r Γ) (ty-endpt r A) (ty-endpt r B)) → Type (ℓ-suc ℓ-zero)
-
-data ValPrec where
-data CompPrec where
-data EvCtxPrec where
-
-
diff --git a/formalizations/guarded-cubical/Syntax/Extensional.agda b/formalizations/guarded-cubical/Syntax/Extensional.agda
deleted file mode 100644
index 7a62b20..0000000
--- a/formalizations/guarded-cubical/Syntax/Extensional.agda
+++ /dev/null
@@ -1,89 +0,0 @@
-module Syntax.Extensional  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 S' T T' U : Ty
-   B B' C C' D D' : Γ ⊑ctx Γ'
-   b b' c c' d d' : S ⊑ S'
-
-data Var : (Γ : Ctx) (S : Ty) → Type where
-  zero : Var (S ∷ Γ) S
-  succ : Var Γ S → Var (T ∷ Γ) S
-
-data Term Γ : (S : Ty) → Type
-
-private
-  variable
-    M M' N N' : Term Γ S
-
-data Term Γ where
-  var : Var Γ S → Term Γ S
-  lda : Term (S ∷ Γ) T → Term Γ (S ⇀ T)
-  app : Term Γ (S ⇀ T) → Term Γ S → Term Γ T
-  zro : Term Γ nat
-  suc : Term Γ nat → Term Γ nat
-  matchNat : Term Γ nat → Term (nat ∷ Γ) T → Term (nat ∷ Γ) T
-           → Term Γ T
-  cast : ∀ S T → Term Γ S → Term Γ T
-
-data Var⊑ : (C : Γ ⊑ctx Γ') (c : S ⊑ S') → Type where
-  zero : Var⊑ (c ∷ C) c
-  suc : Var⊑ C c → Var⊑ (d ∷ C) c
-
-data Term⊑ (C : Γ ⊑ctx Γ') : (c : S ⊑ S') → Type where
-  var : Var⊑ C c → Term⊑ C c
-  lda : Term⊑ (c ∷ C) d → Term⊑ C (c ⇀ d)
-  app : Term⊑ C (c ⇀ d) → Term⊑ C c → Term⊑ C d
-  zro : Term⊑ C nat
-  suc : Term⊑ C nat → Term⊑ C nat
-  matchNat : Term⊑ C nat → Term⊑ (nat ∷ C) c → Term⊑ (nat ∷ C) c
-           → Term⊑ C c
-  castL : ∀ S S' → (c : S ⊑ T)(c' : S' ⊑ T)
-        → Term⊑ C c
-        → Term⊑ C c'
-  castR : ∀ T T' → (c : S ⊑ T) (c' : S ⊑ T')
-        → Term⊑ C c
-        → Term⊑ C c'
-
-var⊑-l : {C : Γ ⊑ctx Γ'} {c : S ⊑ S'} → Var⊑ C c → Var Γ S
-var⊑-l zero = zero
-var⊑-l (suc x) = succ (var⊑-l x)
-
-var⊑-r : {C : Γ ⊑ctx Γ'} {c : S ⊑ S'} → Var⊑ C c → Var Γ' S'
-var⊑-r zero = zero
-var⊑-r (suc x) = succ (var⊑-r x)
-
-term⊑-l : {C : Γ ⊑ctx Γ'} {c : S ⊑ S'} → Term⊑ C c → Term Γ S
-term⊑-l (var x) = var (var⊑-l x)
-term⊑-l (lda m) = lda (term⊑-l m)
-term⊑-l (app m m₁) = app (term⊑-l m) (term⊑-l m₁)
-term⊑-l zro = zro
-term⊑-l (suc m) = suc (term⊑-l m)
-term⊑-l (matchNat m m₁ m₂) = matchNat (term⊑-l m) (term⊑-l m₁) (term⊑-l m₂)
-term⊑-l (castL S S' c _ m) = cast S S' (term⊑-l m)
-term⊑-l (castR T T' c _ m) = term⊑-l m
-
-term⊑-r : {C : Γ ⊑ctx Γ'} {c : S ⊑ S'} → Term⊑ C c → Term Γ' S'
-term⊑-r (var x) = var (var⊑-r x)
-term⊑-r (lda m) = lda (term⊑-r m)
-term⊑-r (app m m₁) = app (term⊑-r m) (term⊑-r m₁)
-term⊑-r zro = zro
-term⊑-r (suc m) = suc (term⊑-r m)
-term⊑-r (matchNat m m₁ m₂) = matchNat (term⊑-r m) (term⊑-r m₁) (term⊑-r m₂)
-term⊑-r (castL S S' c _ m) = term⊑-r m
-term⊑-r (castR T T' c _ m) = cast T T' (term⊑-r m)
diff --git a/formalizations/guarded-cubical/Syntax/GSTLC.agda b/formalizations/guarded-cubical/Syntax/GSTLC.agda
deleted file mode 100644
index 0d9ca07..0000000
--- a/formalizations/guarded-cubical/Syntax/GSTLC.agda
+++ /dev/null
@@ -1,278 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded #-}
-
- -- to allow opening this module in other files while there are still holes
-{-# OPTIONS --allow-unsolved-metas #-}
-
-
-open import Common.Later
-
-module Syntax.GSTLC (k : Clock)  where
-
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Data.Nat hiding (_·_)
-open import Cubical.Relation.Nullary
-open import Cubical.Foundations.Function
-open import Cubical.Data.Prod
-open import Cubical.Foundations.Isomorphism
-
-import Syntax.DeBruijnCommon
-
-
-private
- variable
-   â„“ : Level
-
-private
-  ▹_ : Set ℓ → Set ℓ
-  â–¹_ A = â–¹_,_ k A
-
--- Types --
-
-data Interval : Type where
-  l r : Interval
-
-data iCtx : Type where
-  Empty :  iCtx
-  Full : iCtx
-
-
-data Ty : iCtx -> Type where
-  nat : ∀ {Ξ} -> Ty Ξ
-  dyn : ∀ {Ξ} -> Ty Ξ
-  _=>_ : ∀ {Ξ} -> Ty Ξ -> Ty Ξ -> Ty Ξ
-  inj-nat : Ty Full 
-  inj-arrow : Ty Full -> Ty Full
-
-
--- From a "full" type, i.e. a type precision derivation, we can completely recover its left and
--- right "endpoints"
-{-
-lft : Ty Full -> Ty Empty
-lft nat = nat
-lft dyn = dyn
-lft (cin => cout) = lft cin => lft cout
-lft inj-nat = nat
-lft (inj-arrow c) = lft c -- here, c : A ⊑ (dyn => dyn), and inj-arrow c : A ⊑ dyn
-
-rgt : Ty Full -> Ty Empty
-rgt nat = nat
-rgt dyn = dyn
-rgt (cin => cout) = rgt cin => rgt cout
-rgt inj-nat = dyn
-rgt (inj-arrow c) = dyn
--}
-
-endpoint : Interval -> Ty Full -> Ty Empty
-endpoint p nat = nat
-endpoint p dyn = dyn
-endpoint p (cin => cout) = endpoint p cin => endpoint p cout
-endpoint l inj-nat = nat
-endpoint r inj-nat = dyn
-endpoint l (inj-arrow c) = endpoint l c -- here, c : A ⊑ (dyn => dyn), and inj-arrow c : A ⊑ dyn
-endpoint r (inj-arrow c) = dyn
-
-_[_/i] : Ty Full -> Interval -> Ty Empty
-c [ p /i] = endpoint p c
-
-left : Ty Full -> Ty Empty
-left = endpoint l
-
-right : Ty Full -> Ty Empty
-right = endpoint r
-
-
-_⊑_ : Ty Empty -> Ty Empty -> Type
-A ⊑ B = Σ[ c ∈ Ty Full ] ((left c ≡ A) × (right c ≡ B))
-
-
-infixr 5 _=>_
-
-⊑-ref : (A : Ty Empty) -> A ⊑ A
-⊑-ref nat = nat , (refl , refl)
-⊑-ref dyn = dyn , (refl , refl)
-⊑-ref (Ai => Ao) with ⊑-ref Ai | ⊑-ref Ao
-... | ci , (eq-left-i , eq-right-i) | co , (eq-left-o , eq-right-o) =
-  (ci => co) ,
-    ((congâ‚‚ _=>_ eq-left-i eq-left-o) ,
-     (congâ‚‚ _=>_ eq-right-i eq-right-o))
-
-{-
-
-{-
-data _⊑_ : Ty Empty -> Ty Empty -> Set where
-  dyn : dyn ⊑ dyn
-  _=>_ : {A A' B B' : Ty Empty} ->
-    A ⊑ A' -> B ⊑ B' -> (A => B) ⊑ (A' => B')
-  nat : nat ⊑ nat
-  inj-nat : nat ⊑ dyn
-  inj-arrow : {A : Ty Empty} ->
-    A ⊑ (dyn => dyn) -> A ⊑ dyn
-  -- inj-arrow : {A A' : Ty} ->
-  --   (A => A') ⊑ (dyn => dyn) -> (A => A') ⊑ dyn
--}
-
-
-⊑comp : {A B C : Ty} ->
-  A ⊑ B -> B ⊑ C -> A ⊑ C
-⊑comp dyn dyn = dyn
-⊑comp {Ai => Ao} {Bi => Bo} {Ci => Co} (cin => cout) (din => dout) =
-  (⊑comp cin din) => (⊑comp cout dout)
-⊑comp {Ai => Ao} {Bi => Bo} (cin => cout) (inj-arrow (cin' => cout')) =
-  inj-arrow ((⊑comp cin cin') => (⊑comp cout cout'))
-⊑comp nat nat = nat
-⊑comp nat inj-nat = inj-nat
-⊑comp inj-nat dyn = inj-nat
-⊑comp (inj-arrow c) dyn = inj-arrow c
-
-
-
-module ⊑-properties where
-  -- experiment with modules
-  ⊑-prop : ∀ A B → isProp (A ⊑ B)
-  ⊑-prop .dyn .dyn dyn dyn = refl
-  ⊑-prop .(_ => _) .(_ => _) (p1 => p3) (p2 => p4) = λ i → (⊑-prop _ _ p1 p2 i) => (⊑-prop _ _ p3 p4 i)
-  ⊑-prop .nat .nat nat nat = refl
-  ⊑-prop .nat .dyn inj-nat inj-nat = refl
-  ⊑-prop A .dyn (inj-arrow p1) (inj-arrow p2) = λ i → inj-arrow (⊑-prop _ _ p1 p2 i)
-
-  dyn-⊤ : ∀ A → A ⊑ dyn
-  dyn-⊤ nat = inj-nat
-  dyn-⊤ dyn = dyn
-  dyn-⊤ (A => B) = inj-arrow (dyn-⊤ A => dyn-⊤ B)
-
-  ⊑-dec : ∀ A B → Dec (A ⊑ B)
-  ⊑-dec A dyn = yes (dyn-⊤ A)
-  ⊑-dec nat nat = yes nat
-  ⊑-dec nat (B => B₁) = no (λ ())
-  ⊑-dec dyn nat = no (λ ())
-  ⊑-dec dyn (B => B₁) = no (λ ())
-  ⊑-dec (A => A₁) nat = no ((λ ()))
-  ⊑-dec (A => B) (A' => B') with (⊑-dec A A') | (⊑-dec B B')
-  ... | yes p | yes q = yes (p => q)
-  ... | yes p | no ¬p = no (refute ¬p)
-    where refute : ∀ {A A' B B'} → (¬ (B ⊑ B')) → ¬ ((A => B) ⊑ (A' => B'))
-          refute ¬p (_ => p) = ¬p p
-  ... | no ¬p | _ = no (refute ¬p)
-    where refute : ∀ {A A' B B'} → (¬ (A ⊑ A')) → ¬ ((A => B) ⊑ (A' => B'))
-          refute ¬p (p => _) = ¬p p
-    
--}
-
-
--- Contexts --
-
-data Ctx : iCtx -> Type where
-  · : ∀ {Ξ} -> Ctx Ξ
-  _::_ : ∀ {Ξ} -> Ctx Ξ -> Ty Ξ -> Ctx Ξ
-
-infixr 5 _::_
-
--- Given a "normal" type A, view it as its reflexivity precision derivation c : A ⊑ A.
-ty-refl : Ty Empty -> Ty Full
-ty-refl nat = nat
-ty-refl dyn = dyn
-ty-refl (Ai => Ao) = ty-refl Ai => ty-refl Ao
-
--- View a "normal" typing context Γ as a type precision context where the derivation
--- corresponding to each type A in Γ is just the reflexivity precision derivation A ⊑ A.
-ctx-refl : Ctx Empty -> Ctx Full
-ctx-refl · = ·
-ctx-refl (Γ :: A) = ctx-refl Γ :: ty-refl A
-
--- Flag determining whether the syntax is intensional (i.e., with θ) or extensional
-data IntExt : Type where
-  Int Ext : IntExt
-
--- "Contains" relation stating that a context Γ contains a type T
-data _∋_ : ∀ {Ξ} -> Ctx Ξ -> Ty Ξ -> Set where
-  vz : ∀ {Ξ Γ S} -> _∋_ {Ξ} (Γ :: S) S
-  vs : ∀ {Ξ Γ S T} (x : _∋_ {Ξ} Γ T) -> (Γ :: S ∋ T)
-
-infix 4 _∋_
-
-
--- All constructors below except for those for upcast and downcast are simultaneously
--- the term constructors, as well as the constructors for the corresponding term
--- precision congruence rule.
--- 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.
-
--- All constructors below except for θ simultaneously belong to the extensional
--- and intensional languages. θ only exists in the intensional language.
-data Tm : (α : IntExt) {Ξ : iCtx} -> (Γ : Ctx Ξ) -> Ty Ξ -> Set where
-  var : ∀ {α Ξ Γ T}   -> Γ ∋ T -> Tm α {Ξ} Γ T
-  lda : ∀ {α Ξ Γ S T} -> (Tm α {Ξ} (Γ :: S) T) -> Tm α Γ (S => T)
-  app : ∀ {α Ξ Γ S T} -> (Tm α {Ξ} Γ (S => T)) -> (Tm α Γ S) -> (Tm α Γ T)
-  err : ∀ {α Ξ Γ A} -> Tm α {Ξ} Γ A
-  up  : ∀ {α Γ} (c : Ty Full) -> Tm α {Empty} Γ (left c) -> Tm α {Empty} Γ (right c)
-  dn  : ∀ {α Γ} (c : Ty Full) -> Tm α {Empty} Γ (right c) -> Tm α {Empty} Γ (left c)
-  zro : ∀ {α Ξ Γ} -> Tm α {Ξ} Γ nat
-  suc : ∀ {α Ξ Γ} -> Tm α {Ξ} Γ nat -> Tm α Γ nat
-  θ   : ∀ {Ξ Γ A} -> ▹ Tm Int {Ξ} Γ A -> Tm Int {Ξ} Γ A
-
- 
-
-
-  -- Equational theory
-
-  -- Other term precision rules
-  err-bot : ∀ {α Γ} (c : Ty Full) (M : Tm α {Empty} Γ (right c)) -> Tm α {Full} (ctx-refl Γ) c
-
-
--- TODO need to quotient by the equational theory!
-
--- TODO non-congruence term precision rules
-
-
-
--- Substitution and Renaming using De Bruijn framework
-module DB_Base = Syntax.DeBruijnCommon (Ty Empty) (Ctx 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}
-       (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)
-  -- Note that the type of lft can also be written as (Subst Δ Γ _◈_) -> (Subst (Δ ∷ S) (Γ ∷ S) _◈_)
-
-  -- Traversal function --
-
-
-trav : {Δ Γ : Ctx 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'))
-trav K Ï„ (app f s) =  (app (trav K Ï„ f) (trav K Ï„ s))
-trav K Ï„ (up deriv t') =  (up deriv (trav K Ï„ t'))
-trav K Ï„ (dn deriv t') = (dn deriv (trav K Ï„ t'))
-trav K Ï„ err = err
-trav K Ï„ zro = zro
-trav K Ï„ (suc t') = (suc (trav K Ï„ t'))
-
-
-open DB_Base.DeBruijn trav var
--- Gives us renaming and substitution
-
--- Single substitution
--- N[M/x]
-
-
-_[_] : ∀ {Γ A B}
-  → Tm Ext (Γ :: B) A
-  → Tm Ext Γ B
-  → Tm Ext Γ A
-_[_] {Γ} {A} {B} N M = {!!} -- sub Γ (Γ :: B) σ A N
-  where
-    σ : Subst Γ (Γ :: B) (Tm Ext) -- i.e., {T : Ty} → Γ :: B ∋ T → Tm Γ T
-    σ vz = M
-    σ (vs x) = var x
-
-
-
-
-
diff --git a/formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda b/formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda
deleted file mode 100644
index d566b91..0000000
--- a/formalizations/guarded-cubical/Syntax/GSTLCCollapse.agda
+++ /dev/null
@@ -1,66 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded #-}
-
-open import Common.Later
-
-module Syntax.GSTLCCollapse (k : Clock) where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Data.Nat hiding (_·_)
-open import Cubical.Relation.Nullary
-open import Cubical.Data.Sum
-open import Cubical.Foundations.Isomorphism
-
-import Syntax.DeBruijnCommon
-open import Syntax.GSTLC k
-
-
-private
- variable
-    â„“ : Level
-
-private
-  ▹_ : Set ℓ → Set ℓ
-  â–¹_ A = â–¹_,_ k A
-
-
-IntTm = Tm Int
-ExtTm = Tm Ext
-
-
-⌊_⌋ : ∀ {Γ} {A} -> IntTm {Empty} Γ A -> ExtTm {Empty} Γ A
-⌊ var x ⌋ = var x
-⌊ lda M ⌋ = lda ⌊ M ⌋
-⌊ app M N ⌋ = app ⌊ M ⌋ ⌊ N ⌋
-⌊ err ⌋ = err
-⌊ up c M ⌋ = up c ⌊ M ⌋
-⌊ dn c M ⌋ = dn c ⌊ M ⌋
-⌊ zro ⌋ = zro
-⌊ suc M ⌋ = suc ⌊ M ⌋
-⌊ θ M~ ⌋ = ⌊ M~ ◇ ⌋
-
-
-embed : ∀ {Γ} {A} -> ExtTm {Empty} Γ A -> IntTm {Empty} Γ A
-embed (var x) = var x
-embed (lda M) = lda (embed M)
-embed (app M N) = app (embed M) (embed N)
-embed err = err
-embed (up c M) = up c (embed M)
-embed (dn c M) = dn c (embed M)
-embed zro = zro
-embed (suc M) = suc (embed M)
-
-
-
--- Every extensional term has an intensional program computing it
-collapse-embed : ∀ {Γ} {A} -> retract embed (⌊_⌋ {Γ} {A})
-collapse-embed (var x) = refl
-collapse-embed (lda M) = cong lda (collapse-embed M)
-collapse-embed (app M N) = congâ‚‚ app (collapse-embed M) (collapse-embed N)
-collapse-embed err = refl
-collapse-embed (up c M) = cong (up c) (collapse-embed M)
-collapse-embed (dn c M) = cong (dn c) (collapse-embed M)
-collapse-embed zro = refl
-collapse-embed (suc M) = cong suc (collapse-embed M)
-
-
-
diff --git a/formalizations/guarded-cubical/Syntax/Intensional.agda b/formalizations/guarded-cubical/Syntax/Intensional.agda
deleted file mode 100644
index 380c15b..0000000
--- a/formalizations/guarded-cubical/Syntax/Intensional.agda
+++ /dev/null
@@ -1,266 +0,0 @@
-{-# OPTIONS --cubical #-}
-module Syntax.Intensional  where
-
--- The intensional syntax, which is quotiented by βη equivalence and
--- order equivalence but where casts take observable steps.
-
-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
-open CtxPrec
-
-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'
-
--- Substitutions, Values, Computations and Evaluation contexts,
--- quotiented by *intensional* order equivalence, including βη equalities
-data Subst : (Δ : Ctx) (Γ : Ctx) → Type
-data Subst⊑ : (C : Δ ⊑ctx Δ') (D : Γ ⊑ctx Γ') (γ : Subst Δ Γ) (γ' : Subst Δ' Γ') → Type
-
-data Val : (Γ : Ctx) (S : Ty) → Type
-data Val⊑ : (C : Γ ⊑ctx Γ') (c : S ⊑ S') (V : Val Γ S) (V' : Val Γ' S') → Type
-
-data EvCtx : (Γ : Ctx) (S : Ty) (T : Ty) → Type
-data EvCtx⊑ : (C : Γ ⊑ctx Γ') (c : S ⊑ S') (d : T ⊑ T') (E : EvCtx Γ S T) (E' : EvCtx Γ' S' T') → Type
-
-data Comp : (Γ : Ctx) (S : Ty) → Type
-data Comp⊑ : (C : Γ ⊑ctx Γ') (c : S ⊑ S') (M : Comp Γ S) (M' : Comp Γ' S') → Type
-
-
-private
-  variable
-    γ γ' γ'' : Subst Δ Γ
-    δ δ' δ'' : Subst Θ Δ
-    θ θ' θ'' : Subst Z Θ
-
-    V V' V'' : Val Γ S
-    M M' M'' N N' : Comp Γ S
-    E 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
-
-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 Δ Γ)
-  isPosetSubst : Subst⊑ (refl-⊑ctx Δ) (refl-⊑ctx Γ) γ γ'
-               → Subst⊑ (refl-⊑ctx Δ) (refl-⊑ctx Γ) γ' γ
-               → γ ≡ γ'
-
-  -- [] 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 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 γ γ')
-  hetTrans : Subst⊑ C D γ γ' → Subst⊑ C' D' γ' γ'' → Subst⊑ (trans-⊑ctx C C') (trans-⊑ctx D D') γ γ''
-
-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)
-  δl  : (S⊑T : TyPrec) → Val [ ty-left S⊑T ] (ty-left S⊑T)
-  δr  : (S⊑T : TyPrec) → Val [ ty-right S⊑T ] (ty-right S⊑T)
-
-  isSetVal : isSet (Val Γ S)
-  isPosetVal : Val⊑ (refl-⊑ctx Γ) (refl-⊑ S) V V'
-             → Val⊑ (refl-⊑ctx Γ) (refl-⊑ S) V' V
-             → V ≡ V'
-
-_[_]vP = _[_]v
-varP = var
-
-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
-
-  -- if x <= y then e x <= δr y
-  up-L : ∀ S⊑T → Val⊑ ((ty-prec S⊑T) ∷ []) (refl-⊑ (ty-right S⊑T)) (up S⊑T) (δr S⊑T)
-  -- if x <= y then δl x <= e y
-  up-R : ∀ S⊑T → Val⊑ ((refl-⊑ (ty-left S⊑T)) ∷ []) (ty-prec S⊑T) (δl S⊑T) (up S⊑T)
-
-  isProp⊑ : isProp (Val⊑ C c V V')
-  hetTrans : Val⊑ C c V V' → Val⊑ D d V' V'' → Val⊑ (trans-⊑ctx C D) (trans-⊑ c d) V V''
-
-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)
-  δl  : (S⊑T : TyPrec) → EvCtx [] (ty-left S⊑T) (ty-left S⊑T)
-  δr  : (S⊑T : TyPrec) → EvCtx [] (ty-right S⊑T) (ty-right S⊑T)
-
-  isSetEvCtx : isSet (EvCtx Γ S T)
-  isPosetEvCtx : EvCtx⊑ (refl-⊑ctx Γ) (refl-⊑ S) (refl-⊑ T) E E'
-               → EvCtx⊑ (refl-⊑ctx Γ) (refl-⊑ S) (refl-⊑ T) E' E
-               → E ≡ E'
-
-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)
-  isPosetComp : Comp⊑ (refl-⊑ctx Γ) (refl-⊑ S) M M'
-              → Comp⊑ (refl-⊑ctx Γ) (refl-⊑ S) M' M
-              → M ≡ M'
-
-appP = app
-retP = ret
-_[_]cP = _[_]c
-_[_]∙P = _[_]∙
-
-err' : Comp Γ S
-err' = err [ !s ]c
-
-ret' : Val Γ S → Comp Γ S
-ret' V = ret [ !s ,s V ]c
-
-vToE : Val [ S ] T → EvCtx [] S T
-vToE V = bind (ret [ !s ,s V ]c)
-
-upE : ∀ S⊑T → EvCtx [] (ty-left S⊑T) (ty-right S⊑T)
-upE S⊑T = vToE (up S⊑T)
-
-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 (bind M) (bind M')
-
-  dn-L : ∀ S⊑T → EvCtx⊑ [] (refl-⊑ (ty-right S⊑T)) (ty-prec S⊑T) (dn S⊑T) (δr S⊑T)
-  dn-R : ∀ S⊑T → EvCtx⊑ [] (ty-prec S⊑T) (refl-⊑ (ty-left S⊑T)) (δl S⊑T) (dn S⊑T)
-  retractionR : ∀ S⊑T → EvCtx⊑ [] (refl-⊑ (ty-right S⊑T)) (refl-⊑ (ty-right S⊑T))
-    (vToE (δr S⊑T) ∘E δr S⊑T)
-    (vToE (up S⊑T) ∘E dn S⊑T)
-
-  hetTrans : 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
-
-  hetTrans : 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')
-
--- -- TODO: admissibility of Reflexivity of each ⊑
--- refl-Subst⊑ : ∀ γ → Subst⊑ (refl-⊑ctx Δ) (refl-⊑ctx Γ) γ γ
--- refl-Subst⊑ γ = {!!}
-
--- refl-Val⊑ : ∀ V → Val⊑ (refl-⊑ctx Γ) (refl-⊑ S) V V
--- refl-Val⊑ V = {!!}
-
--- refl-Comp⊑ : ∀ M → Comp⊑ (refl-⊑ctx Γ) (refl-⊑ S) M M
--- refl-Comp⊑ M = {!!}
-
--- refl-EvCtx⊑ : ∀ E → EvCtx⊑ (refl-⊑ctx Γ) (refl-⊑ S) (refl-⊑ S) E E
--- refl-EvCtx⊑ E = {!!}
diff --git a/formalizations/guarded-cubical/Syntax/SyntaxNew.agda b/formalizations/guarded-cubical/Syntax/SyntaxNew.agda
deleted file mode 100644
index 41e59c7..0000000
--- a/formalizations/guarded-cubical/Syntax/SyntaxNew.agda
+++ /dev/null
@@ -1,307 +0,0 @@
-{-# OPTIONS --cubical --rewriting --guarded #-}
-
- -- to allow opening this module in other files while there are still holes
-{-# OPTIONS --allow-unsolved-metas #-}
-{-# OPTIONS --lossy-unification #-}
-
-
-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 (_·_)
-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
--- import Syntax.DeBruijnCommon
-
-private
- variable
-   â„“ â„“' â„“'' : Level
-
-open import Syntax.Types
-open Ctx
--- ############### Terms / Term Precision ###############
-
--- All constructors below except for those for upcast and downcast are simultaneously
--- the term constructors, as well as the constructors for the corresponding term
--- precision congruence rule.
--- 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 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 : ∀ {Γ : 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} {Γ Δ : 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
-
-
-
---   -- Equational theory:
-  
--- {-
---   β-case :
-
---   η-case :
-
---   β-ret :
-
---   η-ret :
--- -}
-
---   -- Propositional truncation:
-  
---   -- squash : ∀ {v α Ξ Γ A} -> (M N : Tm {v} {Ξ} Γ A) -> (p q : M ≡ N) -> p ≡ q
---   squash : ∀ {v α Ξ Γ A} -> isSet (Tm {v} {Ξ} Γ A)
-
---   -- Quotient the ordering:
-  
-
-
--- _⊑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))
-
-
--- Recall:
--- 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} 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)
-
--- tm-endpt p (err-bot B x) = {!!}
-
-
-
--- 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
-
--- 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) = {!!}
-
-
-
-
-
-
-{-
-
--- Substitution and Renaming using De Bruijn framework
-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 : {Δ Γ : 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)
-  -- Note that the type of lft can also be written as (Subst Δ Γ _◈_) -> (Subst (Δ ∷ S) (Γ ∷ S) _◈_)
-
--- Traversal function --
-
-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'))
-trav K Ï„ (app f s) =  (app (trav K Ï„ f) (trav K Ï„ s))
-trav K Ï„ (up deriv t') =  (up deriv (trav K Ï„ t'))
-trav K Ï„ (dn deriv t') = (dn deriv (trav K Ï„ t'))
-trav K Ï„ err = err
-trav K Ï„ zro = zro
-trav K Ï„ (suc t') = (suc (trav K Ï„ t'))
-
-
-open DB_Base.DeBruijn trav var
--- Gives us renaming and substitution
-
--- Single substitution
--- N[M/x]
-
-
-_[_] : ∀ {Γ A B}
-  → Tm Ext (Γ :: B) A
-  → Tm Ext Γ B
-  → Tm Ext Γ A
-_[_] {Γ} {A} {B} N M = {!!} -- sub Γ (Γ :: B) σ A N
-  where
-    σ : Subst Γ (Γ :: B) (Tm Ext) -- i.e., {T : Ty} → Γ :: B ∋ T → Tm Γ T
-    σ vz = M
-    σ (vs x) = var x
-
--}
-- 
GitLab