From 5b9e4b9fffa825162d66d8f2c2c1a4b86ab1231b Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 24 May 2023 13:16:01 -0400
Subject: [PATCH] Implement the GTT logic, reduce the amount of annotations
 using nested var generalization

---
 .../guarded-cubical/Syntax/Logic.agda         | 104 +++++++-
 .../guarded-cubical/Syntax/Terms.agda         | 186 +++++++------
 .../guarded-cubical/Syntax/Types.agda         | 251 ++++++------------
 3 files changed, 279 insertions(+), 262 deletions(-)

diff --git a/formalizations/guarded-cubical/Syntax/Logic.agda b/formalizations/guarded-cubical/Syntax/Logic.agda
index 4e07e64..36d66b8 100644
--- a/formalizations/guarded-cubical/Syntax/Logic.agda
+++ b/formalizations/guarded-cubical/Syntax/Logic.agda
@@ -10,18 +10,106 @@ 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.List hiding (nil)
 open import Cubical.Data.Empty renaming (rec to exFalso)
 
 open import Syntax.Types
 open import Syntax.Terms
 
-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)
+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)) (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
 
-data ValPrec where
-data CompPrec where
-data EvCtxPrec where
+_≈e_ : (E E' : EvCtx Γ S T) → Type _
+E ≈e E' = EvCtx⊑-homo E E' × EvCtx⊑-homo E' E
 
+-- TODO: show up, down are monotone, derive semantics of function casts
diff --git a/formalizations/guarded-cubical/Syntax/Terms.agda b/formalizations/guarded-cubical/Syntax/Terms.agda
index f0b7dc4..32b96e4 100644
--- a/formalizations/guarded-cubical/Syntax/Terms.agda
+++ b/formalizations/guarded-cubical/Syntax/Terms.agda
@@ -11,40 +11,43 @@ 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
 
-SynType = Ty Empty
-TyPrec = Ty Full
-
-TypeCtx = Ctx Empty
-PrecCtx = Ctx Full
+open TyPrec
 
 private
  variable
-   â„“ â„“' â„“'' : Level
-   Δ Γ Θ Z : TypeCtx
-   R S T U : SynType
+   Δ Γ Θ 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 : (Δ : TypeCtx) (Γ : TypeCtx) → Type
-data Val : (Γ : TypeCtx) (A : SynType) → Type
-data EvCtx : (Γ : TypeCtx) (A : SynType) (B : SynType) → Type
-data Comp : (Γ : TypeCtx) (A : SynType) → Type
+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
-_[_]v : Val Γ S → Subst Δ Γ → Val Δ S
-_[_]c : Comp Γ S → Subst Δ Γ → Comp Δ S
-_[_]e : EvCtx Γ S T → Subst Δ Γ → EvCtx Δ S T
-_[_]∙ : EvCtx Γ S T → Comp Γ S → Comp Γ T
-var : Val (S ∷ Γ) S
-ret : Comp [ S ] S
-app : Comp (S ∷ (S ⇀ T) ∷ []) T
+_[_]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
@@ -58,102 +61,95 @@ data Subst where
   -- Subst is a cat
   ids : Subst Γ Γ
   _∘s_ : Subst Δ Θ → Subst Γ Δ → Subst Γ Θ
-  ∘IdL : (γ : Subst Γ Γ) → ids ∘s γ ≡ γ
-  ∘IdR : (γ : Subst Γ Γ) → γ ∘s ids ≡ γ
-  ∘Assoc : (γ : Subst Δ Γ) (δ : Subst Θ Δ)(θ : Subst Z Θ) → γ ∘s (δ ∘s θ) ≡ (γ ∘s δ) ∘s θ
+  ∘IdL : ids ∘s γ ≡ γ
+  ∘IdR : γ ∘s ids ≡ γ
+  ∘Assoc : γ ∘s (δ ∘s θ) ≡ (γ ∘s δ) ∘s θ
 
   -- [] is terminal
   !s : Subst Γ []
-  []η : (γ : Subst Γ []) → γ ≡ !s
+  []η : γ ≡ !s
 
   -- universal property of S ∷ Γ
   -- β (other one is in Val), η and naturality
   _,s_ : Subst Γ Δ → Val Γ S → Subst Γ (S ∷ Δ)
   wk : Subst (S ∷ Γ) Γ
-  wkβ : (δ : Subst Γ Δ)(V : Val Γ S) → wk ∘s (δ ,s V) ≡ δ
-  ,sη : (δ : Subst Γ (S ∷ Δ)) → δ ≡ (wk ∘s δ ,s var [ δ ]v)
+  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
-  varPrim : Val (S ∷ Γ) S
-  varβ : (δ : Subst Γ Δ) (V : Val Γ S) → var [ δ ,s V ]v ≡ V
+  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
-  fun-η : (V : Val Γ (S ⇀ T))
-        -- V = λ x. V x
-        → V ≡ lda (app [ (!s ,s (V [ wk ]v)) ,s var ]c)
+  -- 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)
 
-  -- values form a presheaf over substitutions
-  _[_]v' : Val Γ S → Subst Δ Γ → Val Δ S
-  substId : (V : Val Γ S) → V [ ids ]v ≡ V
-  substAssoc : (V : Val Δ S) (δ : Subst Γ Δ)(γ : Subst Θ Γ)
-          → V [ δ ∘s γ ]v ≡ (V [ δ ]v) [ γ ]v
-
   isSetVal : isSet (Val Γ S)
 
-_[_]v = _[_]v'
-var = varPrim
+_[_]vP = _[_]v
+varP = var
 
 data EvCtx where
   ∙E : EvCtx Γ S S
   _∘E_ : EvCtx Γ T U → EvCtx Γ S T → EvCtx Γ S U
-  ∘IdL : (E : EvCtx Γ S T) → ∙E ∘E E ≡ E
-  ∘IdR : (E : EvCtx Γ S T) → E ∘E ∙E ≡ E
-  ∘Assoc : (E : EvCtx Γ T U) (F : EvCtx Γ S T)(G : EvCtx Γ R S)
-         → E ∘E (F ∘E G) ≡ (E ∘E F) ∘E G
+  ∘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 : EvCtx Γ S T) → E [ ids ]e ≡ E
-  substAssoc : (E : EvCtx Γ S T)(γ : Subst Δ Γ)(δ : Subst Θ Δ)
-            → E [ γ ∘s δ ]e ≡ E [ γ ]e [ δ ]e
+  _[_]e : EvCtx Γ S T → Subst Δ Γ → EvCtx Δ S T
+  substId : E [ ids ]e ≡ E
+  substAssoc : E [ γ ∘s δ ]e ≡ E [ γ ]e [ δ ]e
 
