more progress on evaluation contexts, stuck on an upstream issue

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

@@ -40,13 +40,13 @@ record Model ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
     exponentials : Exponentials cat binProd
     binCoprod : BinCoproducts cat
     monad : Monad cat
-    strength : Strength cat term binProd monad
+    strength : Strength cat binProd monad
 
 
   -- 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
+  open StrengthNotation cat binProd monad strength public
 
   𝟙 = term .fst
 

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

@@ -24,7 +24,7 @@ open Functor
 open NatTrans
 open BinProduct
 
-module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : Monad C) where
+module _ (C : Category ℓ ℓ') (bp : BinProducts C) (T : Monad C) where
   -- A is a kind of "lax equivariance"
   -- A × T B → T (A × B)
   StrengthTrans = NatTrans {C = C ×C C} {D = C} (BinProductF C bp ∘F (Id {C = C} ×F T .fst )) (T .fst ∘F BinProductF C bp)
@@ -33,20 +33,25 @@ module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : M
     open Notation _ bp
 
     -- This says the strength interacts well with the unitor
+    -- π₂ ≡ T π₂ ∘ σ
     StrengthUnitor : Type _
-    StrengthUnitor = (λ (a : C .ob) → π₂ {term .fst} {T .fst ⟅ a ⟆}) ≡ λ a → σ .N-ob ((term .fst) , a) ⋆⟨ C ⟩ T .fst ⟪ π₂ ⟫
+    StrengthUnitor = (λ (a : C .ob)(b : C .ob) → π₂ {a} {T .fst ⟅ b ⟆}) ≡ λ a b → σ .N-ob (a , b) ⋆⟨ C ⟩ T .fst ⟪ π₂ ⟫
 
     -- This says the strength interacts well with the associator
+    -- σ ∘ (id × σ) ≡
+    -- T (π₁π₁ , (π2π1 , π2)) ∘ σ ∘ ((π₁ , π1π2) , π2π2)
     StrengthAssoc : Type _
     StrengthAssoc = -- This one is nicer to express as a square along two isos
               (λ (a b c : C .ob) → C .id {a} ×p σ .N-ob (b , c) ⋆⟨ C ⟩ σ .N-ob (a , (b × c)))
               ≡ λ a b c → ((π₁ ,p (π₁ ∘⟨ C ⟩ π₂)) ,p (π₂ ∘⟨ C ⟩ π₂)) ⋆⟨ C ⟩ σ .N-ob ((a × b) , c) ⋆⟨ C ⟩ T .fst ⟪ (π₁ ∘⟨ C ⟩ π₁) ,p ((π₂ ∘⟨ C ⟩ π₁) ,p π₂) ⟫
-
     open IsMonad
     -- This says the strength interacts well with the unit
+    -- η ≡ σ ∘ (id × η)
     StrengthUnit : Type _
     StrengthUnit = (λ (a b : C .ob) → T .snd .η .N-ob (a × b)) ≡ λ a b → (C .id ×p T .snd .η .N-ob b) ⋆⟨ C ⟩ σ .N-ob _
 
+    -- μ ∘ T σ ∘ σ
+    -- σ ∘ (id × μ)
     StrengthMult : Type _
     StrengthMult =
       (λ (a b : C .ob) → σ .N-ob (a , (T .fst ⟅ b ⟆)) ⋆⟨ C ⟩ T .fst ⟪ σ .N-ob (a , b) ⟫ ⋆⟨ C ⟩ T .snd .μ .N-ob _)
@@ -62,6 +67,8 @@ module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : M
     open Notation _ bp renaming (_×_ to _×c_)
     σ = str .fst
 
+    strength-𝟙 : StrengthUnitor σ
+    strength-𝟙 = str .snd .fst
 
     strength-η : StrengthUnit σ
     strength-η = str .snd .snd .snd .fst

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

@@ -27,10 +27,10 @@ open BinProduct
 open IsMonad
 
 --
-module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : Monad C) (s : Strength C term bp T) where
+module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : Monad C) (s : Strength C bp T) where
   module C = Category C
   open Notation C bp
-  open StrengthNotation C term bp T s
+  open StrengthNotation C bp T s
   module _ (Γ : C .ob) where
     KleisliSlice : Category ℓ ℓ'
     KleisliSlice .ob = C .ob
@@ -55,13 +55,32 @@ module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : M
       ∙ C.⋆Assoc _ _ _
       ∙ cong (C._∘ g) (λ i → T .snd .idl-μ i .N-ob _)
       ∙ C.⋆IdR g
-    -- μ ∘ T (T η ∘ π₂) ∘ σ ∘ (π₁ , f)
-    -- μ ∘ T^2 η ∘ T π₂ ∘ σ ∘ (π₁ , f)
-    -- T η ∘ μ ∘ T π₂ ∘ σ ∘ (π₁ , f)
+    KleisliSlice .⋆IdR f =
+    -- μ ∘ T (η ∘ π₂) ∘ σ ∘ (π₁ , f)
+      cong₂ C._∘_ (cong₂ C._∘_ refl (T .fst .F-seq _ _)) refl
+    -- μ ∘ T η ∘ T π₂ ∘ σ ∘ (π₁ , f)
+      ∙ cong₂ C._∘_ (C .⋆Assoc _ _ _) refl
+      ∙ cong₂ C._∘_ (cong₂ C._∘_ (λ i → T .snd .idr-μ i .N-ob _) refl) refl
+      ∙ cong₂ C._∘_ (C .⋆IdR _) refl
     -- T π₂ ∘ σ ∘ (π₁ , f)
