From 9c9e71fcd63bb5f2ce7f6fd3ee54ed51b108bcf2 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 6 Jan 2022 18:35:46 +0000
Subject: I: 5: c: show being epic and mono is not sufficient to be iso

---
 .../Contradiction/EpiAndMonoImpliesIso.agda        | 24 ++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 src/CatTheory/Exercise1/Contradiction/EpiAndMonoImpliesIso.agda

diff --git a/src/CatTheory/Exercise1/Contradiction/EpiAndMonoImpliesIso.agda b/src/CatTheory/Exercise1/Contradiction/EpiAndMonoImpliesIso.agda
new file mode 100644
index 0000000..d0ed35b
--- /dev/null
+++ b/src/CatTheory/Exercise1/Contradiction/EpiAndMonoImpliesIso.agda
@@ -0,0 +1,24 @@
+{-# OPTIONS --without-K --safe #-}
+
+module CatTheory.Exercise1.Contradiction.EpiAndMonoImpliesIso where
+
+open import Data.Bool using (Bool; true; false; _≤_; f≤t)
+open import Data.Bool.Properties using (≤-preorder)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_)
+
+open import CatTheory.Category.Instance.Of.Preorder
+open import CatTheory.Category.Instance.Of.Properties.Preorder ≤-preorder
+open import Categories.Morphism (OfPreorder ≤-preorder)
+
+f : false ≤ true
+f = f≤t
+
+f-epi : Epi f
+f-epi = ∀-Epi {f = f}
+
+f-mono : Mono f
+f-mono = ∀-Mono {f = f}
+
+¬f-iso : ∀ {g : true ≤ false} → ¬ Iso f g
+¬f-iso {()}
-- 
cgit v1.2.3