-  ∘substDist : (E : EvCtx Γ T U)(F : EvCtx Γ S T)(γ : Subst Δ Γ)
-             → (E ∘E F) [ γ ]e ≡ (E [ γ ]e) ∘E (F [ γ ]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 : EvCtx Γ S T) → E ≡ bind (E [ wk ]e [ ret [ !s ,s var ]c ]∙)
+  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 : (M : Comp Γ S) → ∙E [ M ]∙ ≡ M
-  plugAssoc : (M : Comp Γ S)(E : EvCtx Γ S T)(F : EvCtx Γ T U) → (F ∘E E) [ M ]∙ ≡ F [ E [ M ]∙ ]∙
+  _[_]∙ : 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
+  _[_]c : Comp Δ S → Subst Γ Δ → Comp Γ S
   -- presheaf
-  substId : (M : Comp Γ S) → M [ ids ]c ≡ M
-  substAssoc : (M : Comp Δ S) (δ : Subst Γ Δ)(γ : Subst Θ Γ)
-         → M [ δ ∘s γ ]c ≡ (M [ δ ]c) [ γ ]c
+  substId : M [ ids ]c ≡ M
+  substAssoc : M [ δ ∘s γ ]c ≡ (M [ δ ]c) [ γ ]c
 
   -- Interchange law
