Implement Nbe for solving substitution equations

formalizations/guarded-cubical/Syntax/IntensionalTerms.agda

@@ -114,7 +114,7 @@ data Val where
 
   -- Do these make sense?
   injectN   : Val [ nat ] dyn
-  injectArr : Val [ S ] (dyn ⇀ dyn) -> Val [ S ] dyn
+  injectArr : Val [ dyn ⇀ dyn ] dyn
   mapDyn : Val [ nat ] nat → Val [ dyn ⇀ dyn ] (dyn ⇀ dyn) → Val [ dyn ] dyn
   --mapDynβn : ?
   --mapDynβf : ?
@@ -134,7 +134,8 @@ data Val where
 _[_]vP = _[_]v
 varP = var
 
-
+↑subst : Subst Δ Γ → Subst (R ∷ Δ) (R ∷ Γ)
+↑subst γ = γ ∘s wk ,s var
 
 data EvCtx where
   ∙E : EvCtx Γ S S
@@ -195,9 +196,9 @@ data Comp where
   -- 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)
+  -- match (S y) Kz (x . Ks) ≡ Ks [ y / x ]
+  matchNatβs : (Kz : Comp Γ S) (Ks : Comp (nat ∷ Γ) S)
+             → matchNat Kz Ks [ wk ,s (suc [ !s ,s var ]v) ]c ≡ Ks
   -- M[x] ≡ match x (M[0/x]) (x. M[S x/x])
   matchNatη : M ≡ matchNat
        (M [ ids ,s (zro [ !s ]v) ]c)
@@ -213,9 +214,11 @@ data Comp where
     
   matchDynβf : (Kn : Comp (nat ∷ Γ) S) (Kf : Comp ((dyn ⇀ dyn) ∷ Γ) S)
                (V : Val Γ (dyn ⇀ dyn)) ->
-    matchDyn Kn Kf [ ids ,s ((injectArr var) [ !s ,s V ]v) ]c ≡
+    matchDyn Kn Kf [ ids ,s (injectArr [ !s ,s V ]v) ]c ≡
     Kf [ ids ,s V ]c
 
