diff options
Diffstat (limited to 'src/CatTheory/Category/Instance')
| -rw-r--r-- | src/CatTheory/Category/Instance/Of/Properties/Preorder.agda | 6 |
1 files changed, 6 insertions, 0 deletions
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 = _ |