-  substPlugDist : (E : EvCtx Γ S T) (M : Comp Γ S) → (γ : Subst Δ Γ)
-                → (E [ M ]∙) [ γ ]c ≡ (E [ γ ]e) [ M [ γ ]c ]∙
+  substPlugDist : (E [ M ]∙) [ γ ]c ≡ (E [ γ ]e) [ M [ γ ]c ]∙
 
   err : Comp [] S
   -- E[err] ≡ err
-  strictness : (E : EvCtx Γ S T) → E [ err [ !s ]c ]∙ ≡ err [ !s ]c
+  strictness : E [ err [ !s ]c ]∙ ≡ err [ !s ]c
 
-  retPrim : Comp [ S ] S
+  ret : Comp [ S ] S
   -- x <- ret x; M ≡ M
-  ret-β : (M : Comp (S ∷ Γ) T) → (bind M [ wk ]e [ ret [ !s ,s var ]c ]∙) ≡ M
+  ret-β : (bind M [ wk ]e [ ret [ !s ,s var ]c ]∙) ≡ M
 
-  appPrim : Comp (S ∷ S ⇀ T ∷ []) T
+  app : Comp (S ∷ S ⇀ T ∷ []) T
   -- (λ x. M) x ≡ M
-  fun-β : (M : Comp (S ∷ Γ) T) → app [ (!s ,s ((lda M) [ wk ]v)) ,s var ]c ≡ 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
@@ -163,14 +159,13 @@ data Comp where
   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 : Comp (nat ∷ Γ) S) → M ≡ matchNat (M [ ids ,s (zro [ !s ]v) ]c) (M [ wk ,s (suc [ !s ,s var ]v) ]c)
+  matchNatη : M ≡ matchNat (M [ ids ,s (zro [ !s ]v) ]c) (M [ wk ,s (suc [ !s ,s var ]v) ]c)
 
   isSetComp : isSet (Comp Γ S)
-app = appPrim
-ret = retPrim
-_[_]c = _[_]c'
-_[_]e = _[_]e'
-_[_]∙ = _[_]∙'
+appP = app
+retP = ret
+_[_]cP = _[_]c
+_[_]∙P = _[_]∙
 
 -- More ordinary term constructors are admissible
 -- up, dn, zro, suc, err, app, bind
@@ -179,45 +174,60 @@ 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-nat γ = []η
 
 ,s-nat : (δ : Subst Θ Δ) (γ : Subst Δ Γ) (V : Val Δ S)
        → (γ ,s V) ∘s δ ≡ ((γ ∘s δ) ,s (V [ δ ]v))
 ,s-nat δ γ V =
-  ,sη _
-  ∙ cong₂ _,s_ (∘Assoc _ _ _ ∙ cong (_∘s δ) (wkβ _ _))
-               (substAssoc _ _ _ ∙ cong _[ δ ]v (varβ _ _))
+  ,sη
+  ∙ cong₂ _,s_ (∘Assoc ∙ cong (_∘s δ) wkβ)
+               (substAssoc ∙ cong _[ δ ]v varβ)
 
 -- 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)
+  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 ([]η (!s ∘s the-subst))) (sym (substAssoc _ _ _)
-                                                                                    ∙ cong (lda M [_]v) (sym (wkβ _ var))
-                                                                                    ∙ substAssoc _ _ _))
-                                                      (sym (varβ (γ ∘s wk) _))
+  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
+             ∙ 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β _ _))
+  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-β _)
+  ∙ substAssoc
+  ∙ cong (_[ ids ,s V ]c) fun-β
 
-fun-η' : (V : Val Γ (S ⇀ T)) → V ≡ lda (app' (V [ wk ]v) var)
+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
+
+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))
diff --git a/formalizations/guarded-cubical/Syntax/Types.agda b/formalizations/guarded-cubical/Syntax/Types.agda
index 1e69e68..669826f 100644
--- a/formalizations/guarded-cubical/Syntax/Types.agda
+++ b/formalizations/guarded-cubical/Syntax/Types.agda
@@ -7,44 +7,86 @@ open import Cubical.Foundations.Prelude renaming (comp to compose)
 open import Cubical.Data.Nat
 open import Cubical.Relation.Nullary
 open import Cubical.Foundations.Function
