blob: d0ed35b50af6dbf187b46e77d2e6e183d71952a0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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 {()}
|
