WIP on term semantics: substitutions and some of values

formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient.agda

@@ -49,6 +49,12 @@ record Model ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
 
   𝟙 = term .fst
 
+  !t : ∀ {a} → cat [ a , 𝟙 ]
+  !t = terminalArrow cat term _
+
+  𝟙η : ∀ {a} → (f : cat [ a , 𝟙 ]) → f ≡ !t
+  𝟙η f = sym (terminalArrowUnique cat {T = term} f)
+
   _+_ : (a b : cat .ob) → cat .ob
   a + b = binCoprod a b .binCoprodOb
 

formalizations/guarded-cubical/Semantics/Abstract/TermModel/Convenient/Semantics.agda

@@ -17,6 +17,7 @@ open import Cubical.Categories.Limits.BinProduct
 open import Cubical.Categories.Limits.BinCoproduct
 open import Cubical.Categories.Monad.Base
 open import Cubical.Categories.Exponentials
+open import Cubical.Data.List hiding ([_])
 
 open import Semantics.Abstract.TermModel.Strength
 open import Syntax.Types
@@ -36,6 +37,11 @@ open BinProduct
 private
  variable
    R R' S S' : Ty
+   Γ Γ' Δ Δ' : Ctx
+   γ γ' : Subst Δ Γ
+   V V' : Val Γ S
+   E E' F F' : EvCtx Γ R S
+   M M' N N' : Comp Γ S
 
 module _ (M : Model ℓ ℓ') where
   module M = Model M
@@ -71,3 +77,43 @@ module _ (M : Model ℓ ℓ') where
   ⟦ inj-arr c ⟧p = (M.℧ M.|| ⟦ c ⟧p) M.∘k M.prj
 
   ⟦ c ⟧p' = T.bind .N-ob _ ⟦ c ⟧p
+
+  ⟦_⟧ctx : Ctx → M.cat .ob
+  ⟦ [] ⟧ctx = M.𝟙
+  ⟦ A ∷ Γ ⟧ctx = ⟦ Γ ⟧ctx M.× ⟦ A ⟧ty
+
+  -- The term syntax
+  -- substitutions, values, ev ctxts, terms
+
+  ⟦_⟧S : Subst Δ Γ → M.cat [ ⟦ Δ ⟧ctx , ⟦ Γ ⟧ctx ]
+  ⟦_⟧V : Val Γ S → M.cat [ ⟦ Γ ⟧ctx , ⟦ S ⟧ty ]
+  ⟦_⟧E : EvCtx Γ R S → M.cat [ ⟦ Γ ⟧ctx M.× ⟦ R ⟧ty , M.T ⟅ ⟦ S ⟧ty ⟆ ]
+  ⟦_⟧C : Comp Γ S → M.cat [ ⟦ Γ ⟧ctx , M.T ⟅ ⟦ S ⟧ty ⟆ ]
+
+  ⟦ ids ⟧S = M.cat .id
+  ⟦ γ ∘s δ ⟧S = ⟦ γ ⟧S ∘⟨ M.cat ⟩ ⟦ δ ⟧S
+  ⟦ ∘IdL {γ = γ} i ⟧S = M.cat .⋆IdR ⟦ γ ⟧S i
+  ⟦ ∘IdR {γ = γ} i ⟧S = M.cat .⋆IdL ⟦ γ ⟧S i
+  ⟦ ∘Assoc {γ = γ}{δ = δ}{θ = θ} i ⟧S = M.cat .⋆Assoc ⟦ θ ⟧S ⟦ δ ⟧S ⟦ γ ⟧S i
+  ⟦ !s ⟧S = M.!t
+  ⟦ []η {γ = γ} i ⟧S = M.𝟙η ⟦ γ ⟧S i
+  ⟦ γ ,s V ⟧S = ⟦ γ ⟧S M.,p ⟦ V ⟧V
+  ⟦ wk ⟧S = M.π₁
+  ⟦ wkβ {δ = γ}{V = V} i ⟧S = M.×β₁ {f = ⟦ γ ⟧S}{g = ⟦ V ⟧V} i
+  ⟦ ,sη {δ = γ} i ⟧S = M.×η {f = ⟦ γ ⟧S} i
+  ⟦ isSetSubst γ γ' p q i j ⟧S = M.cat .isSetHom ⟦ γ ⟧S ⟦ γ' ⟧S (cong ⟦_⟧S p) (cong ⟦_⟧S q) i j
+
+  ⟦ V [ γ ]v ⟧V = ⟦ V ⟧V ∘⟨ M.cat ⟩ ⟦ γ ⟧S
+  ⟦ substId {V = V} i ⟧V = M.cat .⋆IdL ⟦ V ⟧V i
+  ⟦ substAssoc {V = V}{δ = δ}{γ = γ} i ⟧V = M.cat .⋆Assoc ⟦ γ ⟧S ⟦ δ ⟧S ⟦ V ⟧V i
+  ⟦ var ⟧V = M.π₂
+  ⟦ varβ {δ = γ}{V = V} i ⟧V = M.×β₂ {f = ⟦ γ ⟧S}{g = ⟦ V ⟧V} i
+  ⟦ zro ⟧V = {!!}
+  ⟦ suc ⟧V = {!!}
+  ⟦ lda x ⟧V = {!!}
+  ⟦ fun-η i ⟧V = {!!}
+  ⟦ up S⊑T ⟧V = {!!}
+  ⟦ isSetVal V V' p q i j ⟧V = M.cat .isSetHom ⟦ V ⟧V ⟦ V' ⟧V (cong ⟦_⟧V p) (cong ⟦_⟧V q) i j
+
+  ⟦_⟧E = {!!}
+  ⟦_⟧C = {!!}

formalizations/guarded-cubical/Syntax/Terms.agda

@@ -64,6 +64,7 @@ data Subst where
   ∘IdL : ids ∘s γ ≡ γ
   ∘IdR : γ ∘s ids ≡ γ
   ∘Assoc : γ ∘s (δ ∘s θ) ≡ (γ ∘s δ) ∘s θ
+  isSetSubst : isSet (Subst Δ Γ)
 
   -- [] is terminal
   !s : Subst Γ []