-open import Cubical.Data.List
+open import Cubical.Data.List hiding (nil)
 open import Cubical.Data.Prod hiding (map)
 open import Cubical.Data.Empty renaming (rec to exFalso)
 
-private
- variable
-   â„“ : Level
-
-
 -- Types --
+data Ty : Type where
+  nat : Ty
+  dyn : Ty
+  _⇀_ : Ty -> Ty -> Ty
 
-data Interval : Type where
-  l r : Interval
-
-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 : endpt-fun Ty
-
-_⊑_ : Ty Empty -> Ty Empty -> Type
-A ⊑ B = Σ[ c ∈ Ty Full ] ((ty-endpt l c ≡ A) × (ty-endpt r c ≡ B))
-
-data Ty where
-  nat : ∀ {Ξ} -> Ty Ξ
-  dyn : ∀ {Ξ} -> Ty Ξ
-  _⇀_ : ∀ {Ξ} -> Ty Ξ -> Ty Ξ -> Ty Ξ
-  inj-nat : Ty Full
-  inj-arr : Ty Full
-  comp : ∀ (c : Ty Full) -> (d : Ty Full) ->
-    (ty-endpt l c ≡ ty-endpt r d) -> Ty Full
-  -- isProp⊑ : ∀ {A B : Ty }
-
+private -- should we make this public???
+ variable
+   R R' S S' T T' U U' : Ty
+
+data _⊑_ : Ty → Ty → Type where
+  nat : nat ⊑ nat
+  dyn : dyn ⊑ dyn
+  _⇀_ : R ⊑ R' → S ⊑ S' → (R ⇀ S) ⊑ (R' ⇀ S')
+  inj-nat : nat ⊑ dyn
+  inj-arr : (dyn ⇀ dyn) ⊑ dyn
+  trans   : R ⊑ S → S ⊑ T → R ⊑ T
+  -- this is not provable bc we can do a trans with an id relation
+  -- might cause issues later though...
+  isProp⊑ : isProp (R ⊑ S)
+
+refl-⊑ : ∀ S → S ⊑ S
+refl-⊑ nat = nat
+refl-⊑ dyn = dyn
+refl-⊑ (S ⇀ T) = refl-⊑ S ⇀ refl-⊑ T
+
+record TyPrec : Type where
+  field
+    ty-left  : Ty
+    ty-right : Ty
+    ty-prec  : ty-left ⊑ ty-right
+
+open TyPrec
+
+refl-TP : ∀ (S : Ty) → TyPrec
+refl-TP S = record { ty-left = S ; ty-right = S ; ty-prec = refl-⊑ S }
+
+Ctx = List Ty
+private
+  variable
+    Γ Γ' Δ Δ' Θ Θ' : Ctx
+
+-- Couldn't find anything in the stdlib. Data.List.Dependent is close
+-- but only works for one parameter
+data _⊑ctx_ : Ctx → Ctx → Type where
+  [] : [] ⊑ctx []
+  _∷_ : S ⊑ S' → Γ ⊑ctx Γ' → (S ∷ Γ) ⊑ctx (S' ∷ Γ')
+
+refl-⊑ctx : ∀ Γ → Γ ⊑ctx Γ
+refl-⊑ctx [] = []
+refl-⊑ctx (S ∷ Γ) = (refl-⊑ S) ∷ (refl-⊑ctx Γ)
+
+trans-⊑ctx : Γ ⊑ctx Δ → Δ ⊑ctx Θ → Γ ⊑ctx Θ
+trans-⊑ctx [] [] = []
+trans-⊑ctx (c ∷ C) (d ∷ D) = (trans c d) ∷ (trans-⊑ctx C D)
+
+record CtxPrec : Type where
+  field
+    ctx-left : Ctx
+    ctx-right : Ctx
+    ctx-prec : ctx-left ⊑ctx ctx-right
+
+open CtxPrec
+nil : CtxPrec
+nil .ctx-left = []
+nil .ctx-right = []
+nil .ctx-prec = []
+
+cons : TyPrec → CtxPrec → CtxPrec
+cons c C .ctx-left = c .ty-left ∷ C .ctx-left
+cons c C .ctx-right = c .ty-right ∷ C .ctx-right
+cons c C .ctx-prec = (ty-prec c) ∷ (ctx-prec C)
+
+refl-CP : Ctx → CtxPrec
+refl-CP [] = nil
+refl-CP (S ∷ Γ) = cons (refl-TP S) (refl-CP Γ)
 module _ where
   open import Cubical.Foundations.HLevels
   open import Cubical.Data.W.Indexed
