1 files changed, 18 insertions, 0 deletions
diff --git a/src/CatTheory/Category/Instance/Of/Properties/Preorder.agda b/src/CatTheory/Category/Instance/Of/Properties/Preorder.agda
new file mode 100644
index 0000000..025964f
--- /dev/null
+++ b/src/CatTheory/Category/Instance/Of/Properties/Preorder.agda
@@ -0,0 +1,18 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Bundles using (Preorder)
+
+module CatTheory.Category.Instance.Of.Properties.Preorder
+  {a l₁ l₂}
+  (P : Preorder a l₁ l₂)
+  where
+
+open import CatTheory.Category.Instance.Of.Preorder
+open Preorder P
+open import Categories.Morphism (OfPreorder P)
+
+∀-Mono : ∀ {A B} {f : A ∼ B} → Mono f
+∀-Mono = _
+
+sym⇒retract : ∀ {A B} {f : A ∼ B} {g : B ∼ A} → g RetractOf f
+sym⇒retract = _