misc: define OfPreorder category

1 files changed, 30 insertions, 0 deletions

diff --git a/src/CatTheory/Category/Instance/Of/Preorder.agda b/src/CatTheory/Category/Instance/Of/Preorder.agda
new file mode 100644
index 0000000..3e65f20
--- /dev/null
+++ b/src/CatTheory/Category/Instance/Of/Preorder.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Bundles using (Preorder)
+
+module CatTheory.Category.Instance.Of.Preorder
+  {a l₁ l₂}
+  (P : Preorder a l₁ l₂)
+  where
+
+open import Categories.Category using (Category)
+open import Data.Unit using (⊤)
+open import Function using (flip)
+open import Level using (0ℓ)
+open Preorder P
+
+OfPreorder : Category a l₂ 0ℓ
+OfPreorder = record
+  { Obj       = Carrier
+  ; _⇒_       = _∼_
+  ; _≈_       = λ _ _ → ⊤
+  ; id        = refl
+  ; _∘_       = flip trans
+  ; assoc     = _
+  ; sym-assoc = _
+  ; identityˡ = _
+  ; identityʳ = _
+  ; identity² = _
+  ; equiv     = _
+  ; ∘-resp-≈  = _
+  }