80 lines
2.6 KiB
Agda
80 lines
2.6 KiB
Agda
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
|