From ac004c06239f7dceea40f90427916013f7e9a9a6 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Sat, 15 Jul 2023 16:08:13 +0200
Subject: [PATCH] Initial commit

---
 Poset.agda     | 81 ++++++++++++++++++++++++++++++++++++++++++++++++++
 Poset.agda-lib |  3 ++
 2 files changed, 84 insertions(+)
 create mode 100644 Poset.agda
 create mode 100644 Poset.agda-lib

diff --git a/Poset.agda b/Poset.agda
new file mode 100644
index 0000000..0892d82
--- /dev/null
+++ b/Poset.agda
@@ -0,0 +1,81 @@
+module Poset where
+
+open import Level
+open import Relation.Binary
+open import Categories.Monad
+open import Categories.Category
+open import Categories.Category.Construction.Thin
+open import Categories.Functor renaming (id to Id)
+open import Categories.NaturalTransformation
+open import Data.Product renaming (_×_ to _∧_)
+open import Agda.Builtin.Unit
+
+private
+    variable
+        o ℓ₁ ℓ₂ e : Level
+
+
+-- Definining a closure operator on a poset
+record Closure (𝑃 : Poset o ℓ₁ ℓ₂) : Set (o ⊔ ℓ₁ ⊔ ℓ₂) where
+    open Poset 𝑃 using (Carrier; _≤_; _≈_)
+    field
+        T : Carrier → Carrier
+        extensiveness : ∀ {X : Carrier} → X ≤ T X
+        monotonicity : ∀ {X Y : Carrier} → X ≤ Y → T X ≤ T Y
+        idempotence : ∀ {X : Carrier} → T (T X) ≈ T X
+
+
+--*
+-- Proposition: closure operators on posets are equivalent to monads on the corresponding thin category
+--* 
+
+-- '→'
+Closure→Monad : ∀ {𝑃 : Poset o ℓ₁ ℓ₂} → Closure 𝑃 → Monad {o} {ℓ₂} {e} (Thin e 𝑃)
+Closure→Monad {𝑃 = 𝑃} T = record 
+    { F = F
+    ; η = η'
+    ; μ = μ'
+
+    ; assoc = λ {X} → lift tt
+    ; sym-assoc = λ {X} → lift tt
+    ; identityˡ = λ {X} → lift tt
+    ; identityʳ = λ {X} → lift tt
+    }
+    where
+        open Closure T renaming (T to T₀)
+        open Poset 𝑃 using (Carrier; _≤_; _≈_; reflexive)
+        F = record
+            { F₀ = T₀
+            ; F₁ = monotonicity
+            ; identity = lift tt
+            ; homomorphism = lift tt
+            ; F-resp-≈ = λ {A} {B} {f} {g} _ → lift tt
+            }
+        η' = ntHelper {F = Id} {G = F} record
+            { η = λ X → extensiveness
+            ; commute = λ {X} {Y} f → lift tt
+            }
+        μ' = ntHelper {F = F ∘F F} {G = F} record
+            { η = λ X → reflexive idempotence
+            ; commute = λ {X} {Y} f → lift tt
+            }
+        open NaturalTransformation η'
+        open NaturalTransformation μ' renaming (η to μ)
+
+
+-- '←'
+Monad→Closure : ∀ {𝑃 : Poset o ℓ₁ ℓ₂} → Monad {o} {ℓ₂} {e} (Thin e 𝑃) → Closure 𝑃
+Monad→Closure {𝑃 = 𝑃} 𝑀 = record
+    { T = F₀
+    ; extensiveness = λ {X} → η.η X
+    ; monotonicity = F₁
+    ; idempotence = λ {X} → antisym (μ.η X) (η.η (F₀ X))
+    }
+    where
+        open Poset 𝑃
+        open Monad 𝑀
+        open Functor F
+
+-- full proof
+Closure↔Monad : ∀ {𝑃 : Poset o ℓ₁ ℓ₂} → (Closure 𝑃 → Monad {o} {ℓ₂} {e} (Thin e 𝑃)) ∧ (Monad {o} {ℓ₂} {e} (Thin e 𝑃) → Closure 𝑃)
+Closure↔Monad = Closure→Monad , Monad→Closure
\ No newline at end of file
diff --git a/Poset.agda-lib b/Poset.agda-lib
new file mode 100644
index 0000000..ae471ed
--- /dev/null
+++ b/Poset.agda-lib
@@ -0,0 +1,3 @@
+name: Poset
+include: .
+depend: agda-categories, standard-library
\ No newline at end of file