From 8dd4b315a849aacc4d63d466edb3b634daf300cc Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 5 Jan 2022 19:09:36 +0000
Subject: misc: define OfPreorder category

---
 src/CatTheory/Category/Instance/Of/Preorder.agda | 30 ++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 src/CatTheory/Category/Instance/Of/Preorder.agda

(limited to 'src/CatTheory/Category')

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-≈  = _
+  }
-- 
cgit v1.2.3