model of types and precision in an abstract model

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

@@ -2,21 +2,23 @@
 module Semantics.Abstract.TermModel.Convenient where
 
 -- A convenient model of the term language is
--- 1. A cartesian closed category
+-- 1. A bicartesian closed category
 -- 2. Equipped with a strong monad
 -- 3. An object modeling the numbers with models of the con/dtors
--- 4. An object modeling the dynamic type with models of the up/dn casts that are independent of the derivation
+-- 4. An object modeling the dynamic type with models of the inj casts
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Categories.Category
 open import Cubical.Categories.Functor
+open import Cubical.Categories.Functors.Constant
+open import Cubical.Categories.NaturalTransformation as NT hiding (NatTrans)
 open import Cubical.Categories.Limits.Terminal
 open import Cubical.Categories.Limits.BinProduct
+open import Cubical.Categories.Limits.BinProduct.More
 open import Cubical.Categories.Limits.BinCoproduct
 open import Cubical.Categories.Monad.Base
 open import Cubical.Categories.Exponentials
 
-open import Cubical.Categories.Presheaf.Representable
 open import Semantics.Abstract.TermModel.Strength
 
 private
@@ -28,7 +30,7 @@ open Functor
 open BinCoproduct
 open BinProduct
 
-record Model ℓ ℓ' ℓ'' : Type (ℓ-suc (ℓ-max ℓ (ℓ-max ℓ' ℓ''))) where
+record Model ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   field
     -- A cartesian closed category
     cat : Category ℓ ℓ'
@@ -36,25 +38,29 @@ record Model ℓ ℓ' ℓ'' : Type (ℓ-suc (ℓ-max ℓ (ℓ-max ℓ' ℓ'')))
     binProd : BinProducts cat
     exponentials : Exponentials cat binProd
     binCoprod : BinCoproducts cat
+    monad : Monad cat
+    strength : Strength cat term binProd monad
 
-  𝟙 = term .fst
 
-  _×_ : (a b : cat .ob) → cat .ob
-  a × b = binProd a b .binProdOb
+  -- TODO: rename Notation and make similar modules for terminal, coprod
+  open Notation cat binProd public
+  open ExpNotation cat binProd exponentials public
+  open StrengthNotation cat term binProd monad strength public
+
+  𝟙 = term .fst
 
   _+_ : (a b : cat .ob) → cat .ob
   a + b = binCoprod a b .binCoprodOb
 
-  _⇒_ : (a b : cat .ob) → cat .ob
-  a ⇒ b = ExponentialF cat binProd exponentials ⟅ a , b ⟆
+  σ1 : {a b : cat .ob} → cat [ a , a + b ]
+  σ1 = binCoprod _ _ .binCoprodInj₁
+  σ2 : {a b : cat .ob} → cat [ b , a + b ]
+  σ2 = binCoprod _ _ .binCoprodInj₂
+  _||_ : {a b c : cat .ob} → cat [ a , c ] → cat [ b , c ] → cat [ a + b , c ]
+  f1 || f2 = binCoprod _ _ .univProp f1 f2 .fst .fst
 
-  field
-    -- with a strong monad
-    monad : Monad cat
-    strength : Strength cat term binProd monad
   T = monad .fst
 
-
   _⇀_ : (a b : cat .ob) → cat .ob
   a ⇀ b = a ⇒ T ⟅ b ⟆
 
@@ -71,3 +77,13 @@ record Model ℓ ℓ' ℓ'' : Type (ℓ-suc (ℓ-max ℓ (ℓ-max ℓ' ℓ'')))
     -- arbitrary morphisms
     inj : cat [ nat + (dyn ⇀ dyn) , dyn ]
     prj : cat [ dyn , T ⟅ nat + (dyn ⇀ dyn) ⟆ ]
+
+    -- and the error of course!
+    -- err : 1 ⇀ A
+    -- naturality says err ≡ T f ∘ err
+    -- not sure if that's exactly right...
+    err : NT.NatTrans (Constant _ _ 𝟙) T
+
+  ℧ : ∀ {Γ d} → cat [ Γ , T ⟅ d ⟆ ]
+  ℧ {Γ} = NT.NatTrans.N-ob err _ ∘⟨ cat ⟩ terminalArrow cat term Γ
+

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

