Initial commit

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

Poset.agda-lib

@@ -0,0 +1,3 @@
+name: Poset
+include: .
+depend: agda-categories, standard-library