I: 5: c: show being epic and mono is not sufficient to be isoHEADmaster

1 files changed, 24 insertions, 0 deletions

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 {()}