update to extensionsystem version of comonads/strong monads

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

@@ -13,12 +13,14 @@ 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.Terminal.More
 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.Monad.Strength.Cartesian
+open import Cubical.Categories.Monad.ExtensionSystem
+open import Cubical.Categories.Comonad.Instances.Environment
+open import Cubical.Categories.Monad.Strength.Cartesian.ExtensionSystem
 
 private
   variable
@@ -28,7 +30,6 @@ open Category
 open Functor
 open BinCoproduct
 open BinProduct
-open IsMonad
 
 record Model ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   field
@@ -39,21 +40,15 @@ record Model ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
     exponentials : Exponentials cat binProd
     binCoprod : BinCoproducts cat
     -- with a strong monad
-    monad : Monad cat
-    strength : Strength binProd monad
+    monad : StrongExtensionSystem binProd
 
 
   -- TODO: rename Notation and make similar modules for terminal, coprod
   open Notation cat binProd public
   open ExpNotation cat binProd exponentials public
-
-  𝟙 = term .fst
-
-  !t : ∀ {a} → cat [ a , 𝟙 ]
-  !t = terminalArrow cat term _
-
-  𝟙η : ∀ {a} → (f : cat [ a , 𝟙 ]) → f ≡ !t
-  𝟙η f = sym (terminalArrowUnique cat {T = term} f)
+  open TerminalNotation cat term public
+  open StrongMonadNotation binProd monad public
+  open EnvNotation binProd public
 
   _+_ : (a b : cat .ob) → cat .ob
   a + b = binCoprod a b .binCoprodOb
@@ -65,13 +60,12 @@ record Model ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
   _||_ : {a b c : cat .ob} → cat [ a , c ] → cat [ b , c ] → cat [ a + b , c ]
   f1 || f2 = binCoprod _ _ .univProp f1 f2 .fst .fst
 
-  T = monad .fst
-
-  ret : ∀ {a} → cat [ a , T ⟅ a ⟆ ]
-  ret = monad .snd .η .NT.NatTrans.N-ob _
-
   _⇀_ : (a b : cat .ob) → cat .ob
-  a ⇀ b = a ⇒ T ⟅ b ⟆
+  a ⇀ b = a ⇒ T b
+
+  -- TODO: should this go into notation?
+  Linear = PKleisli
+  ClLinear = Kleisli cat (StrongMonad→Monad binProd term monad)
 
   field
     -- a weak model of the natural numbers, but good enough for our syntax
@@ -84,15 +78,19 @@ record Model ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
 
     -- at this point we will model injection and projection as
     -- arbitrary morphisms