@@ -53,17 +95,17 @@ module _ where
 
   private
     X = Unit
-    S : Unit → Type
-    S tt = Unit ⊎ (Unit ⊎ Unit)
-    P : ∀ x → S x → Type
+    St : Unit → Type
+    St tt = Unit ⊎ (Unit ⊎ Unit)
+    P : ∀ x → St x → Type
     P tt (inl x) = ⊥
     P tt (inr (inl x)) = ⊥
     P tt (inr (inr x)) = Unit ⊎ Unit
-    inX : ∀ x → (s : S x) → P x s → X
+    inX : ∀ x → (s : St x) → P x s → X
     inX x s p = tt
-    W = IW S P inX tt
+    W = IW St P inX tt
 
-    Ty→W : Ty Empty → W
+    Ty→W : Ty → W
     Ty→W nat = node (inl tt) exFalso
     Ty→W dyn = node (inr (inl tt)) exFalso
     Ty→W (A ⇀ B) = node (inr (inr tt)) trees where
@@ -71,138 +113,15 @@ module _ where
       trees (inl x) = Ty→W A
       trees (inr x) = Ty→W B
 
-    W→Ty : W → Ty Empty
+    W→Ty : W → Ty
     W→Ty (node (inl x) subtree) = nat
     W→Ty (node (inr (inl x)) subtree) = dyn
     W→Ty (node (inr (inr x)) subtree) = W→Ty (subtree (inl tt)) ⇀ W→Ty (subtree (inr tt))
 
-    rtr : (x : Ty Empty) → W→Ty (Ty→W x) ≡ x
+    rtr : (x : Ty) → W→Ty (Ty→W x) ≡ x
     rtr nat = refl
     rtr dyn = refl
     rtr (A ⇀ B) = cong₂ _⇀_ (rtr A) (rtr B)