+  matchDynSubst : ∀ (M : Comp (nat ∷ Γ) R) (N : Comp ((dyn ⇀ dyn) ∷ Γ) R) (γ : Subst Δ Γ)
+    → matchDyn M N [ ↑subst γ ]c ≡ matchDyn (M [ ↑subst γ ]c) (N [ ↑subst γ ]c)
 {-
   matchDynβf' : (Kn : Comp (nat ∷ Γ) S) (Kf : Comp ((dyn ⇀ dyn) ∷ Γ) S)
                 (V : Val Γ T) (V-up : Val [ T ] (dyn ⇀ dyn)) ->
@@ -227,6 +230,8 @@ data Comp where
   
   -- tick commutes with ev ctxs
   tick-strictness : ∀ {M} -> E [ tick M ]∙ ≡ tick (E [ M ]∙)
+  -- tick subs
+  tickSubst : (tick M) [ γ ]c ≡ tick (M [ γ ]c)
 
   isSetComp : isSet (Comp Γ S)
   -- isPosetComp : Comp⊑ (refl-⊑ctx Γ) (refl-⊑ S) M M'
@@ -339,6 +344,9 @@ subst-naturality {S} {Γ} {Δ} {γ} {γ'} {V} {V'} =
 !s-ext : {γ : Subst Γ []} → γ ≡ δ
 !s-ext = []η ∙ sym []η
 
+ids-sole : ∀ {R} → ids {Γ = R ∷ []} ≡ (!s ,s var)
+ids-sole = ,sη ∙ cong₂ _,s_ []η substId
+
 ,s-nat : (γ ,s V) ∘s δ ≡ ((γ ∘s δ) ,s (V [ δ ]v))
 ,s-nat =
   ,sη ∙ cong₂ _,s_ (∘Assoc ∙ cong₂ (_∘s_) wkβ refl)
@@ -381,6 +389,54 @@ fun-β' M V =
 fun-η' : V ≡ lda (appVal (V [ wk ]v) var)
 fun-η' = fun-η
 
+matchNatβz' : matchNat M N [ γ ,s (zro [ !s ]v) ]c ≡ M [ γ ]c
+matchNatβz' {M = M}{N = N}{γ = γ} =
+  cong (matchNat M N [_]c)
+    (sym (,s-nat ∙ cong₂ _,s_ ∘IdL (sym substAssoc ∙ cong (zro [_]v) []η)))
+  ∙ substAssoc ∙ cong (_[ γ ]c) (matchNatβz _ N)
+
+matchNatβs' : (matchNat M N [ γ ,s (suc [ !s ,s V ]v) ]c) ≡ (N [ γ ,s V ]c)
+matchNatβs' {M = M}{N = N}{γ = γ}{V = V} =
+  cong (matchNat M N [_]c)
+    (sym (,s-nat ∙ cong₂ _,s_ wkβ (sym substAssoc ∙ cong (suc [_]v) (,s-nat ∙ cong₂ _,s_ []η varβ))))
+  ∙ substAssoc ∙ cong (_[ γ ,s V ]c) (matchNatβs M N )
+
+matchNat-nat :
+  matchNat M N [ ↑subst γ ]c
+  ≡ matchNat (M [ γ ]c)
+             (N [ ↑subst γ ]c)
+matchNat-nat {M = M}{N = N}{γ = γ} = matchNatη
+  ∙ cong₂ matchNat
+    (sym substAssoc
+    ∙ cong (matchNat M N [_]c)
+           (,s-nat ∙ cong₂ _,s_ (sym ∘Assoc ∙ cong (γ ∘s_) wkβ ∙ ∘IdR) varβ)
+    ∙ matchNatβz')
+    (sym substAssoc
+    ∙ cong (matchNat M N [_]c)
+      (,s-nat ∙ cong₂ _,s_ (sym ∘Assoc ∙ cong (γ ∘s_) wkβ) varβ)
+    ∙ matchNatβs')
+-- (γ , V) ≡ (γ o π1 , π2) ∘ (ids , V)
+
+,s-separate : (γ ,s V) ≡ (↑subst γ) ∘s (ids ,s V)
+,s-separate {γ = γ} =
+  sym (,s-nat ∙ cong₂ _,s_ (sym ∘Assoc ∙ cong (γ ∘s_) wkβ ∙ ∘IdR) varβ)
+
+matchNat-nat' :
+  matchNat M N [ γ ,s V ]c
+  ≡ matchNat (M [ γ ]c)
+             (N [ ↑subst γ ]c) [ ids ,s V ]c
+matchNat-nat' {M = M}{N = N}{γ = γ}{V = V} =
+  cong (matchNat M N [_]c) ,s-separate
+  ∙ substAssoc ∙ cong (_[ ids ,s V ]c) matchNat-nat
+
+matchDyn-nat' :
+  matchDyn M N [ γ ,s V ]c
+  ≡ matchDyn (M [ ↑subst γ ]c)
+             (N [ ↑subst γ ]c)
+             [ ids ,s V ]c
+matchDyn-nat' {M = M}{N = N}{γ = γ}{V = V} =
+  cong (matchDyn M N [_]c) ,s-separate
+  ∙ substAssoc ∙ cong (_[ ids ,s V ]c) (matchDynSubst _ _ _)
 
 bind-nat : (bind M) [ γ ]e ≡ bind (M [ γ ∘s wk ,s var ]c)
 bind-nat {M = M} {γ = γ} = ret-η ∙ cong bind (cong (_[ ret [ !s ,s var ]c ]∙) (sym substAssoc)
@@ -441,7 +497,7 @@ Pertᴾ→EC (δi ⇀ δo) = bind (ret' (lda (
        ((Pertᴾ→EC δo [ !s ]e) [ ret' var ]∙)))))
 Pertᴾ→EC (PertD δn δf) = bind (matchDyn
   (((Pertᴾ→EC δn [ !s ]e) [ ret' var ]∙) >> ret' (injectN [ wk ]v))
-  (((Pertᴾ→EC δf [ !s ]e) [ ret' var ]∙) >> ret' (injectArr var [ wk ]v)))
+  (((Pertᴾ→EC δf [ !s ]e) [ ret' var ]∙) >> ret' (injectArr [ wk ]v)))
 
 
 -- The four cast rule delay terms are admissible in the syntax
@@ -483,7 +539,7 @@ emb (ci ⇀ co) =
   ((app [ drop2nd ]c) >>
   ((vToE (emb co) [ !s ]e) [ ret' var ]∙)))
 emb inj-nat = injectN
-emb (inj-arr c) = injectArr (emb c)
+emb (inj-arr c) = injectArr [ !s ,s (emb c) ]v
 
 
 -- We can show that emb (c ∘ d) ≡ emb d ∘ emb c

formalizations/guarded-cubical/Syntax/IntensionalTerms/Induction.agda

+module Syntax.IntensionalTerms.Induction where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
+open import Cubical.Data.List
+open import Cubical.Data.Unit
+open import Cubical.Data.Sigma
+
+open import Syntax.IntensionalTerms
+open import Syntax.Types
+
+private
+ variable
+   Δ Γ Θ Z Δ' Γ' Θ' Z' : Ctx
+   R S T U R' S' T' U' : Ty
+
+   γ γ' γ'' : Subst Δ Γ
+   δ δ' δ'' : Subst Θ Δ
+   θ θ' θ'' : Subst Z Θ
+
+   V V' V'' : Val Γ S
+   M M' M'' N N' : Comp Γ S
+   E E' E'' F F' : EvCtx Γ S T
+   ℓ ℓ' ℓ'' ℓ''' ℓ'''' : Level
+
+module SynInd
+  (Ps : ∀ {Δ} {Γ} → Subst Δ Γ → hProp ℓ)
+  (Pv : ∀ {Γ} {R} → Val Γ R → hProp ℓ')
+  (Pc : ∀ {Γ} {R} → Comp Γ R → hProp ℓ'')
+  (Pe : ∀ {Γ R S} → EvCtx Γ R S → hProp ℓ''')
+  where
+
+  record indCases : Type (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ'''))) where
+    field
+      indIds : ⟨ Ps {Γ} ids ⟩
+      ind∘s : ⟨ Ps γ ⟩ → ⟨ Ps θ ⟩ → ⟨ Ps (γ ∘s θ) ⟩
+      ind!s : ⟨ Ps {Δ} !s ⟩
+      ind,s : ⟨ Ps {Θ}{Γ} γ ⟩ → ⟨ Pv {R = R} V ⟩ → ⟨ Ps (γ ,s V) ⟩
+      indwk : ⟨ Ps (wk {S = S}{Γ = Γ}) ⟩
+
+      ind[]v : ⟨ Pv V ⟩ → ⟨ Ps γ ⟩ → ⟨ Pv (V [ γ ]v)⟩
+      indVar : ⟨ Pv {Γ = (R ∷ Γ)} var ⟩
+      indZero : ⟨ Pv zro ⟩
+      indSuc : ⟨ Pv suc ⟩
+      indLda : ⟨ Pc M ⟩ → ⟨ Pv (lda M) ⟩
+      indInjN : ⟨ Pv injectN ⟩
+      indInjArr : ⟨ Pv injectArr ⟩
+      indMapDyn : ⟨ Pv V ⟩ → ⟨ Pv V' ⟩
+                → ⟨ Pv (mapDyn V V') ⟩
+
+      ind[]∙ : ⟨ Pe E ⟩ → ⟨ Pc M ⟩ → ⟨ Pc (E [ M ]∙)⟩
+      ind[]c : ⟨ Pc M ⟩ → ⟨ Ps γ ⟩ → ⟨ Pc (M [ γ ]c)⟩
+      indErr : ⟨ Pc {R = R} err ⟩
+      indTick : ⟨ Pc M ⟩ → ⟨ Pc (tick M) ⟩
+      indRet : ⟨ Pc {R = R} ret ⟩
+      indApp : ⟨ Pc (app {S = S}{T = T}) ⟩
+      indMatchNat : ⟨ Pc M ⟩ → ⟨ Pc M' ⟩ → ⟨ Pc (matchNat M M' )⟩
+      indMatchDyn : ⟨ Pc M ⟩ → ⟨ Pc M' ⟩ → ⟨ Pc (matchDyn M M' )⟩
+
+      ind∙ : ⟨ Pe {Γ}{R} ∙E ⟩
+      ind∘E : ⟨ Pe E ⟩ → ⟨ Pe F ⟩ → ⟨ Pe (E ∘E F) ⟩
+      ind[]e : ⟨ Pe E ⟩ → ⟨ Ps γ ⟩ → ⟨ Pe (E [ γ ]e)⟩
+      indbind : ⟨ Pc M ⟩ → ⟨ Pe (bind M) ⟩
+
+  module _ (ic : indCases) where
+    open indCases ic
+    indPs : ∀ (γ : Subst Δ Γ) → ⟨ Ps γ ⟩
+    indPv : ∀ (V : Val Γ R) → ⟨ Pv V ⟩
+    indPc : ∀ (M : Comp Γ R) → ⟨ Pc M ⟩
+    indPe : ∀ (E : EvCtx Γ R S) → ⟨ Pe E ⟩
+
+    indPs ids = indIds
+    indPs (γ ∘s γ₁) = ind∘s (indPs γ) (indPs γ₁)
+    indPs !s = ind!s
+    indPs (γ ,s V) = ind,s (indPs γ) (indPv V)
+    indPs wk = indwk
+    indPs (∘IdL {γ = γ} i) =
+     isProp→PathP ((λ i → Ps (∘IdL {γ = γ} i) .snd)) (ind∘s indIds (indPs γ)) (indPs γ) i
+    indPs (∘IdR {γ = γ} i) = isProp→PathP (((λ i → Ps (∘IdR {γ = γ} i) .snd)))
+      ((ind∘s (indPs γ) indIds)) ((indPs γ)) i
+    indPs (∘Assoc {γ = γ}{δ = δ}{θ = θ} i) =
+      isProp→PathP (λ i → Ps (∘Assoc {γ = γ} {δ = δ} {θ = θ} i) .snd)
+        (ind∘s (indPs γ) (ind∘s (indPs δ) (indPs θ)))
+        (ind∘s (ind∘s (indPs γ) (indPs δ)) (indPs θ))
+        i
+    indPs ([]η {γ = γ} i) = isProp→PathP (λ i → Ps ([]η {γ = γ} i) .snd)
+      (indPs γ) ind!s i
+    indPs (wkβ {δ = δ}{V = V} i) = isProp→PathP (λ i → Ps (wkβ {δ = δ}{V = V} i) .snd)
+      (ind∘s indwk (ind,s (indPs δ) (indPv V))) (indPs δ) i
+    indPs (,sη {δ = δ} i) = isProp→PathP (λ i → Ps (,sη {δ = δ} i) .snd)
+      (indPs δ) (ind,s (ind∘s indwk (indPs δ)) (ind[]v indVar (indPs δ))) i
+    indPs (isSetSubst γ γ' p q i j) = isOfHLevel→isOfHLevelDep 2 (λ x → isProp→isSet (Ps x .snd))
+      (indPs γ)
+      (indPs γ')
+      (λ j → indPs (p j))
+      (λ j → indPs (q j))
+      (isSetSubst γ γ' p q) i j
+
+    indPv (V [ γ ]v) = ind[]v (indPv V) (indPs γ)
+    indPv var = indVar
+    indPv zro = indZero
+    indPv suc = indSuc
+    indPv (lda M) = indLda (indPc M)
+    indPv injectN = indInjN
+    indPv injectArr = indInjArr
+    indPv (mapDyn V V') = indMapDyn (indPv V) (indPv V')
+    -- avert your eyes
+    indPv (substId {V = V} i) =
+      isProp→PathP (λ i → Pv (substId i) .snd) (ind[]v (indPv V) indIds) (indPv V) i
+    indPv (substAssoc {V = V}{δ = δ}{γ = γ} i) = isProp→PathP (λ i → Pv (substAssoc i) .snd)
+     (ind[]v (indPv V) (ind∘s (indPs δ) (indPs γ)))
+     (ind[]v (ind[]v (indPv V) (indPs δ)) (indPs γ))
+     i
+
+    indPv (varβ {δ = δ}{V = V} i) = isProp→PathP (λ i → Pv (varβ i) .snd)
+      (ind[]v indVar (ind,s (indPs δ) (indPv V)))
+      (indPv V)
+      i
+
+    indPv (fun-η {V = V} i) = isProp→PathP (λ i → Pv (fun-η i) .snd)
+      (indPv V)
+      (indLda (ind[]c indApp (ind,s (ind,s ind!s (ind[]v (indPv V) indwk)) indVar)))
+      i
+    indPv (isSetVal V V' p q i j) = isOfHLevel→isOfHLevelDep 2 (λ x → isProp→isSet (Pv x .snd))
+      (indPv V)
+      (indPv V')
+      (λ j → indPv (p j))
+      (λ j → indPv (q j))
+      (isSetVal V V' p q)
+      i j
+
+    indPc (E [ M ]∙) = ind[]∙ (indPe E) (indPc M)
+    indPc (M [ γ ]c) = ind[]c (indPc M) (indPs γ)
+    indPc err = indErr
+    indPc (tick M) = indTick (indPc M)
+    indPc ret = indRet
+    indPc app = indApp
+    indPc (matchNat M M₁) = indMatchNat (indPc M) (indPc M₁)
+    indPc (matchDyn M M₁) = indMatchDyn (indPc M) (indPc M₁)
+    -- macros did this
+    indPc (plugId {M = M} i) = isProp→PathP (λ i → Pc (plugId i) .snd) (ind[]∙ ind∙ (indPc M)) (indPc M) i
+    indPc (plugAssoc {F = F}{E = E}{M = M} i) = isProp→PathP (λ i → Pc (plugAssoc i) .snd) (ind[]∙ (ind∘E (indPe F) (indPe E)) (indPc M)) (ind[]∙ (indPe F) (ind[]∙ (indPe E) (indPc M))) i
+    indPc (substId {M = M} i) = isProp→PathP (λ i → Pc (substId i) .snd) (ind[]c (indPc M) indIds) (indPc M) i
+    indPc (substAssoc {M = M}{δ = δ}{γ = γ} i) = isProp→PathP (λ i → Pc (substAssoc i) .snd) (ind[]c (indPc M) (ind∘s (indPs δ) (indPs γ))) (ind[]c (ind[]c (indPc M) (indPs δ)) (indPs γ)) i
+    indPc (substPlugDist {E = E}{M = M}{γ = γ} i) = isProp→PathP (λ i → Pc (substPlugDist i) .snd) (ind[]c (ind[]∙ (indPe E) (indPc M)) (indPs γ)) (ind[]∙ (ind[]e (indPe E) (indPs γ)) (ind[]c (indPc M) (indPs γ))) i
+    indPc (strictness {E = E} i) = isProp→PathP (λ i → Pc (strictness i) .snd) (ind[]∙ (indPe E) (ind[]c indErr ind!s)) (ind[]c indErr ind!s) i
+    indPc (ret-β {M = M} i) = isProp→PathP (λ i → Pc (ret-β i) .snd) (ind[]∙ (ind[]e (indbind (indPc M)) indwk) (ind[]c indRet (ind,s ind!s indVar))) (indPc M) i
+    indPc (fun-β {M = M} i) = isProp→PathP (λ i → Pc (fun-β i) .snd) (ind[]c indApp (ind,s (ind,s ind!s (ind[]v (indLda (indPc M)) indwk)) indVar)) (indPc M) i
+    indPc (matchNatβz M N i) = isProp→PathP (λ i → Pc (matchNatβz M N i) .snd) (ind[]c (indMatchNat (indPc M) (indPc N)) (ind,s indIds (ind[]v indZero ind!s))) (indPc M) i
+    indPc (matchNatβs M N i) = isProp→PathP (λ i → Pc (matchNatβs M N i) .snd) (ind[]c (indMatchNat (indPc M) (indPc N)) (ind,s indwk (ind[]v indSuc (ind,s ind!s indVar)))) (indPc N) i
+    indPc (matchNatη {M = M} i) = isProp→PathP (λ i → Pc (matchNatη i) .snd) (indPc M) (indMatchNat (ind[]c (indPc M) (ind,s indIds (ind[]v indZero ind!s))) (ind[]c (indPc M) (ind,s indwk (ind[]v indSuc (ind,s ind!s indVar))))) i
+    indPc (matchDynβn M N V i) = isProp→PathP (λ i → Pc (matchDynβn M N V i) .snd) (ind[]c (indMatchDyn (indPc M) (indPc N)) (ind,s indIds (ind[]v indInjN (ind,s ind!s (indPv V))))) (ind[]c (indPc M) (ind,s indIds (indPv V))) i
+    indPc (matchDynβf M N V i) = isProp→PathP (λ i → Pc (matchDynβf M N V i) .snd) (ind[]c (indMatchDyn (indPc M) (indPc N)) (ind,s indIds (ind[]v indInjArr (ind,s ind!s (indPv V))))) (ind[]c (indPc N) (ind,s indIds (indPv V))) i
+    indPc (matchDynSubst M N γ i) = isProp→PathP (λ i → Pc (matchDynSubst M N γ i) .snd) (ind[]c (indMatchDyn (indPc M) (indPc N)) (ind,s (ind∘s (indPs γ) indwk) indVar)) (indMatchDyn (ind[]c (indPc M) (ind,s (ind∘s (indPs γ) indwk) indVar)) (ind[]c (indPc N) (ind,s (ind∘s (indPs γ) indwk) indVar))) i
+    indPc (tick-strictness {E = E}{M = M} i) = isProp→PathP (λ i → Pc (tick-strictness i) .snd) (ind[]∙ (indPe E) (indTick (indPc M))) (indTick (ind[]∙ (indPe E) (indPc M))) i
+    indPc (tickSubst {M = M}{γ = γ} i) = isProp→PathP (λ i → Pc (tickSubst i) .snd) (ind[]c (indTick (indPc M)) (indPs γ)) (indTick (ind[]c (indPc M) (indPs γ))) i
+    indPc (isSetComp M N p q i j) = isOfHLevel→isOfHLevelDep 2 (λ x → isProp→isSet (Pc x .snd))
+      (indPc M)
+      (indPc N)
+      (λ j → indPc (p j))
+      (λ j → indPc (q j))
+      (isSetComp M N p q)
+      i j
+
+    indPe ∙E = ind∙
+    indPe (E ∘E E₁) = ind∘E (indPe E) (indPe E₁)
+    indPe (E [ γ ]e) = ind[]e (indPe E) (indPs γ)
+    indPe (bind M) = indbind (indPc M)
+    indPe (∘IdL {E = E} i) = isProp→PathP (λ i → Pe (∘IdL i) .snd) (ind∘E ind∙ (indPe E)) (indPe E) i
+    indPe (∘IdR {E = E} i) = isProp→PathP (λ i → Pe (∘IdR i) .snd) (ind∘E (indPe E) ind∙) (indPe E) i
+    indPe (∘Assoc {E = E}{F = F}{F' = F'} i) = isProp→PathP (λ i → Pe (∘Assoc i) .snd) (ind∘E (indPe E) (ind∘E (indPe F) (indPe F'))) (ind∘E (ind∘E (indPe E) (indPe F)) (indPe F')) i
+    indPe (substId {E = E} i) = isProp→PathP (λ i → Pe (substId i) .snd) (ind[]e (indPe E) indIds) (indPe E) i
+    indPe (substAssoc {E = E}{γ = γ}{δ = δ} i) = isProp→PathP (λ i → Pe (substAssoc i) .snd) (ind[]e (indPe E) (ind∘s (indPs γ) (indPs δ))) (ind[]e (ind[]e (indPe E) (indPs γ)) (indPs δ)) i
+    indPe (∙substDist {γ = γ} i) = isProp→PathP (λ i → Pe (∙substDist i) .snd) (ind[]e ind∙ (indPs γ)) (ind∙) i
+    indPe (∘substDist {E = E}{F = F}{γ = γ} i) = isProp→PathP (λ i → Pe (∘substDist i) .snd) (ind[]e (ind∘E (indPe E) (indPe F)) (indPs γ)) (ind∘E (ind[]e (indPe E) (indPs γ)) (ind[]e (indPe F) (indPs γ))) i
+    indPe (ret-η {E = E} i) = isProp→PathP (λ i → Pe (ret-η i) .snd) (indPe E) (indbind (ind[]∙ (ind[]e (indPe E) indwk) (ind[]c indRet (ind,s ind!s indVar)))) i
+    indPe (isSetEvCtx E F p q i j) = isOfHLevel→isOfHLevelDep 2 (λ x → isProp→isSet (Pe x .snd))
+      (indPe E)
+      (indPe F)
+      (λ j → indPe (p j))
+      (λ j → indPe (q j))
+      (isSetEvCtx E F p q)
+      i j

formalizations/guarded-cubical/Syntax/Nbe.agda

 module Syntax.Nbe where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Structure
 open import Cubical.Data.List
 open import Cubical.Data.Unit
 open import Cubical.Data.Sigma
 
 open import Syntax.IntensionalTerms
+open import Syntax.IntensionalTerms.Induction
 open import Syntax.Types
 
 private
@@ -20,6 +23,7 @@ private
    V V' V'' : Val Γ S
    M M' M'' N N' : Comp Γ S
    E E' E'' F F' : EvCtx Γ S T
+   ℓ ℓ' ℓ'' ℓ''' ℓ'''' : Level
 
 -- Part 1: define a semantics of contexts, i.e. every context
 -- gets interpreted as an product of the Value presheaves
@@ -27,35 +31,12 @@ ctx-sem : ∀ (Γ : Ctx) → (Ctx → Type (ℓ-suc ℓ-zero))
 ctx-sem [] Δ      = Unit*
 ctx-sem (A ∷ Γ) Δ = ctx-sem Γ Δ × Val Δ A
 
-data CompNF (Γ : Ctx) : (R : Ty) → Type (ℓ-suc ℓ-zero) where
-  errNF : CompNF Γ R
-  retNF : Val Γ R → CompNF Γ R
-  bindNF : Comp Γ R → CompNF (R ∷ Γ) S → CompNF Γ S
-  tickNF : CompNF Γ R → CompNF Γ R
-  neuNF : Comp Γ R → CompNF Γ R
-
-  -- neuNF is a congruence with respect to equality of Comp
-  neuNF-cong : M ≡ N → neuNF M ≡ neuNF N
-
-  -- strictness :
-
-
-_[_]cnf : CompNF Γ R → Subst Δ Γ → CompNF Δ R
-errNF [ γ ]cnf = errNF
-retNF V [ γ ]cnf = retNF (V [ γ ]v)
-bindNF M Nnf [ γ ]cnf = bindNF (M [ γ ]c) (Nnf [ γ ∘s wk ,s var ]cnf)
-tickNF M [ γ ]cnf = tickNF (M [ γ ]cnf)
-neuNF M [ γ ]cnf = neuNF (M [ γ ]c)
-
-
-
-
 _[_]sem : ctx-sem Γ Δ → Subst Θ Δ → ctx-sem Γ Θ
 _[_]sem {Γ = []} tt* δ = tt*
 _[_]sem {Γ = x ∷ Γ} (γ~ , v) δ = (γ~ [ δ ]sem) , (v [ δ ]v)
 
-wk-ctx-sem : ctx-sem Γ Θ → ctx-sem Γ (R ∷ Θ)
-wk-ctx-sem γ~ = γ~ [ wk ]sem
+↑sem : ctx-sem Γ Θ → ctx-sem (R ∷ Γ) (R ∷ Θ)
+↑sem γ~ = γ~ [ wk ]sem , var
 
 -- Part 2: prove the presheaf semantics is equivalent to the yoneda
 -- embedding (i.e. prove Yoneda preserves cartesian structure)
@@ -64,10 +45,19 @@ reify : ctx-sem Γ Δ → Subst Δ Γ
 reify {Γ = []} γ~ = !s
 reify {Γ = x ∷ Γ} (γ~ , v) = reify γ~ ,s v
 
+reify-natural :
+  ∀ {δ : Subst Θ Δ} {γ~ : ctx-sem Γ Δ} → reify γ~ ∘s δ ≡ reify (γ~ [ δ ]sem)
+reify-natural {Γ = []} = []η
+reify-natural {Γ = R ∷ Γ} =
+  ,s-nat ∙ cong₂ _,s_ reify-natural refl
+
 reflect : Subst Δ Γ → ctx-sem Γ Δ
 reflect {Γ = []} γ = tt*
 reflect {Γ = x ∷ Γ} γ = (reflect (wk ∘s γ)) , (var [ γ ]v)
 
+univ-sem-subst : ctx-sem Γ Γ
+univ-sem-subst = reflect ids
+
 reify<-reflect≡id : (γ : Subst Δ Γ) → reify (reflect γ) ≡ γ
 reify<-reflect≡id {Γ = []} γ = sym []η
 reify<-reflect≡id {Γ = x ∷ Γ} γ = sym (,sη ∙ cong₂ _,s_ (sym (reify<-reflect≡id (wk ∘s γ))) refl)
@@ -76,226 +66,224 @@ reflect<-reify≡id : (γ~ : ctx-sem Γ Δ) → reflect (reify γ~) ≡ γ~
 reflect<-reify≡id {Γ = []} γ~ = refl
 reflect<-reify≡id {Γ = x ∷ Γ} γ~ = ΣPathP (cong reflect wkβ ∙ reflect<-reify≡id (γ~ .fst) , varβ)
 
-
-reifyC : CompNF Γ R -> Comp Γ R
-reifyC errNF = err'
-reifyC (retNF V) = ret' V
-reifyC (bindNF M Nnf) = bind (reifyC Nnf) [ M ]∙
-reifyC (tickNF M) = tick (reifyC M)
-reifyC (neuNF M) = M
-
-{-
-reflectC : Comp Γ R -> CompNF Γ R
-reflectC (E [ M ]∙) = bindNF M {!!}
-reflectC (plugId i) = {!!}
-reflectC (plugAssoc i) = {!!}
-reflectC (M [ γ ]c) = neuNF (M [ γ ]c)
-reflectC (substId i) = {!!}
-reflectC (substAssoc i) = {!!}
-reflectC (substPlugDist i) = {!!}
-reflectC err = errNF
-reflectC (strictness i) = {!!}
-reflectC ret = retNF var
-reflectC (ret-β i) = {!!}
-reflectC app = neuNF app
-reflectC (fun-β i) = {!!}
-reflectC (matchNat M N) = neuNF (matchNat {!!} {!!})
-reflectC (matchNatβz M N i) = {!!}
-reflectC (matchNatβs M N V i) = {!!}
-reflectC (matchNatη i) = {!!}
-reflectC (matchDyn M M₁) = {!!}
-reflectC (matchDynβn M N V i) = {!!}
-reflectC (matchDynβf M N V i) = {!!}
-reflectC (tick M) = tickNF (reflectC M)
-reflectC (tick-strictness i) = {!!}
-reflectC (isSetComp M N p q i j) = {!!}
--}
-
--- bindNF : Comp Γ R → CompNF (R ∷ Γ) S → CompNF Γ S
-
-bindNF' : CompNF Γ R → CompNF (R ∷ Γ) S → CompNF Γ S
-bindNF' errNF K = errNF
-bindNF' (retNF x) K = K [ ids ,s x ]cnf
-bindNF' (bindNF {R = R'} M Nnf) K = bindNF M (bindNF' Nnf (K [ wk ∘s wk ,s var ]cnf))
--- Also works: bindNF M (bindNF (reifyC Nnf) (K [ wk ∘s wk ,s var ]cnf)) 
-bindNF' (tickNF Mnf) K = tickNF (bindNF' Mnf K)
-bindNF' (neuNF M) K = neuNF ((bind (reifyC K)) [ M ]∙) -- correct?
-
-
--- Part 3: give a semantics of terms as "polymorphic transformations"
--- These will all end up being natural but fortunately we don't need that.
-
-ev-sem' : EvCtx Γ R S → ∀ {Θ} → ctx-sem Γ Θ → CompNF Θ R → CompNF Θ S
-comp-sem' : Comp Γ R → ∀ {Θ} → ctx-sem Γ Θ → CompNF Θ R
-
-ev-sem' ∙E x M~ = M~
-ev-sem' (E ∘E F) x M~ = ev-sem' E x (ev-sem' F x M~)
-ev-sem' (∘IdL {E = E} i) x M~ = ev-sem' E x M~
-ev-sem' (∘IdR {E = E} i) x M~ = ev-sem' E x M~
-ev-sem' (∘Assoc {E = E} {F = F} {F' = F'} i) x M~ = ev-sem' E x (ev-sem' F x (ev-sem' F' x M~))
-ev-sem' (E [ γ ]e) x M~ = ev-sem' E (reflect (γ ∘s reify x)) M~ -- could define differently?
-ev-sem' (substId {E = E} i) x M~ = ev-sem' E (pf i) M~
-  where pf : reflect (ids ∘s reify x) ≡ x
-        pf = (cong reflect ∘IdL) ∙ (reflect<-reify≡id x)
-ev-sem' (substAssoc {E = E} {γ = γ} {δ = δ} i) x M~ = ev-sem' E (reflect (pf i)) M~
-  where
-    pf : ((γ ∘s δ) ∘s reify x) ≡ (γ ∘s reify (reflect (δ ∘s reify x)))
-    pf = sym ∘Assoc ∙ cong₂ _∘s_ refl (sym (reify<-reflect≡id _))
--- pf : ((γ ∘s δ) ∘s reify x) ≡
---      (γ ∘ (δ ∘s reify x)) ≡
---      (γ ∘s reify (reflect (δ ∘s reify x)))
-ev-sem' (∙substDist i) x M~ = M~
-ev-sem' (∘substDist {E = E} {F = F} {γ = γ} i) x M~ =
-  ev-sem' E (reflect (γ ∘s reify x)) (ev-sem' F (reflect (γ ∘s reify x)) M~)
-ev-sem' (bind N[x]) x M~ = bindNF (reifyC M~) (comp-sem' N[x] (wk-ctx-sem x , var)) -- ???
-ev-sem' (ret-η i) x M~ = {!!}
-ev-sem' (isSetEvCtx E F p q i j) x M~ = {!!}
-
-
-comp-sem' (E [ M ]∙) x = ev-sem' E x (comp-sem' M x)
-comp-sem' (plugId {M = M} i) x = comp-sem' M x
-comp-sem' (plugAssoc {F = F} {E = E} {M = M} i) x = ev-sem' F x (ev-sem' E x (comp-sem' M x))
-comp-sem' (M [ γ ]c) x = comp-sem' M (reflect (γ ∘s reify x)) -- could define differently?
-comp-sem' (substId {M = M} i) x = {!!}
-comp-sem' (substAssoc {δ = δ} {γ = γ} i) x = {!!}
-comp-sem' (substPlugDist {E = E} {M = M} {γ = γ} i) x =
-  ev-sem' E (reflect (γ ∘s reify x)) (comp-sem' M (reflect (γ ∘s reify x)))
-comp-sem' err x = errNF
-comp-sem' (strictness i) x = {!!}
-comp-sem' ret (_ , V) = retNF V
-comp-sem' (ret-β i) x = {!!}
-comp-sem' app ((_ , Vf) , Vx) = neuNF (app [ !s ,s Vf ,s Vx ]c)
-comp-sem' (fun-β i) x = {!!}
-comp-sem' (matchNat Kz Ks) (x , Vn) = neuNF (matchNat Kz Ks [ reify x ,s Vn ]c)
-comp-sem' (matchNatβz M N i) x = {!!}
-comp-sem' (matchNatβs M N V i) x = {!!}
-comp-sem' (matchNatη i) x = {!!}
-comp-sem' (matchDyn M N) x = {!!}
-comp-sem' (matchDynβn M N V i) x = {!!}
-comp-sem' (matchDynβf M N V i) x = {!!}
-comp-sem' (tick M) x = tickNF (comp-sem' M x)
-comp-sem' (tick-strictness i) x = {!!}
-comp-sem' (isSetComp M N p q i j) x = {!!}
-
-
-subst-sem : Subst Δ Γ → ∀ {Θ} → ctx-sem Δ Θ → ctx-sem Γ Θ
-val-sem : Val Γ R → ∀ {Θ} → ctx-sem Γ Θ → Val Θ R
-comp-sem : Comp Γ R → ∀ {Θ} → ctx-sem Γ Θ → Comp Θ R
-ev-sem : EvCtx Γ R S → ∀ {Θ} → ctx-sem Γ Θ → Comp Θ R → Comp Θ S
-
-subst-sem ids x = x
-subst-sem (γ ∘s δ) x = subst-sem γ (subst-sem δ x)
-subst-sem !s = λ _ → tt*
-subst-sem (γ ,s v) x = (subst-sem γ x) , (val-sem v x)
-subst-sem wk = fst
-
--- these equations should essentially hold by refl
-subst-sem ([]η i) = λ _ → tt*
-subst-sem (∘IdL {γ = γ} i) = subst-sem γ
-subst-sem (∘IdR {γ = γ} i) = subst-sem γ
-subst-sem (∘Assoc {γ = γ} {δ = δ} {θ = θ} i) x = subst-sem γ (subst-sem δ (subst-sem θ x))
-subst-sem (wkβ {δ = δ} {V = V} i) x = subst-sem δ x
-subst-sem (,sη {δ = δ} i) x = subst-sem δ x
-subst-sem (isSetSubst γ γ' p q i j) = {!!}
-
-val-sem (V [ γ ]v) x = val-sem V (subst-sem γ x)
-val-sem var x = x .snd
-val-sem zro x = zro [ !s ]v
-val-sem suc (_ , n) = suc [ !s ,s n ]v
-val-sem (lda M[x]) x = lda (comp-sem M[x] ((x [ wk ]sem) , var))
-
-val-sem injectN (_ , V) = injectN [ !s ,s V ]v
-val-sem (injectArr V) x = {!!}
-val-sem (mapDyn Vn Vf) x = {!!}
-
--- don't bother proving these until you have to
-val-sem (varβ i) x = {!!}
-val-sem (substId i) x = {!!}
-val-sem (substAssoc i) x = {!!}
-val-sem (fun-η i) x = {!!}
-val-sem (isSetVal V V₁ x₁ y i i₁) x = {!!}
-
-comp-sem (E [ M ]∙) x = ev-sem E x (comp-sem M x)
-comp-sem (M [ γ ]c) x = comp-sem M (subst-sem γ x)
-comp-sem err x = err [ !s ]c
-comp-sem ret (_ , v) = ret [ !s ,s v ]c
-comp-sem app ((_ , f) , x) = app [ !s ,s f ,s x ]c
-comp-sem (matchNat Mz Ms) (x , d) =
-  matchNat (comp-sem Mz x)
-           (comp-sem Ms ((x [ wk ]sem) , var))
-           [ ids ,s d ]c 
-comp-sem (matchDyn Mn Md) (x , d) =
-  matchDyn (comp-sem Mn ((x [ wk ]sem) , var))
-           (comp-sem Md ((x [ wk ]sem) , var))
-           [ ids ,s d ]c
-comp-sem (tick M) x =
-  tick (comp-sem M x)
-comp-sem (plugId {M = M} i) x = comp-sem M x
-comp-sem (plugAssoc {F = F} {E = E} {M = M} i) x = ev-sem F x (ev-sem E x (comp-sem M x))
-comp-sem (substId {M = M} i) x = comp-sem M x
-comp-sem (substAssoc {M = M} {δ = δ} {γ = γ} i) x = comp-sem M (subst-sem δ (subst-sem γ x))
-comp-sem (substPlugDist {E = E} {M = M} {γ = γ} i) x = ev-sem E (subst-sem γ x) (comp-sem M (subst-sem γ x))
-comp-sem (strictness {E = E} i) x = {!!}
-
-comp-sem (ret-β i) x = {!!}
-comp-sem (fun-β i) x = {!fun-β!}
-comp-sem (matchNatβz M N i) x = {!!}
-comp-sem (matchNatβs M N V i) x = {!!}
-comp-sem (matchNatη i) x = {!!}
-comp-sem (matchDynβn M N V i) x = {!!}
-comp-sem (matchDynβf M N V i) x = {!!}
-comp-sem (tick-strictness i) x = {!!}
-comp-sem (isSetComp M N p q i j) x = {!!}
-
-ev-sem ∙E x M = M
-ev-sem (E ∘E E₁) x M = ev-sem E x (ev-sem E₁ x M)
-ev-sem (E [ γ ]e) x M = ev-sem E (subst-sem γ x) M
-ev-sem (bind K) x M = bind (comp-sem K ((x [ wk ]sem) , var)) [ M ]∙
-
-ev-sem (∘IdL {E = E} i) x M = ev-sem E x M
-ev-sem (∘IdR {E = E} i) x M = ev-sem E x M
-ev-sem (∘Assoc {E = E} {F = F} {F' = F'} i) x M = ev-sem E x (ev-sem F x (ev-sem F' x M))
-ev-sem (substId {E = E} i) x M = ev-sem E x M
-ev-sem (substAssoc {E = E} {γ = γ} {δ = δ} i) x M = ev-sem E (subst-sem γ (subst-sem δ x)) M
-ev-sem (∙substDist i) x M = M
-ev-sem (∘substDist {E = E} {F = F} {γ = γ} i) x M = ev-sem E (subst-sem γ x) (ev-sem F (subst-sem γ x) M)
-
-ev-sem (ret-η i) x M = {!!}
-ev-sem (isSetEvCtx E F p q i j) x M = {!!}
-
--- Part 4: Show the semantics of terms is equivalent to the yoneda
--- embedding of terms UP TO the equivalence between ctx-sem and Subst.
-
-subst-correct : ∀ (γ : Subst Δ Γ)(δ~ : ctx-sem Δ Θ) → γ ∘s (reify δ~) ≡ reify (subst-sem γ δ~)
-val-correct : ∀ (V : Val Δ S)(δ~ : ctx-sem Δ Θ) → V [ reify δ~ ]v ≡ val-sem V δ~
-comp-correct : ∀ (M : Comp Δ S)(δ~ : ctx-sem Δ Θ) → M [ reify δ~ ]c ≡ comp-sem M δ~
-ev-correct : ∀ (E : EvCtx Δ S R)(δ~ : ctx-sem Δ Θ) → E [ reify δ~ ]e [ M ]∙ ≡ ev-sem E δ~ M
-
-subst-correct ids δ~ = ∘IdL
-subst-correct (γ ∘s γ') δ~ = sym ∘Assoc
-  ∙ cong (γ ∘s_) (subst-correct γ' δ~ )
-  ∙ subst-correct γ _
-subst-correct !s δ~ = []η
--- This is the naturality of ,s we discussed
-subst-correct (γ ,s v) δ~ = {!!}
-subst-correct wk δ~ = wkβ
--- This all should follow by isSet stuff
-subst-correct (∘IdL {γ = γ'} i) δ~ = {!!}
-subst-correct (∘IdR i) δ~ = {!!}
-subst-correct (∘Assoc i) δ~ = {!!}
-subst-correct (isSetSubst γ γ₁ x y i i₁) δ~ = {!!}
-subst-correct ([]η i) δ~ = {!!}
-subst-correct (wkβ i) δ~ = {!!}
-subst-correct (,sη i) δ~ = {!!}
-
-val-correct V δ~ = {!!}
-
-comp-correct M δ~ = {!!}
-ev-correct E δ~ = {!!}
-
--- Part 5: Now we get out a kind of "normalization" proof
-normalize-val : (V : Val Γ S) → Val Γ S
-normalize-val V = val-sem V (reflect ids)
-
-normalize-v-correct : ∀ (V : Val Γ S) → V ≡ normalize-val V
-normalize-v-correct V = (sym substId ∙ cong (V [_]v) (sym (reify<-reflect≡id _))) ∙ val-correct V (reflect ids)
+-- Part 3:
+--
+-- Give a semantics of terms as "polymorphic transformations"
+-- Simultaneously prove the correctness of this translation.
+
+-- By proving correctness we can make the goal be contractible,
+-- eliminating the need to prove we respect equations!
+
+-- ordinary:
+-- M : Comp Θ R
+-- K : Comp (Θ , R) S
+
+-- compromise: β but not η...
+-- module _ where
+--   module Bind = SynInd (λ _ → (Unit , isPropUnit)) (λ _ → (Unit , isPropUnit))
+--     (λ {Γ}{R} M → (∀ {Δ}{S} (K : ∀ {Θ}(δv~ : ctx-sem (R ∷ Δ) Θ) → Comp Θ S) → (δ~ : ctx-sem Δ Γ) → singl (bind (K ((δ~ [ wk ]sem) , var)) [ M ]∙))
+--     , isPropImplicitΠ2 (λ _ _ → isPropΠ2 (λ _ _ → isPropSingl)))
+--     (λ _ → (Unit , isPropUnit))
+--   open Bind.indCases
+--   open SynInd.indCases
+--   private
+--     c : Bind.indCases
+--     c .indIds = _
+--     c .ind∘s = _
+--     c .ind!s = _
+--     c .ind,s = _
+--     c .indwk = _
+--     c .ind[]v = _
+--     c .indVar = _
+--     c .indZero = _
+--     c .indSuc = _
+--     c .indLda = _
+--     c .indInjN = _
+--     c .indInjArr = _
+--     c .indMapDyn = _
+
+--     c .ind[]∙ _ ihM K δ~ = isContrSingl _ .fst
+--     c .ind[]c {M = x₂ [ M ]∙} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = plugId i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = plugAssoc i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = M [ x₂ ]c} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = substId i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = substAssoc i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = substPlugDist i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = err} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = strictness i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = ret} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = ret-β i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = app} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = fun-β i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = matchNat M M₁} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = matchNatβz M M₁ i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = matchNatβs M M₁ V i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = matchNatη i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = matchDyn M M₁} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = matchDynβn M M₁ V i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = matchDynβf M M₁ V i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = tick M} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = tick-strictness i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = tickSubst i} x x₁ K δ~ = {!!}
+--     c .ind[]c {M = isSetComp M M₁ x₂ y i i₁} x x₁ K δ~ = {!!}
+--     c .indErr = {!!}
+--     c .indTick = {!!}
+--     c .indRet = {!!}
+--     c .indApp = {!!}
+--     c .indMatchNat = {!!}
+--     c .indMatchDyn = {!!}
+--     c .ind∙ = {!!}
+--     c .ind∘E = {!!}
+--     c .ind[]e = {!!}
+--     c .indbind = {!!}
+--   sem-bind = Bind.indPc c
+
+SubstSem : ∀ (γ : Subst Δ Γ) → hProp _
+SubstSem γ .fst = ∀ {Θ}(δ~ : ctx-sem _ Θ) → singl (reflect (γ ∘s reify δ~))
+SubstSem γ .snd = isPropImplicitΠ λ _ → isPropΠ λ _ → isPropSingl
+
+ValSem : ∀ (V : Val Γ R) → hProp _
+ValSem V .fst = ∀ {Θ}(γ~ : ctx-sem _ Θ) → singl (V [ reify γ~ ]v)
+ValSem V .snd = isPropImplicitΠ λ _ → isPropΠ λ _ → isPropSingl
+
+CompSem : ∀ (M : Comp Γ R) → hProp _
+CompSem M .fst = ∀ {Θ}(γ~ : ctx-sem _ Θ) → singl (M [ reify γ~ ]c)
+CompSem M .snd = isPropImplicitΠ λ _ → isPropΠ λ _ → isPropSingl
+
+EvCtxSem : ∀ (E : EvCtx Γ R S) → hProp _
+EvCtxSem E .fst = ∀ {Θ}(γ~ : ctx-sem _ Θ)(M : Comp _ _) → singl (E [ reify γ~ ]e [ M ]∙)
+EvCtxSem E .snd = isPropImplicitΠ λ _ → isPropΠ2 λ _ _ → isPropSingl
+
+module Sem = SynInd SubstSem ValSem CompSem EvCtxSem
+
+open SynInd.indCases
+sem-cases : Sem.indCases
+sem-cases .indIds δ~ .fst = δ~
+sem-cases .indIds δ~ .snd = cong reflect ∘IdL
+   ∙ reflect<-reify≡id _
+sem-cases .ind∘s ih ih' δ~ .fst = ih (ih' δ~ .fst) .fst
+sem-cases .ind∘s ih ih' δ~ .snd =
+  (cong reflect (sym ∘Assoc ∙ cong (_ ∘s_) (sym (reify<-reflect≡id _)))
+  ∙ ih _ .snd)
+  ∙ cong (λ x → ih x .fst) (ih' δ~ .snd)
+sem-cases .ind!s δ~ .fst = tt*
+sem-cases .ind!s δ~ .snd = refl
+sem-cases .ind,s ihγ ihV δ~ .fst =
+  ihγ δ~ .fst , ihV δ~ .fst 
+sem-cases .ind,s ihγ ihV δ~ .snd = ΣPathP
+  ( (cong reflect (∘Assoc ∙ cong₂ _∘s_ wkβ refl)
+    ∙ ihγ δ~ .snd)
+  , substAssoc
+    ∙ cong _[ reify δ~ ]v varβ
+    ∙ ihV δ~ .snd
+  )
+sem-cases .indwk δ~ .fst = δ~ .fst
+sem-cases .indwk δ~ .snd =
+  cong reflect wkβ
+  ∙ reflect<-reify≡id _
+
+sem-cases .ind[]v ihV ihγ γ~ .fst =
+  ihV (ihγ γ~ .fst) .fst
+sem-cases .ind[]v {V = V} ihV ihγ γ~ .snd =
+  sym substAssoc
+  ∙ cong (V [_]v) (sym (reify<-reflect≡id _))
+  ∙ ihV _ .snd ∙ cong (λ x → ihV x .fst) (ihγ _ .snd)
+sem-cases .indVar γ~ .fst = γ~ .snd
+sem-cases .indVar γ~ .snd = varβ
+
+sem-cases .indRet γ~ = isContrSingl _ .fst
+sem-cases .indApp γ~ = isContrSingl _ .fst
+sem-cases .indErr γ~ = isContrSingl _ .fst
+sem-cases .indZero γ~ = isContrSingl _ .fst
+sem-cases .indSuc γ~ = isContrSingl _ .fst
+sem-cases .indInjN γ~ = isContrSingl _ .fst
+sem-cases .indInjArr γ~ = isContrSingl _ .fst
+
+sem-cases .indLda ihM[x] γ~ .fst =
+  lda (ihM[x] (↑sem γ~) .fst)
+sem-cases .indLda {M = M} ihM[x] γ~ .snd =
+  lda-nat _ _
+  ∙ cong lda (cong (M [_]c) (cong₂ _,s_ reify-natural refl))
+  ∙ cong lda (ihM[x] _ .snd)
+sem-cases .indMapDyn ihVn ihVd γ~ .fst = mapDyn (ihVn (tt* , var) .fst) (ihVd (tt* , var) .fst) [ !s ,s γ~ .snd ]v
+sem-cases .indMapDyn {V = V}{V' = V'} ihVn ihVd γ~ .snd =
+  cong (_[ !s ,s γ~ .snd ]v) (cong₂ mapDyn
+    (sym substId ∙ cong (V [_]v) ids-sole ∙ ihVn (tt* , var) .snd)
+    (sym substId ∙ cong (V' [_]v) ids-sole ∙ ihVd (tt* , var) .snd))
+
+sem-cases .ind[]∙ ihE ihM γ~ .fst = ihE γ~ (ihM γ~ .fst) .fst
+sem-cases .ind[]∙ ihE ihM γ~ .snd =
+  substPlugDist
+  ∙ ihE γ~ _ .snd ∙ cong (λ x → ihE _ x .fst) (ihM _ .snd)
+sem-cases .ind[]c ihM ihγ γ~ .fst =
+  ihM (ihγ γ~ .fst) .fst
+sem-cases .ind[]c {M = M} ihM ihγ γ~ .snd =
+  sym substAssoc ∙ cong (M [_]c) (sym (reify<-reflect≡id _))
+  ∙ ihM _ .snd ∙ cong (λ x → ihM x .fst) (ihγ γ~ .snd)
+sem-cases .indTick ihM γ~ .fst = tick (ihM γ~ .fst)
+sem-cases .indTick ihM γ~ .snd = tickSubst ∙ cong tick (ihM γ~ .snd)
+sem-cases .indMatchNat ihM ihM' γ~ .fst =
+  matchNat (ihM (γ~ .fst) .fst) (ihM' (↑sem (γ~ .fst)) .fst) [ ids ,s γ~ .snd ]c
+sem-cases .indMatchNat {M' = M'} ihM ihM' γ~ .snd =
+  matchNat-nat'
+  ∙ cong (_[ ids ,s γ~ .snd ]c) (cong₂ matchNat (ihM _ .snd)
+    (cong (M' [_]c) (cong (_,s var) reify-natural) ∙ ihM' _ .snd))
+sem-cases .indMatchDyn ihM ihM' γ~ .fst =
+  matchDyn (ihM  (↑sem (γ~ .fst)) .fst)
+           (ihM' (↑sem (γ~ .fst)) .fst)
+           [ ids ,s γ~ .snd ]c
+sem-cases .indMatchDyn {M = M}{M' = M'} ihM ihM' γ~ .snd =
+  matchDyn-nat'
+  ∙ cong (_[ ids ,s γ~ .snd ]c)
+    (cong₂ matchDyn
+      (cong (M  [_]c) (cong (_,s var) reify-natural) ∙ ihM  _ .snd)
+      (cong (M' [_]c) (cong (_,s var) reify-natural) ∙ ihM' _ .snd))
+
+sem-cases .ind∙ γ~ M .fst = M
+sem-cases .ind∙ γ~ M .snd =
+  cong (_[ M ]∙) ∙substDist
+  ∙ plugId
+sem-cases .ind∘E ihE ihF γ~ M .fst =
+  ihE γ~ (ihF γ~ M .fst) .fst
+sem-cases .ind∘E ihE ihF γ~ M .snd =
+  cong (_[ M ]∙) ∘substDist
+  ∙ plugAssoc
+  ∙ ihE γ~ _ .snd
+  ∙ cong (λ x → ihE γ~ x .fst) (ihF _ _ .snd)
+sem-cases .ind[]e ihE ihγ γ~ M .fst =
+  ihE (ihγ γ~ .fst) M .fst
+sem-cases .ind[]e {E = E} ihE ihγ γ~ M .snd =
+  cong (_[ M ]∙) (sym substAssoc)
+  ∙ cong (_[ M ]∙) (cong (E [_]e) (sym (reify<-reflect≡id _)))
+  ∙ ihE _ _ .snd
+  ∙ cong (λ x → ihE x M .fst) (ihγ γ~ .snd)
+-- sem-bind N (λ γ~ → ih-M[x] γ~ .fst) γ~ .fst  
+sem-cases .indbind ih-M[x] γ~ N .fst =
+  bind (ih-M[x] ((γ~ [ wk ]sem) , var) .fst) [ N ]∙
+sem-cases .indbind {M = M} ih-M[x] γ~ N .snd =
+  cong (_[ N ]∙) (bind-nat ∙ cong bind (cong (M [_]c) (cong (_,s var) reify-natural))) -- | TODO: bind natural
+  ∙ (cong (_[ N ]∙)) (cong bind (ih-M[x] _ .snd))
+  -- ∙ sem-bind N (λ γ~ → ih-M[x] γ~ .fst) γ~ .snd
+-- sem-cases .indIds δ~ .fst = δ~
+-- sem-cases .indIds δ~ .snd = cong reflect ∘IdL
+--   ∙ reflect<-reify≡id _
+
+-- | The actual "tactics"
+vsimpl : Val Γ R → Val Γ R
+vsimpl V = Sem.indPv sem-cases V univ-sem-subst .fst
+
+vsimpl-eq : (V : Val Γ R) → V ≡ vsimpl V
+vsimpl-eq V =
+  sym substId
+  ∙ cong (V [_]v) (sym (reify<-reflect≡id _))
+  ∙ Sem.indPv sem-cases V univ-sem-subst .snd
+
+csimpl : Comp Γ R → Comp Γ R
+csimpl M = Sem.indPc sem-cases M univ-sem-subst .fst
+
+csimpl-eq : (M : Comp Γ R) → M ≡ csimpl M
+csimpl-eq M =
+  sym substId
+  ∙ cong (M [_]c) (sym (reify<-reflect≡id _))
+  ∙ Sem.indPc sem-cases M univ-sem-subst .snd