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