-    
-  isSetTy : isSet (Ty Empty)
-  isSetTy = isSetRetract Ty→W W→Ty rtr (isOfHLevelSuc-IW 1 (λ tt → isSet⊎ isSetUnit (isSet⊎ isSetUnit isSetUnit)) tt)
-
-ty-endpt p nat = nat
-ty-endpt p dyn = dyn
-ty-endpt p (cin ⇀ cout) = ty-endpt p cin ⇀ ty-endpt p cout
-ty-endpt l inj-nat = nat
-ty-endpt r inj-nat = dyn
-ty-endpt l inj-arr = (dyn ⇀ dyn) -- inj-arr : (dyn -> dyn) ⊑ dyn
-ty-endpt r inj-arr = dyn
-ty-endpt l (comp c d _) = ty-endpt l d
-ty-endpt r (comp c d _) = ty-endpt r c
-
-_[_/i] : Ty Full -> Interval -> Ty Empty
-c [ p /i] = ty-endpt p c
-
-ty-left : Ty Full -> Ty Empty
-ty-left = ty-endpt l
-
-ty-right : Ty Full -> Ty Empty
-ty-right = ty-endpt r
-
-CompTyRel : Type
-CompTyRel = Σ (Ty Full × Ty Full)
-  λ { (c' , c) -> (ty-left c') ≡ (ty-right c) }
-
-CompTyRel-comp : CompTyRel -> Ty Full
-CompTyRel-comp ((c' , c) , pf) = comp c' c pf
-
-CompTyRel-endpt : Interval -> CompTyRel -> Ty Full
-CompTyRel-endpt l ((c , d) , _) = c
-CompTyRel-endpt r ((c , d) , _) = d
-
--- 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
-
-ty-endpt-refl : {A : Ty Empty} -> (p : Interval) -> ty-endpt p (ty-refl A) ≡ A
-ty-endpt-refl {nat} p = refl
-ty-endpt-refl {dyn} p = refl
-ty-endpt-refl {A ⇀ B} p = cong₂ _⇀_ (ty-endpt-refl p) (ty-endpt-refl p)
 
--- ############### Contexts ###############
-
-Ctx : iCtx -> Type
-Ctx Ξ = List (Ty Ξ)
-
--- Endpoints of a full context
-ctx-endpt : (p : Interval) -> Ctx Full -> Ctx Empty
-ctx-endpt p = map (ty-endpt p)
-
--- CompCtx : (Δ Γ : Ctx Full) -> (pf : ctx-endpt l Δ ≡ ctx-endpt r Γ) ->
---   Ctx Full
--- CompCtx Δ Γ pf = {!!}
-
--- "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 _∋_
-
-∋-ctx-endpt : {Γ : Ctx Full} {c : Ty Full} -> (p : Interval) ->
-  (Γ ∋ c) -> ((ctx-endpt p Γ) ∋ (ty-endpt p c))
-∋-ctx-endpt p vz = vz
-∋-ctx-endpt p (vs Γ∋c) = vs (∋-ctx-endpt p Γ∋c)
-
-
-
--- 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 = map ty-refl
---ctx-refl · = ·
---ctx-refl (A :: Γ) = ty-refl A :: ctx-refl Γ
-
--- For a given typing context, the endpoints of the corresponding reflexivity precision
--- context are the typing context itself.
-ctx-endpt-refl : {Γ : Ctx Empty} -> (p : Interval) -> ctx-endpt p (ctx-refl Γ) ≡ Γ
-ctx-endpt-refl {[]} p = refl
-ctx-endpt-refl {A ∷ Γ} p = cong₂ _∷_  (ty-endpt-refl p) (ctx-endpt-refl p)
-
--- open Ctx
-
--- TyCtx : iCtx → Type (ℓ-suc ℓ-zero)
--- TyCtx Ξ = Ctx (Ty Ξ)
-
--- -- Endpoints of a full context
--- ctx-endpt : endpt-fun TyCtx
--- ctx-endpt p = Context.map (ty-endpt p)
-
--- CompCtx : (Δ Γ : TyCtx Full)
---         -> (pf : ctx-endpt l Δ ≡ ctx-endpt r Γ)
---         -> TyCtx Full
--- CompCtx Δ Γ pf .var = Δ .var
--- CompCtx Δ Γ pf .isFinSetVar = Δ .isFinSetVar
--- CompCtx Δ Γ pf .el x = comp (Δ .el x)
---                             (Γ .el (transport (cong var pf) x))
---                             λ i → pf i .el (transport-filler (cong var pf) x i)
-
--- -- -- "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 _∋_
-
--- -- ∋-ctx-endpt : {Γ : Ctx Full} {c : Ty Full} -> (p : Interval) ->
--- --   (Γ ∋ c) -> ((ctx-endpt p Γ) ∋ (ty-endpt p c))
--- -- ∋-ctx-endpt p vz = vz
--- -- ∋-ctx-endpt p (vs Γ∋c) = vs (∋-ctx-endpt p Γ∋c)
-
-
-
--- -- 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 : TyCtx Empty -> TyCtx Full
--- ctx-refl = Context.map ty-refl
-
--- -- For a given typing context, the endpoints of the corresponding reflexivity precision
--- -- 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)
+  isSetTy : isSet Ty
+  isSetTy = isSetRetract Ty→W W→Ty rtr (isOfHLevelSuc-IW 1 (λ tt → isSet⊎ isSetUnit (isSet⊎ isSetUnit isSetUnit)) tt)
-- 
GitLab