Add non-setoid-based preorders

1 files changed, 58 insertions, 0 deletions

diff --git a/Category/Instance/Preorders/Primitive.agda b/Category/Instance/Preorders/Primitive.agda
new file mode 100644
index 0000000..49b687f
--- /dev/null
+++ b/Category/Instance/Preorders/Primitive.agda
@@ -0,0 +1,58 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Category.Instance.Preorders.Primitive where
+
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Function using (id; _∘_)
+open import Level using (Level; _⊔_; suc)
+open import Preorder.Primitive using (Preorder; module Isomorphism)
+open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; ≃-isEquivalence; module ≃; map-resp-≅)
+
+-- The category of primitive preorders and monotone maps
+
+private
+
+  module _ {c ℓ : Level} where
+
+    identity : {A : Preorder c ℓ} → MonotoneMap A A
+    identity = record
+        { map = id
+        ; mono = id
+        }
+
+    compose : {A B C : Preorder c ℓ} → MonotoneMap B C → MonotoneMap A B → MonotoneMap A C
+    compose f g = record
+        { map = f.map ∘ g.map
+        ; mono = f.mono ∘ g.mono
+        }
+      where
+        module f = MonotoneMap f
+        module g = MonotoneMap g
+
+    compose-resp-≃
+        : {A B C : Preorder c ℓ}
+          {f h : MonotoneMap B C}
+          {g i : MonotoneMap A B}
+        → f ≃ h
+        → g ≃ i
+        → compose f g ≃ compose h i
+    compose-resp-≃ {C = C} {h = h} {g} f≃h g≃i x = ≅.trans (f≃h (map g x)) (map-resp-≅ h (g≃i x))
+      where
+        open MonotoneMap using (map; mono)
+        open Preorder C
+        open Isomorphism C
+
+Preorders : (c ℓ : Level) → Category (suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+Preorders c ℓ = categoryHelper record
+    { Obj = Preorder c ℓ
+    ; _⇒_ = MonotoneMap
+    ; _≈_ = _≃_
+    ; id = identity
+    ; _∘_ = compose
+    ; assoc = λ {f = f} {g h} → ≃.refl {x = compose (compose h g) f}
+    ; identityˡ = λ {f = f} → ≃.refl {x = f}
+    ; identityʳ = λ {f = f} → ≃.refl {x = f}
+    ; equiv = ≃-isEquivalence
+    ; ∘-resp-≈ = λ {f = f} {g h i} → compose-resp-≃ {f = f} {g} {h} {i}
+    }