commit 484599bb014e82ee5cb43f9c0aa30075570a43d5
Author: Leon Vatthauer <leon.vatthauer@fau.de>
Date:   Sat Jul 15 12:19:40 2023 +0200

    initial commit

diff --git a/ExtensionSystem.agda b/ExtensionSystem.agda
new file mode 100644
index 0000000..6cd6b68
--- /dev/null
+++ b/ExtensionSystem.agda
@@ -0,0 +1,123 @@
+module ExtensionSystem where
+
+open import Level
+open import Function using (_$_)
+open import Data.Product renaming (_×_ to _∧_)
+open import Categories.Category
+open import Categories.Functor renaming (id to Id)
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Categories.Monad
+open import Categories.NaturalTransformation
+
+-- formalizing the notion 'extension system', formerly known as 'kleisli-triple' and proving that it is equivalent to a monad
+-- https://ncatlab.org/nlab/show/extension+system
+
+private
+    variable
+        o ℓ e : Level
+
+
+-- typedef, an extensionsystem is a specilization of RMonad
+ExtensionSystem : (𝒞 : Category o ℓ e) → Set (o ⊔ ℓ ⊔ e)
+ExtensionSystem 𝒞 = (RMonad (Id {C = 𝒞}))
+
+
+--*
+-- Proposition: ExtensionSystem is an equivalent definition of monad
+--*
+
+-- '→' 
+ExtensionSystem→Monad : ∀ {𝒞 : Category o ℓ e} → ExtensionSystem 𝒞 → Monad 𝒞
+ExtensionSystem→Monad {𝒞 = 𝒞} 𝐾 = record
+    { F = T
+    ; η = η'
+    ; μ = μ'
+    ; identityˡ = Identityˡ
+    ; identityʳ = K2
+    ; assoc = assoc'
+    ; sym-assoc = sym assoc'
+    }
+    where
+        open RMonad 𝐾 using (unit) renaming (extend to _ᵀ; F₀ to T₀; extend-≈ to ᵀ-≈; identityˡ to K1; identityʳ to K2; assoc to K3)
+        open Category 𝒞 renaming (id to idC)
+        open HomReasoning
+        T : Endofunctor 𝒞
+        T = RMonad⇒Functor 𝐾
+        open Functor T renaming (F₁ to T₁)
+        open Equiv
+        η' = ntHelper {F = Id} {G = T} record
+            { η = λ X → unit
+            ; commute = λ {X} {Y} f → sym K2
+            }
+        μ' = ntHelper {F = T ∘F T} {G = T} record
+            { η = λ X → (idC {A = T₀ X})ᵀ
+            ; commute = λ {X} {Y} f → begin 
+                ((idC ᵀ) ∘ (unit ∘ (unit ∘ f)ᵀ)ᵀ)       ≈⟨ (sym $ K3) ⟩ 
+                (((idC ᵀ) ∘ unit ∘ ((unit ∘ f) ᵀ)) ᵀ)   ≈⟨ ᵀ-≈ sym-assoc ⟩
+                ((((idC ᵀ) ∘ unit) ∘ ((unit ∘ f) ᵀ)) ᵀ) ≈⟨ ᵀ-≈ (∘-resp-≈ˡ K2) ⟩
+                ((idC ∘ ((unit ∘ f) ᵀ)) ᵀ)              ≈⟨ ᵀ-≈ identityˡ ⟩
+                (((unit ∘ f) ᵀ) ᵀ)                      ≈⟨ ᵀ-≈ (sym identityʳ) ⟩
+                ((((unit ∘ f) ᵀ) ∘ idC) ᵀ)              ≈⟨ K3 ⟩ 
+                (unit ∘ f)ᵀ ∘ (idC ᵀ) ∎
+            }
+        open NaturalTransformation η' using () renaming (η to η)
+        open NaturalTransformation μ' using () renaming (η to μ)
+        Identityˡ = λ {X} → begin 
+            (μ X ∘ ((η (T₀ X)) ∘ (η X))ᵀ)             ≈⟨ (sym $ K3) ⟩ 
+            (((idC ᵀ) ∘ η (T₀ X) ∘ η X) ᵀ)            ≈⟨ ᵀ-≈ sym-assoc ⟩
+            ((((idC ᵀ) ∘ η (T₀ X)) ∘ η X) ᵀ)          ≈⟨ ᵀ-≈ (∘-resp-≈ˡ K2) ⟩
+            ((idC ∘ η X) ᵀ)                           ≈⟨ ᵀ-≈ identityˡ ⟩
+            (η X ᵀ)                                   ≈⟨ K1 ⟩
+            idC ∎ 
+        assoc' = λ {X} → begin
+            idC ᵀ ∘ (η _ ∘ idC ᵀ)ᵀ                    ≈⟨ sym K3 ⟩ 
+            (((idC ᵀ) ∘ η (T₀ X) ∘ (idC ᵀ)) ᵀ)        ≈⟨ ᵀ-≈ sym-assoc ⟩
+            ((((idC ᵀ) ∘ η (T₀ X)) ∘ (idC ᵀ)) ᵀ)      ≈⟨ ᵀ-≈ (∘-resp-≈ˡ K2) ⟩
+            ((idC ∘ (idC ᵀ)) ᵀ)                       ≈⟨ ᵀ-≈ identityˡ ⟩
+            ((idC ᵀ) ᵀ)                               ≈⟨ ᵀ-≈ (sym identityʳ) ⟩
+            (((idC ᵀ) ∘ idC) ᵀ)                       ≈⟨ K3 ⟩
+            idC ᵀ ∘ idC ᵀ ∎
+
+-- '←'
+Monad→ExtensionSystem : ∀ {𝒞 : Category o ℓ e} → Monad 𝒞 → ExtensionSystem 𝒞
+Monad→ExtensionSystem {𝒞 = 𝒞} 𝑀 = record
+    { F₀ = T₀
+    ; unit = η _
+    ; extend = λ {X} {Y} f → μ Y ∘ T₁ f
+    -- K1
+    ; identityˡ = M3
+    -- K2
+    ; identityʳ = λ {X} {Y} {f} → begin 
+        (μ Y ∘ T₁ f) ∘ η X                            ≈⟨ assoc ⟩ 
+        (μ Y ∘ T₁ f ∘ η X)                            ≈⟨ ∘-resp-≈ʳ (sym (η-commute _)) ⟩
+        (μ Y ∘ η (T₀ Y) ∘ f)                          ≈⟨ sym-assoc ⟩
+        ((μ Y ∘ η (T₀ Y)) ∘ f)                        ≈⟨ ∘-resp-≈ˡ M2 ⟩
+        (idC ∘ f) ≈⟨ identityˡ ⟩
+        f ∎
+    -- K3
+    ; assoc = λ {X} {Y} {Z} {f} {g} → begin 
+        μ Z ∘ T₁ ((μ Z ∘ T₁ g) ∘ f)                   ≈⟨ ∘-resp-≈ʳ homomorphism ⟩
+        (μ Z ∘ (T₁ (μ Z ∘ T₁ g) ∘ T₁ f))              ≈⟨ ∘-resp-≈ʳ (∘-resp-≈ˡ homomorphism) ⟩ 
+        (μ Z ∘ (T₁ (μ Z) ∘ T₁ (T₁ g)) ∘ T₁ f)         ≈⟨ sym-assoc ⟩ 
+        ((μ Z ∘ T₁ (μ Z) ∘ T₁ (T₁ g)) ∘ T₁ f)         ≈⟨ ∘-resp-≈ˡ sym-assoc ⟩ 
+        (((μ Z ∘ T₁ (μ Z)) ∘ T₁ (T₁ g)) ∘ T₁ f)       ≈⟨ ∘-resp-≈ˡ (∘-resp-≈ˡ M1) ⟩ 
+        (((μ Z ∘ μ (T₀ Z)) ∘ T₁ (T₁ g)) ∘ T₁ f)       ≈⟨ ∘-resp-≈ˡ assoc ⟩ 
+        ((μ Z ∘ μ (T₀ Z) ∘ T₁ (T₁ g)) ∘ T₁ f)         ≈⟨ ∘-resp-≈ˡ (∘-resp-≈ʳ (μ-commute g)) ⟩ 
+        ((μ Z ∘ T₁ g ∘ μ Y) ∘ T₁ f)                   ≈⟨ assoc ⟩ 
+        (μ Z ∘ (T₁ g ∘ μ Y) ∘ T₁ f)                   ≈⟨ ∘-resp-≈ʳ assoc ⟩ 
+        (μ Z ∘ T₁ g ∘ μ Y ∘ T₁ f)                     ≈⟨ sym-assoc ⟩ 
+        (μ Z ∘ T₁ g) ∘ μ Y ∘ T₁ f ∎
+    ; extend-≈ = λ fg → ∘-resp-≈ʳ (T-resp-≈ fg) 
+    }
+    where
+        open Category 𝒞 renaming (id to idC)
+        open Monad 𝑀 using () renaming (F to T; η to η'; μ to μ'; assoc to M1; identityʳ to M2; identityˡ to M3)
+        open Functor T renaming (F₀ to T₀; F₁ to T₁; F-resp-≈ to T-resp-≈)
+        open NaturalTransformation η' using (η) renaming (commute to η-commute)
+        open NaturalTransformation μ' renaming (η to μ; commute to μ-commute)
+        open HomReasoning
+        open Equiv
+
+-- proof:
+ExtensionSystem↔Monad : ∀ {𝒞 : Category o ℓ e} → (Monad 𝒞 → ExtensionSystem 𝒞) ∧ (ExtensionSystem 𝒞 → Monad 𝒞)
+ExtensionSystem↔Monad {𝒞} = (Monad→ExtensionSystem , ExtensionSystem→Monad)
\ No newline at end of file
diff --git a/ExtensionSystem.agda-lib b/ExtensionSystem.agda-lib
new file mode 100644
index 0000000..c868c88
--- /dev/null
+++ b/ExtensionSystem.agda-lib
@@ -0,0 +1,3 @@
+name: ExtensionSystem
+include: . 
+depend: agda-categories standard-library