From ac85887301dc69367098f14ac33c3b9762a3edea Mon Sep 17 00:00:00 2001
From: Leon <leon.vatthauer@fau.de>
Date: Mon, 17 Jul 2023 12:32:54 +0200
Subject: [PATCH] Proof that in tosets every monad is strong (given a terminal
object)
---
Toset.agda | 115 +++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 115 insertions(+)
create mode 100644 Toset.agda
diff --git a/Toset.agda b/Toset.agda
new file mode 100644
index 0000000..eb988e0
--- /dev/null
+++ b/Toset.agda
@@ -0,0 +1,115 @@
+open import Level
+
+
+module Toset {o ℓ₁ ℓ₂ e : Level} where
+
+open import Relation.Binary using (TotalOrder)
+open import Categories.Monad
+open import Categories.Monad.Strong
+open import Categories.Category
+open import Categories.Category.Product
+open import Categories.Category.Cartesian
+open import Categories.Category.Cartesian.Monoidal
+open import Categories.Category.Monoidal
+open import Categories.Category.Construction.Thin
+open import Categories.Functor renaming (id to Id)
+open import Categories.NaturalTransformation
+open import Categories.Object.Product
+open import Data.Product renaming (_×_ to _∧_)
+open import Data.Sum
+open import Agda.Builtin.Unit
+open import Poset
+import Relation.Binary.PropositionalEquality as PEq
+
+--*
+-- Proof that in the category 𝐶 induced by a total order 𝑇 every monad is strong (if there exists a terminal object!)
+--*
+
+module _ (𝑇 : TotalOrder o ℓ₁ ℓ₂) where
+ open TotalOrder 𝑇 renaming (poset to 𝑃)
+ open Category (Thin e 𝑃) renaming (id to idC)
+
+ --*
+ -- First we identify products in thin categories then we proof that if there exists a terminal object (i.e. if the toset is bounded)
+ -- the thin category is cartesian
+ --*
+
+ module _ {⊤ : Carrier} (max : ∀ {X} → X ≤ ⊤) where
+ ThinCartesian : Cartesian (Thin e 𝑃)
+ ThinCartesian = record
+ { terminal = record
+ { ⊤ = ⊤
+ ; ⊤-is-terminal = record
+ { ! = max
+ ; !-unique = λ {A} f → lift tt
+ }
+ }
+ ; products = record
+ { product = λ {A} {B} → record
+ { A×B = get-A×B A B
+ ; π₁ = get-π₁
+ ; π₂ = get-π₂
+ ; ⟨_,_⟩ = get-⟨⟩
+ ; project₁ = lift tt
+ ; project₂ = lift tt
+ ; unique = λ {j₁} {h} {i} {j} _ _ → lift tt
+ }
+ }
+ }
+ where
+ open Equiv using () renaming (refl to Crefl)
+ get-A×B : Carrier → Carrier → Carrier
+ get-A×B A B with (total A B)
+ ... | inj₁ A≤B = A
+ ... | inj₂ B≤A = B
+ get-π₁ : ∀ {A B} → (get-A×B A B) ≤ A
+ get-π₁ {A} {B} with (total A B)
+ ... | inj₁ H = refl
+ ... | inj₂ H = H
+ get-π₂ : ∀ {A B} → (get-A×B A B) ≤ B
+ get-π₂ {A} {B} with (total A B)
+ ... | inj₁ H = H
+ ... | inj₂ H = refl
+ get-⟨⟩ : ∀ {A B C} (f : C ≤ A) (g : C ≤ B) → C ≤ get-A×B A B
+ get-⟨⟩ {A} {B} {C} f g with (total A B)
+ ... | inj₁ H = f
+ ... | inj₂ H = g
+
+ -- a cartesian category is always monoidal, we need the monoidal property for strong monad
+ open CartesianMonoidal ThinCartesian using (monoidal)
+
+
+ --*
+ -- The actual proof that every monad is a strong monad
+ -- We only need to construct the natural transformation strength, every other proof is for free
+ --*
+
+ module _ (T : Closure 𝑃) where
+ Monad→StrongMonad : Monad (Thin e 𝑃) → StrongMonad {C = Thin e 𝑃} monoidal
+ Monad→StrongMonad 𝑀 = record
+ { M = 𝑀
+ ; strength = record
+ { strengthen = ntHelper record
+ { η = λ where
+ (A , B) → helper A B
+ ; commute = λ {X} {Y} f → lift tt
+ }
+ ; identityˡ = λ {A} → lift tt
+ ; η-comm = λ {A} {B} → lift tt
+ ; μ-η-comm = λ {A} {B} → lift tt
+ ; strength-assoc = λ {A} {B} {C} → lift tt
+ }
+ }
+ where
+ open Monad 𝑀
+ open Functor F
+ open Monoidal monoidal
+ open Closure (Monad→Closure {𝑃 = 𝑃} 𝑀)
+ -- The helper takes two object (of the product (A,B)) and constructs the strength morphism.
+ -- For this we need to destruct A ≤ B and A ≤ (F₀ B)
+ helper : (A : Carrier) → (B : Carrier) → Functor.₀ (⊗ ∘F (Id ⁂ F)) (A , B) ⇒ ₀ (Functor.₀ ⊗ (A , B))
+ helper A B with (total A B) | (total A (F₀ B))
+ ... | inj₁ H | inj₁ H0 = trans refl extensiveness
+ ... | inj₂ H | inj₁ H0 = H0
+ ... | inj₁ H | inj₂ H0 = trans H0 extensiveness
+ ... | inj₂ H | inj₂ H0 = refl
\ No newline at end of file