misc: instance: define Preorders

1 files changed, 58 insertions, 0 deletions

diff --git a/src/CatTheory/Category/Instance/Preorders.agda b/src/CatTheory/Category/Instance/Preorders.agda
new file mode 100644
index 0000000..06b4d60
--- /dev/null
+++ b/src/CatTheory/Category/Instance/Preorders.agda
@@ -0,0 +1,58 @@
+{-# OPTIONS --without-K --safe #-}
+
+module CatTheory.Category.Instance.Preorders where
+
+-- The category of preordered sets and order-preserving maps.
+
+open import Level
+open import Relation.Binary using (Preorder; IsEquivalence; _Preserves_⟶_)
+open import Relation.Binary.Morphism using (IsOrderHomomorphism)
+open import Relation.Binary.Morphism.Bundles using (PreorderHomomorphism)
+import Relation.Binary.Morphism.Construct.Identity as Id
+import Relation.Binary.Morphism.Construct.Composition as Comp
+
+open import Categories.Category
+
+open Preorder renaming (_≈_ to ₍_₎_≈_; _∼_ to ₍_₎_∼_)
+open PreorderHomomorphism using (⟦_⟧; cong)
+
+private
+  variable
+    a₁ a₂ a₃ b₁ b₂ b₃ : Level
+    A B C : Preorder a₁ a₂ a₃
+
+module _ {A : Preorder a₁ a₂ a₃} {B : Preorder b₁ b₂ b₃} where
+
+  infix 4 _≗_
+
+  -- Pointwise equality (on order preserving maps).
+
+  _≗_ : (f g : PreorderHomomorphism A B) → Set (a₁ ⊔ b₂)
+  f ≗ g = ∀ {x} → ₍ B ₎ ⟦ f ⟧ x ≈ ⟦ g ⟧ x
+
+  ≗-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 posets and order-preserving maps.
+
+Preorders : ∀ c ℓ₁ ℓ₂ → Category (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) (c ⊔ ℓ₁ ⊔ ℓ₂) (c ⊔ ℓ₁)
+Preorders c ℓ₁ ℓ₂ = record
+  { Obj       = Preorder c ℓ₁ ℓ₂
+  ; _⇒_       = 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)
+  }