From f23b3c0e5d72d65b60f8eb9611e2ccfff9b99412 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 6 Jan 2022 18:27:05 +0000
Subject: I: 5: b: characterise epimorphisms of OfPreorder

---
 src/CatTheory/Category/Instance/Of/Properties/Preorder.agda | 6 ++++++
 1 file changed, 6 insertions(+)

(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
index 025964f..da9e083 100644
--- a/src/CatTheory/Category/Instance/Of/Properties/Preorder.agda
+++ b/src/CatTheory/Category/Instance/Of/Properties/Preorder.agda
@@ -16,3 +16,9 @@ open import Categories.Morphism (OfPreorder P)
 
 sym⇒retract : ∀ {A B} {f : A ∼ B} {g : B ∼ A} → g RetractOf f
 sym⇒retract = _
+
+∀-Epi : ∀ {A B} {f : A ∼ B} → Epi f
+∀-Epi = _
+
+sym⇒section : ∀ {A B} {f : A ∼ B} {g : B ∼ A} → g SectionOf f
+sym⇒section = _
-- 
cgit v1.2.3