-    inj : cat [ nat + (dyn ⇀ dyn) , dyn ]
-    prj : cat [ dyn , T ⟅ nat + (dyn ⇀ dyn) ⟆ ]
+    inj : cat      [ nat + (dyn ⇀ dyn) , dyn ]
+    prj : ClLinear [ dyn , 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
+    err : ∀ {a} → cat [ 𝟙 , a ]
+  ℧ : ∀ {Γ a} → cat [ Γ , T a ]
+  ℧ = err ∘⟨ cat ⟩ !t
 
-  ℧ : ∀ {Γ d} → cat [ Γ , T ⟅ d ⟆ ]
-  ℧ {Γ} = NT.NatTrans.N-ob err _ ∘⟨ cat ⟩ terminalArrow cat term Γ
+  field
+    ℧-homo : ∀ {Γ a b} → (f : Linear Γ [ a , b ])
+           -- define this explicitly as a profunctor?
+           → bind f ∘⟨ cat ⟩ ((cat .id ,p ℧)) ≡ ℧
 

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

-{-# OPTIONS --lossy-unification #-}
-module Semantics.Abstract.TermModel.Convenient.Linear where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Categories.Category
-open import Cubical.Categories.Functor
-open import Cubical.Categories.Monad.Strength.Cartesian
-open import Cubical.Categories.Monad.Kleisli
-open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Base
-open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Morphism
-open import Cubical.Categories.Comonad.Instances.Environment
-
-open import Semantics.Abstract.TermModel.Convenient
-
-private
-  variable
-    ℓ ℓ' : Level
-
-module StrengthNotation (𝓜 : Model ℓ ℓ') where
-  open Model 𝓜
-  open Category cat
-  Linear : ∀ (Γ : ob) → Category _ _
-  Linear Γ = BiKleisli (Env Γ (binProd Γ)) monad (strength-law binProd monad strength Γ)
-
-  ClosedLinear : Category _ _
-  ClosedLinear = Kleisli monad
-
-  wkClosed : ∀ Γ → Functor ClosedLinear (Linear Γ)
-  wkClosed = wkF binProd monad strength
-
-  _^* : ∀ {Δ Γ}(γ : Hom[ Δ , Γ ]) → Functor (Linear Γ) (Linear Δ)
-  γ ^* = change-of-comonad (change-of-base _ _ strength γ)

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

-module Semantics.Abstract.TermModel.Convenient.Linear.Properties where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Categories.Category
-open import Cubical.Categories.Functor
-open import Cubical.Categories.Monad.Strength.Cartesian
-open import Cubical.Categories.Monad.Kleisli
-open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Base
-open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Morphism
-open import Cubical.Categories.DistributiveLaw.ComonadOverMonad.BiKleisli.Morphism.Properties
-open import Cubical.Categories.Comonad.Instances.Environment
-
-open import Semantics.Abstract.TermModel.Convenient
-open import Semantics.Abstract.TermModel.Convenient.Linear
-private
-  variable
-    ℓ ℓ' : Level
-
-module StrengthLemmas (𝓜 : Model ℓ ℓ') where
-  open Model 𝓜
-  open Category cat
-  open Functor
-  open StrengthNotation 𝓜
-
-  private
-    variable
-      Γ Δ a b c : ob
-      γ δ : Hom[ Δ , Γ ]
-      E : Linear Γ [ a , b ]
-  id^* : (id ^*) ⟪ E ⟫ ≡ E
-  id^* {E = E} = cong₂ _∘_ refl (×pF .F-id) ∙ ⋆IdL _
-
-  comp^* : ((γ ∘ δ) ^*) ⟪ E ⟫ ≡ ((δ ^*) ⟪ ((γ ^*) ⟪ E ⟫) ⟫)
-  comp^* {E = E} =
-    cong₂ _∘_ refl (cong₂ _,p_ (sym (⋆Assoc _ _ _) ∙ cong₂ _∘_ refl (sym ×β₁) ∙ ⋆Assoc _ _ _)
-                               (sym ×β₂ ∙ cong₂ _∘_ (sym (⋆IdR _)) refl)
-                   ∙ sym ,p-natural)
-    ∙ (⋆Assoc _ _ _)

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

@@ -23,8 +23,6 @@ open import Cubical.Data.List hiding ([_])
 open import Syntax.Types
 open import Syntax.Terms
 open import Semantics.Abstract.TermModel.Convenient
-open import Semantics.Abstract.TermModel.Convenient.Linear
-open import Semantics.Abstract.TermModel.Convenient.Linear.Properties
 
 private
   variable
@@ -48,10 +46,7 @@ private
 
 module _ (𝓜 : Model ℓ ℓ') where
   module 𝓜 = Model 𝓜
-  module T = IsMonad (𝓜.monad .snd)
   ⇒F = ExponentialF 𝓜.cat 𝓜.binProd 𝓜.exponentials
-  open StrengthNotation 𝓜
-  open StrengthLemmas 𝓜
 
   ⟦_⟧ty : Ty → 𝓜.cat .ob
   ⟦ nat ⟧ty = 𝓜.nat
@@ -59,8 +54,8 @@ module _ (𝓜 : Model ℓ ℓ') where
   ⟦ S ⇀ T ⟧ty = ⟦ S ⟧ty 𝓜.⇀ ⟦ T ⟧ty
 
   ⟦_⟧e : S ⊑ R → 𝓜.cat [ ⟦ S ⟧ty , ⟦ R ⟧ty ]
-  ⟦_⟧p : S ⊑ R → 𝓜.cat [ ⟦ R ⟧ty , 𝓜.T ⟅ ⟦ S ⟧ty ⟆ ]
-  ⟦_⟧p' : S ⊑ R → 𝓜.cat [ 𝓜.T ⟅ ⟦ R ⟧ty ⟆ , 𝓜.T ⟅ ⟦ S ⟧ty ⟆ ]
+  ⟦_⟧p : S ⊑ R → 𝓜.ClLinear [ ⟦ R ⟧ty , ⟦ S ⟧ty ]
+  ⟦_⟧p' : S ⊑ R → 𝓜.cat [ 𝓜.T ⟦ R ⟧ty , 𝓜.T ⟦ S ⟧ty ]
 
   ⟦ nat ⟧e = 𝓜.cat .id
   ⟦ dyn ⟧e = 𝓜.cat .id
@@ -68,20 +63,20 @@ module _ (𝓜 : Model ℓ ℓ') where
   -- λ f . λ x . x'  <- p x;
   --             y'  <- app(f,x');
   --             η (e y')
-  ⟦ c ⇀ d ⟧e     = 𝓜.lda ((𝓜.ret ∘⟨ 𝓜.cat ⟩ ⟦ d ⟧e) ∘⟨ ClosedLinear ⟩
-                         𝓜.app ∘⟨ Linear _ ⟩
-                         wkClosed _ ⟪ ⟦ c ⟧p ⟫)
+  ⟦ c ⇀ d ⟧e     = 𝓜.lda ((𝓜.ClLinear .id ∘⟨ 𝓜.cat ⟩ ⟦ d ⟧e) ∘⟨ 𝓜.ClLinear ⟩
+                         𝓜.app ∘⟨ 𝓜.Linear _ ⟩
+                         {!!})
   ⟦ inj-nat ⟧e   = 𝓜.inj ∘⟨ 𝓜.cat ⟩ 𝓜.σ1
   ⟦ inj-arr c ⟧e = 𝓜.inj ∘⟨ 𝓜.cat ⟩ 𝓜.σ2 ∘⟨ 𝓜.cat ⟩ ⟦ c ⟧e
 
-  ⟦ nat ⟧p = 𝓜.ret
-  ⟦ dyn ⟧p = 𝓜.ret
+  ⟦ nat ⟧p = 𝓜.ClLinear .id
+  ⟦ dyn ⟧p = 𝓜.ClLinear .id
   -- = η ∘ (⟦ c ⟧e ⇒ ⟦ d ⟧p')
-  ⟦ c ⇀ d ⟧p     = 𝓜.ret ∘⟨ 𝓜.cat ⟩ ⇒F ⟪ ⟦ c ⟧e , ⟦ d ⟧p' ⟫
-  ⟦ inj-nat ⟧p   = (𝓜.ret 𝓜.|| 𝓜.℧) ∘⟨ ClosedLinear ⟩ 𝓜.prj
-  ⟦ inj-arr c ⟧p = (𝓜.℧ 𝓜.|| ⟦ c ⟧p) ∘⟨ ClosedLinear ⟩ 𝓜.prj
+  ⟦ c ⇀ d ⟧p     = {!!} -- 𝓜.ret ∘⟨ 𝓜.cat ⟩ ⇒F ⟪ ⟦ c ⟧e , ⟦ d ⟧p' ⟫
+  ⟦ inj-nat ⟧p   = {!!} -- (𝓜.ret 𝓜.|| 𝓜.℧) ∘⟨ 𝓜.ClLinear ⟩ 𝓜.prj
+  ⟦ inj-arr c ⟧p = {!!} -- (𝓜.℧ 𝓜.|| ⟦ c ⟧p) ∘⟨ 𝓜.ClLinear ⟩ 𝓜.prj
 
-  ⟦ c ⟧p' = T.bind .N-ob _ ⟦ c ⟧p
+  ⟦ c ⟧p' = {!!} -- 𝓜.bind .N-ob _ ⟦ c ⟧p
 
   ⟦_⟧ctx : Ctx → 𝓜.cat .ob
   ⟦ [] ⟧ctx = 𝓜.𝟙
@@ -92,8 +87,8 @@ module _ (𝓜 : Model ℓ ℓ') where
 
   ⟦_⟧S : Subst Δ Γ → 𝓜.cat [ ⟦ Δ ⟧ctx , ⟦ Γ ⟧ctx ]
   ⟦_⟧V : Val Γ S → 𝓜.cat [ ⟦ Γ ⟧ctx , ⟦ S ⟧ty ]
-  ⟦_⟧E : EvCtx Γ R S → Linear ⟦ Γ ⟧ctx [ ⟦ R ⟧ty , ⟦ S ⟧ty ]
-  ⟦_⟧C : Comp Γ S → 𝓜.cat [ ⟦ Γ ⟧ctx , 𝓜.T ⟅ ⟦ S ⟧ty ⟆ ]
+  ⟦_⟧E : EvCtx Γ R S → 𝓜.Linear ⟦ Γ ⟧ctx [ ⟦ R ⟧ty , ⟦ S ⟧ty ]
+  ⟦_⟧C : Comp Γ S → 𝓜.cat [ ⟦ Γ ⟧ctx , 𝓜.T ⟦ S ⟧ty ]
 
   ⟦ ids ⟧S = 𝓜.cat .id
   ⟦ γ ∘s δ ⟧S = ⟦ γ ⟧S ∘⟨ 𝓜.cat ⟩ ⟦ δ ⟧S
@@ -120,19 +115,20 @@ module _ (𝓜 : Model ℓ ℓ') where
   ⟦ up S⊑T ⟧V = ⟦ S⊑T .ty-prec  ⟧e ∘⟨ 𝓜.cat ⟩ 𝓜.π₂
   ⟦ isSetVal V V' p q i j ⟧V = 𝓜.cat .isSetHom ⟦ V ⟧V ⟦ V' ⟧V (cong ⟦_⟧V p) (cong ⟦_⟧V q) i j
 
-  ⟦ ∙E ⟧E = Linear _ .id
-  ⟦ E ∘E F ⟧E = ⟦ E ⟧E ∘⟨ Linear _ ⟩ ⟦ F ⟧E
-  ⟦ ∘IdL {E = E} i ⟧E = Linear _ .⋆IdR ⟦ E ⟧E i
-  ⟦ ∘IdR {E = E} i ⟧E = Linear _ .⋆IdL ⟦ E ⟧E i
-  ⟦ ∘Assoc {E = E}{F = F}{F' = F'} i ⟧E = Linear _ .⋆Assoc ⟦ F' ⟧E ⟦ F ⟧E ⟦ E ⟧E i
-  ⟦ E [ γ ]e ⟧E = (⟦ γ ⟧S ^*) ⟪ ⟦ E ⟧E ⟫
-  ⟦ substId {E = E} i ⟧E = id^* {E = ⟦ E ⟧E} i
-  ⟦ substAssoc {E = E}{γ = γ}{δ = δ} i ⟧E = comp^* {γ = ⟦ γ ⟧S} {δ = ⟦ δ ⟧S} {E = ⟦ E ⟧E} i
-  ⟦ ∙substDist {γ = γ} i ⟧E = (⟦ γ ⟧S ^*) .F-id i
-  ⟦ ∘substDist {E = E}{F = F}{γ = γ} i ⟧E = (⟦ γ ⟧S ^*) .F-seq ⟦ F ⟧E ⟦ E ⟧E i
+  ⟦ ∙E ⟧E = 𝓜.Linear _ .id
+  ⟦ E ∘E F ⟧E = ⟦ E ⟧E ∘⟨ 𝓜.Linear _ ⟩ ⟦ F ⟧E
+  ⟦ ∘IdL {E = E} i ⟧E = 𝓜.Linear _ .⋆IdR ⟦ E ⟧E i
+  ⟦ ∘IdR {E = E} i ⟧E = 𝓜.Linear _ .⋆IdL ⟦ E ⟧E i
+  ⟦ ∘Assoc {E = E}{F = F}{F' = F'} i ⟧E = 𝓜.Linear _ .⋆Assoc ⟦ F' ⟧E ⟦ F ⟧E ⟦ E ⟧E i
+  ⟦ E [ γ ]e ⟧E = (𝓜.pull ⟦ γ ⟧S) ⟪ ⟦ E ⟧E ⟫
+  ⟦ substId {E = E} i ⟧E = 𝓜.id^* i ⟪ ⟦ E ⟧E ⟫
+  ⟦ substAssoc {E = E}{γ = γ}{δ = δ} i ⟧E = 𝓜.comp^* ⟦ γ ⟧S ⟦ δ ⟧S i ⟪ ⟦ E ⟧E ⟫
+  ⟦ ∙substDist {γ = γ} i ⟧E = (𝓜.pull ⟦ γ ⟧S) .F-id i
+    
+  ⟦ ∘substDist {E = E}{F = F}{γ = γ} i ⟧E = 𝓜.pull ⟦ γ ⟧S .F-seq ⟦ F ⟧E ⟦ E ⟧E i
   ⟦ bind M ⟧E = ⟦ M ⟧C
   ⟦ ret-η i ⟧E = {!!}
-  ⟦ dn S⊑T ⟧E = wkClosed 𝓜.𝟙 ⟪ ⟦ S⊑T .ty-prec ⟧p ⟫
+  ⟦ dn S⊑T ⟧E = ⟦ S⊑T .ty-prec ⟧p ∘⟨ 𝓜.cat ⟩ 𝓜.π₂
   ⟦ isSetEvCtx E F p q i j ⟧E = 𝓜.cat .isSetHom ⟦ E ⟧E ⟦ F ⟧E (cong ⟦_⟧E p) (cong ⟦_⟧E q) i j
 
-  ⟦_⟧C = {!!}
+  ⟦ M ⟧C = {!M!}