From 60e43c84effcefcb154aafca087328c9ee2395a4 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 5 Jan 2022 19:20:37 +0000 Subject: I: 4: f: characterise monomorphisms of OfPreorder --- .../Category/Instance/Of/Properties/Preorder.agda | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 src/CatTheory/Category/Instance/Of/Properties/Preorder.agda (limited to 'src/CatTheory/Category/Instance') 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 = _ -- cgit v1.2.3