{-
Strong monads on cartesian categories as extension systems,
i.e., in terms of unit and bind, deriving the rest of the structure
https://ncatlab.org/nlab/show/extension+system
-}
{-# OPTIONS --safe --lossy-unification #-}
module Cubical.Categories.Monad.Strength.Cartesian.ExtensionSystem where
open import Cubical.Foundations.Prelude
open import Cubical.Categories.Category
open import Cubical.Categories.Functor renaming (𝟙⟨_⟩ to funcId)
open import Cubical.Categories.Limits.BinProduct.More
open import Cubical.Categories.Limits.Terminal
open import Cubical.Categories.Limits.Terminal.More
open import Cubical.Categories.Limits.Cartesian.Base
open import Cubical.Categories.Comonad.Instances.Environment
open import Cubical.Categories.Monad.ExtensionSystem as Monad
open import Cubical.Tactics.CategorySolver.Reflection
private
variable
ℓ ℓ' : Level
module _ {C : Category ℓ ℓ'} (bp : BinProducts C) where
open Category
open BinProductsNotation bp
-- open EnvNotation bp
private
variable
Γ Δ a b c : C .ob
γ δ : C [ Δ , Γ ]
f g : C [ a , b ]
-- s t : With Γ [ a , b ]
-- TODO: reformulate this stuff in terms of Displayed categories.
--
-- This is what Jacobs calls the "simple fibration"
-- -- Env [ γ ][ a , b ] is a map Δ × a → b
-- -- With is a fibered category over C. With : C → Cat
-- -- A Strong extension system is a section of this bundle of categories
-- open ExtensionSystemFor
-- record StrongExtensionSystem : Type (ℓ-max ℓ ℓ') where
-- field
-- T : C .ob → C .ob
-- systems : ∀ Γ → Monad.ExtensionSystemFor (With Γ) T
-- -- η ∘ (γ × id) ≡ η
-- η-natural : (γ ^*) ⟪ systems Γ .η {a = a} ⟫ ≡ systems Δ .η
-- -- bind f ∘ (γ × id) ≡ bind (f ∘ (γ × id))
-- bind-natural :
-- (γ ^*) ⟪ systems Γ .bind s ⟫ ≡ systems Δ .bind ((γ ^*) ⟪ s ⟫)
-- -- | TODO: resulting η, bind are natural in all arguments
-- -- If C further has a terminal object we get an "underlying monad"
-- -- on C because Envs 𝟙 ≅ Id
-- module _ (term : Terminal C) (SE : StrongExtensionSystem) where
-- open StrongExtensionSystem SE
-- open TerminalNotation C term
-- open CartesianCategoryNotation (C , term , bp)
-- open isIso
-- -- This follows abstractly from showing (𝟙 ×-) is equivalent to
-- -- the identity monad
-- -- we'll just be explicit here
-- E1 = systems 𝟙
-- -- f ∘ π₂
-- toWith1 : C [ a , b ] → With 𝟙 [ a , b ]
-- toWith1 = C ._⋆_ (unitor-l .fst)
-- -- f ∘ (! , id)
-- fromWith1 : With 𝟙 [ a , b ] → C [ a , b ]
-- fromWith1 = C ._⋆_ (unitor-l .snd .inv)
-- fromTo : fromWith1 (toWith1 f) ≡ f
-- fromTo =
-- sym (C .⋆Assoc _ _ _) ∙
-- cong₂ (comp' C) refl (unitor-l .snd .sec) ∙ C .⋆IdL _
-- toFrom : toWith1 (fromWith1 f) ≡ f
-- toFrom =
-- sym (C .⋆Assoc _ _ _) ∙
-- cong₂ (comp' C) refl (unitor-l .snd .ret) ∙ C .⋆IdL _
-- -- TODO: recover a monad on the original category
-- -- General principle would be that you can transport a monad
-- -- along an equivalence of categories...
-- global-ESF : Monad.ExtensionSystemFor C T
-- global-ESF .η = fromWith1 (E1 .η)
-- global-ESF .bind s = fromWith1 (E1 .bind (toWith1 s))
-- global-ESF .bind-r =
-- cong fromWith1 (cong (E1 .bind) toFrom) ∙
-- cong fromWith1 (E1 .bind-r) ∙ ×β₂
-- global-ESF .bind-l {f = f} =
-- -- (f o π₂)^+ ∘ (!,id) ∘ η ∘ (!, id)
-- -- (f o π₂)^+ ∘ (!,η) ∘ η ∘ (!, id)
-- ((C .⋆Assoc _ _ _) ∙ cong₂ (seq' C) refl
-- (sym (C .⋆Assoc _ _ _) ∙
-- cong₂ (seq' C)
-- (,p-natural ∙ cong₂ _,p_ (𝟙η' {g = π₁}) (C .⋆IdR _)) refl ∙
-- E1 .bind-l {f = (toWith1 f)} ))
-- ∙ sym (C .⋆Assoc _ _ _) ∙ cong₂ (comp' C) refl ×β₂ ∙ C .⋆IdL _
-- -- ((f ∘ π₂)^+ ∘ (! , id)) ∘ ((g ∘ π₂)^+ ∘ (! , id))
-- global-ESF .bind-comp {f = f}{g = g} =
-- -- ((f ∘ π₂)^+ ∘ (! , id)) ∘ ((g ∘ π₂)^+ ∘ (! , id))
-- lem -- f ∘𝟙 g = f^+
-- -- ((f ∘ π₂)^+ ∘ (π₁ , (g ∘ π₂)^+)) ∘ (! , id)
-- ∙ cong₂ (seq' C) refl (cong₂ (comp' C) refl
-- (,p-natural ∙ cong₂ _,p_ (𝟙η' {g = π₁}) (C .⋆IdR _)) ∙ E1 .bind-comp)
-- ∙ cong₂ (seq' C) refl (cong (E1 .bind)
-- -- (E1 .bind (toWith1 f)) ∘ (π₁ , (g ∘ π₂))
-- -- ≡ (E1 .bind (toWith f) ∘ g ∘ π₂)
-- ((cong₂ (comp' C) refl (cong₂ _,p_ 𝟙η' (sym (C .⋆IdR _)) ∙
-- sym ,p-natural) ∙ C .⋆Assoc _ _ _) ∙ C .⋆Assoc _ _ _))
-- -- (((f ∘ π₂)^+ ∘ (! , id) ∘ g) ∘ π₂)^+ ∘ (! , id)
-- where
-- lem : comp' C (fromWith1 (E1 .bind (toWith1 f)))
-- (fromWith1 (E1 .bind (toWith1 g))) ≡
-- ((E1 .bind (toWith1 f)) ∘⟨ C ⟩
-- ((!t ,p C .id) ∘⟨ C ⟩ E1 .bind (toWith1 g))) ∘⟨ C ⟩
-- ((!t ,p C .id))
-- lem = solveCat! C
-- StrongMonad→Monad : Monad.ExtensionSystem C
-- StrongMonad→Monad = T , global-ESF
-- -- TODO: once we establish that T is a functor,
-- -- we can show the following is natural
-- σ : C [ Γ × T a , T (Γ × a) ]
-- σ {Γ = Γ} = systems Γ .bind (fromWith1 (E1 .η))
-- module StrongMonadNotation {C : Category ℓ ℓ'}
-- (bp : BinProducts C) (SE : StrongExtensionSystem bp) where
-- open Category
-- open Notation C bp
-- open EnvNotation bp
-- open StrongExtensionSystem SE public
-- private
-- variable
-- Γ Δ a b c : C .ob
-- γ δ : C [ Δ , Γ ]
-- f g : C [ a , b ]
-- s t : With Γ [ a , b ]
-- open Functor
-- PKleisli : C .ob → Category _ _
-- PKleisli Γ = Monad.Kleisli (With Γ) (T , systems Γ)
-- PG : (Γ : C .ob) → Functor (PKleisli Γ) (With Γ)
-- PG Γ = Monad.G ((With Γ)) ((T , systems Γ))
-- bindP : PKleisli Γ [ a , b ] → With Γ [ T a , T b ]
-- bindP {Γ = Γ} = PG Γ .F-hom
-- retP : PKleisli Γ [ a , a ]
-- retP {Γ} = PKleisli Γ .id
-- bindP-comp : bindP f ∘⟨ With Γ ⟩ bindP g ≡ bindP (bindP f ∘⟨ With Γ ⟩ g)
-- bindP-comp {Γ = Γ} = ExtensionSystemFor.bind-comp (systems Γ)
-- bindP-l : bindP f ∘⟨ With Γ ⟩ retP ≡ f
-- bindP-l {Γ = Γ} = ExtensionSystemFor.bind-l (systems Γ)
-- bindP-r : bindP (retP {a = a}) ≡ With Γ .id
-- bindP-r {Γ = Γ} = ExtensionSystemFor.bind-r (systems Γ)
-- open Functor
-- pull : (γ : C [ Δ , Γ ]) → Functor (PKleisli Γ) (PKleisli Δ)
-- pull γ .F-ob = λ z → z
-- pull γ .F-hom f = (γ ^*) ⟪ f ⟫
-- pull γ .F-id = η-natural
-- pull {Δ = Δ} γ .F-seq f g =
-- (γ ^*) .F-seq _ _ ∙ cong₂ (seq' (With Δ)) refl bind-natural