+{-# OPTIONS --cubical #-}
+module Semantics.Abstract.TermModel.Convenient.Semantics where
+
+-- A convenient model of the term language is
+-- 1. A bicartesian closed category
+-- 2. Equipped with a strong monad
+-- 3. An object modeling the numbers with models of the con/dtors
+-- 4. An object modeling the dynamic type with models of the inj casts
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Categories.Category
+open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.BinProduct
+open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Limits.Terminal
+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 Semantics.Abstract.TermModel.Strength
+open import Syntax.Types
+open import Syntax.Terms
+open import Semantics.Abstract.TermModel.Convenient
+
+private
+  variable
+    ℓ ℓ' : Level
+
+open Category
+open Functor
+open NatTrans
+open BinCoproduct
+open BinProduct
+
+private
+ variable
+   R R' S S' : Ty
+
+module _ (M : Model ℓ ℓ') where
+  module M = Model M
+  module T = IsMonad (M.monad .snd)
+  ⇒F = ExponentialF M.cat M.binProd M.exponentials
+  ⟦_⟧ty : Ty → M.cat .ob
+  ⟦ nat ⟧ty = M.nat
+  ⟦ dyn ⟧ty = M.dyn
+  ⟦ S ⇀ T ⟧ty = ⟦ S ⟧ty M.⇀ ⟦ T ⟧ty
+
+  ⟦_⟧e : S ⊑ R → M.cat [ ⟦ S ⟧ty , ⟦ R ⟧ty ]
+  ⟦_⟧p : S ⊑ R → M.cat [ ⟦ R ⟧ty , M.T ⟅ ⟦ S ⟧ty ⟆ ]
+  ⟦_⟧p' : S ⊑ R → M.cat [ M.T ⟅ ⟦ R ⟧ty ⟆ , M.T ⟅ ⟦ S ⟧ty ⟆ ]
+
+
+  ⟦ nat ⟧e = M.cat .id
+  ⟦ dyn ⟧e = M.cat .id
+  -- The most annoying one because it's not from bifunctoriality, more like separate functoriality
+  -- λ f . λ x . x'  <- p x;
+  --             y'  <- app(f,x');
+  --             η (e y')
+  ⟦ c ⇀ d ⟧e     = M.lda ((T.η .N-ob _ ∘⟨ M.cat ⟩ ⟦ d ⟧e) M.∘k
+                         (M.app' (M.π₁ ∘⟨ M.cat ⟩ M.π₁) M.π₂ M.∘sk
+                         (⟦ c ⟧p ∘⟨ M.cat ⟩ M.π₂)))
+  ⟦ inj-nat ⟧e   = M.inj ∘⟨ M.cat ⟩ M.σ1
+  ⟦ inj-arr c ⟧e = M.inj ∘⟨ M.cat ⟩ M.σ2 ∘⟨ M.cat ⟩ ⟦ c ⟧e
+
+  ⟦ nat ⟧p = T.η .N-ob M.nat
+  ⟦ dyn ⟧p = T.η .N-ob M.dyn
+  -- = η ∘ (⟦ c ⟧e ⇒ ⟦ d ⟧p')
+  ⟦ c ⇀ d ⟧p     = T.η .N-ob _ ∘⟨ M.cat ⟩ ⇒F ⟪ ⟦ c ⟧e , ⟦ d ⟧p' ⟫
+  ⟦ inj-nat ⟧p   = (T.η .N-ob _ M.|| M.℧) M.∘k M.prj
+  ⟦ inj-arr c ⟧p = (M.℧ M.|| ⟦ c ⟧p) M.∘k M.prj
+
+  ⟦ c ⟧p' = T.bind .N-ob _ ⟦ c ⟧p

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

@@ -54,3 +54,17 @@ module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : M
   open import Cubical.Data.Sigma
   Strength : Type _
   Strength = Σ[ σ ∈ StrengthTrans ] (StrengthUnitor σ × (StrengthAssoc σ × (StrengthUnit σ × StrengthMult σ)))
+
+  -- The reason strength is useful is because we get "strong bind"
+  -- C [ Γ × a , T b ] → C [ Γ , T a ] → C [ Γ , T b ]
+  module StrengthNotation (str : Strength) where
+    open Notation _ bp renaming (_×_ to _×c_)
+    σ = str .fst
+    -- TODO: move this upstream in Monad.Notation
+    _∘k_ : ∀ {a b c} → C [ b , T .fst ⟅ c ⟆ ] → C [ a , T .fst ⟅ b ⟆ ] → C [ a , T .fst ⟅ c ⟆ ]
+    f ∘k g = (IsMonad.bind (T .snd)) .N-ob _ f ∘⟨ C ⟩ g
+
+    strong-bind : ∀ {Γ a b} → C [ Γ ×c a , T .fst ⟅ b ⟆ ] → C [ Γ , T .fst ⟅ a ⟆ ] → C [ Γ , T .fst ⟅ b ⟆ ]
+    strong-bind f m = f ∘k σ .N-ob _ ∘⟨ C ⟩ (C .id ,p m)
+
+    _∘sk_ = strong-bind