+      ∙ C .⋆Assoc _ _ _
+      ∙ cong₂ C._∘_ (λ i → strength-𝟙 (~ i) _ _) refl
+    -- π₂ ∘ (π₁ , f)
+      ∙ ×β₂
     -- ≡ f
-    KleisliSlice .⋆IdR f = {!!}
-    KleisliSlice .⋆Assoc = {!!}
+
+    -- μ ∘ T h ∘ σ ∘ (π₁ , μ ∘ T g ∘ σ ∘ (π1 , f))
+    -- μ ∘ T h ∘ σ ∘ (π₁ ∘ (π₁ , T g ∘ σ ∘ (π1 , f)) , μ ∘ π₂ ∘ (π₁ , T g ∘ σ ∘ (π1 , f)))
+    -- μ ∘ T h ∘ σ ∘ (id ∘ π1 , μ ∘ π2) ∘ (π₁ , T g ∘ σ ∘ (π1 , f))
+    -- μ ∘ T h ∘ σ ∘ (id × μ) ∘ (π₁ , T g ∘ σ ∘ (π1 , f))
+    -- μ ∘ T h ∘ μ ∘ T σ ∘ σ ∘ (π₁ , T g ∘ σ ∘ (π1 , f))
+
+    -- μ ∘ T h ∘ μ ∘ T σ ∘ σ ∘ T (π₁ , g) ∘ σ ∘ (π1 , f)
+    -- μ ∘ T h ∘ μ ∘ T σ ∘ T (π₁ , g) ∘ σ ∘ (π1 , f)
+    -- μ ∘ μ ∘ T^2 h ∘ T σ ∘ T (π₁ , g) ∘ σ ∘ (π1 , f)
+    -- μ ∘ T μ ∘ T^2 h ∘ T σ ∘ T (π₁ , g) ∘ σ ∘ (π1 , f)
+    -- μ ∘ T (μ ∘ T h ∘ σ ∘ (π₁ , g)) ∘ σ ∘ (π1 , f)
+    KleisliSlice .⋆Assoc f g h = {!!}
     KleisliSlice .isSetHom = C.isSetHom
 
   module _ {Δ : C .ob} {Γ : C .ob} where
@@ -69,4 +88,24 @@ module _ (C : Category ℓ ℓ') (term : Terminal C) (bp : BinProducts C) (T : M
     (γ ^*) .F-ob a = a
     (γ ^*) .F-hom f = f C.∘ (γ ×p C.id)
     (γ ^*) .F-id = sym (C.⋆Assoc _ _ _) ∙ cong₂ C._⋆_ (×β₂ ∙ C .⋆IdR π₂) refl
-    (γ ^*) .F-seq f g = {!!}
+    -- T (γ × V) ∘ σ ≡ σ ∘ (γ × T V)
+
+    (γ ^*) .F-seq f g =
+    -- μ ∘ T g ∘ σ ∘ (π₁ , f) ∘ (γ ∘ π₁ , id ∘ π₂)
+      sym (C .⋆Assoc _ _ _)
+      ∙ cong₂ C._∘_ refl (sym (C .⋆Assoc _ _ _))
+      ∙ cong₂ C._∘_ refl (cong₂ C._∘_ refl (,p-natural
+                                           ∙ cong₂ _,p_ ×β₁ (sym (C .⋆IdR _) ∙ cong₂ C._∘_ (sym (T .fst .F-id)) refl)))
+    -- ≡ μ ∘ T g ∘ σ ∘ (π₁ ∘ (γ ∘ π₁ , id ∘ π₂) , f ∘ (γ ∘ π₁ , id ∘ π₂))
+    -- ≡ μ ∘ T g ∘ σ ∘ (γ ∘ π₁ , T id ∘ f ∘ (γ ∘ π₁ , id ∘ π₂))
+      ∙ {!!}
+    -- ≡ μ ∘ T g ∘ σ ∘ (γ ∘ π₁ , T id ∘ π₂) ∘ (π₁ , f ∘ (γ ∘ π₁ , id ∘ π₂))
+    -- ≡ μ ∘ T g ∘ σ ∘ (γ × T id) ∘ (π₁ , f ∘ (γ ∘ π₁ , id ∘ π₂))
+    --
+    -- Problem: naturality of σ isn't behaving correctly because of some stuff we did...
+      ∙ cong₂ C._∘_ refl (cong₂ C._∘_ refl (cong₂ C._∘_ ({!σ .N-hom ?!}) refl ∙ sym (C .⋆Assoc _ _ _))
+                         ∙ C .⋆Assoc _ _ _)
+      ∙ C .⋆Assoc _ _ _
+    -- ≡ μ ∘ T g ∘ T (γ × id) ∘ σ ∘ (π₁ , f ∘ (γ ∘ π₁ , id ∘ π₂))
+      ∙ cong₂ C._∘_ (cong₂ C._∘_ refl (sym (T .fst .F-seq _ _))) refl
+    -- ≡ μ ∘ T (g ∘ (γ ∘ π₁ , id ∘ π₂)) ∘ σ ∘ (π₁ , f ∘ (γ ∘ π₁ , id ∘ π₂))