Add category of preorders

1 files changed, 50 insertions, 0 deletions

diff --git a/Category/Instance/Preorders.agda b/Category/Instance/Preorders.agda
new file mode 100644
index 0000000..7dde3af
--- /dev/null
+++ b/Category/Instance/Preorders.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorders where
+
+import Relation.Binary.Morphism.Construct.Identity as Id
+import Relation.Binary.Morphism.Construct.Composition as Comp
+
+open import Categories.Category using (Category)
+open import Level using (Level; _⊔_; suc)
+open import Relation.Binary using (Preorder; IsEquivalence)
+open import Relation.Binary.Morphism using (PreorderHomomorphism)
+
+open Preorder using (Carrier; module Eq) renaming (_≈_ to ₍_₎_≈_; _≲_ to ₍_₎_≤_)
+open PreorderHomomorphism using (⟦_⟧; cong)
+
+module _ {c₁ c₂ ℓ₁ ℓ₂ e₁ e₂ : Level} {A : Preorder c₁ ℓ₁ e₁} {B : Preorder c₂ ℓ₂ e₂} where
+
+  -- Pointwise equality of monotone maps
+
+  _≗_ : (f g : PreorderHomomorphism A B) → Set (c₁ ⊔ ℓ₂)
+  f ≗ g = {x : Carrier A} → ₍ B ₎ ⟦ f ⟧ x ≈ ⟦ g ⟧ x
+
+  infix 4 _≗_
+
+  ≗-isEquivalence : IsEquivalence _≗_
+  ≗-isEquivalence = record
+    { refl    = Eq.refl B
+    ; sym     = λ f≈g → Eq.sym B f≈g
+    ; trans   = λ f≈g g≈h → Eq.trans B f≈g g≈h
+    }
+
+  module ≗ = IsEquivalence ≗-isEquivalence
+
+-- The category of preorders and monotone maps
+
+Preorders : ∀ c ℓ e → Category (suc (c ⊔ ℓ ⊔ e)) (c ⊔ ℓ ⊔ e) (c ⊔ ℓ)
+Preorders c ℓ e = record
+  { Obj       = Preorder c ℓ e
+  ; _⇒_       = PreorderHomomorphism
+  ; _≈_       = _≗_
+  ; id        = λ {A} → Id.preorderHomomorphism A
+  ; _∘_       = λ f g → Comp.preorderHomomorphism g f
+  ; assoc     = λ {_ _ _ D} → Eq.refl D
+  ; sym-assoc = λ {_ _ _ D} → Eq.refl D
+  ; identityˡ = λ {_ B} → Eq.refl B
+  ; identityʳ = λ {_ B} → Eq.refl B
+  ; identity² = λ {A} → Eq.refl A
+  ; equiv     = ≗-isEquivalence
+  ; ∘-resp-≈  = λ {_ _ C _ h} f≈h g≈i → Eq.trans C f≈h (cong h g≈i)
+  }