blob: 12aa82b8aa6656c0eeff0d44849782069dce41cd (
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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
{-# OPTIONS --without-K --safe #-}
module CatTheory.Exercise1.Contradiction.SetoidsRetractsUnique where
open import Categories.Category using (Category)
open import Categories.Category.Instance.Setoids
import Categories.Morphism as M
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; suc)
open import Function.Equality using (_⟨$⟩_)
open import Function.Structures using (IsInjection)
open import Level using (0ℓ)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)
module Monomorphisms where
open Category (Setoids 0ℓ 0ℓ)
open M (Setoids 0ℓ 0ℓ)
f : setoid Bool ⇒ setoid ℕ
f = record { _⟨$⟩_ = λ { true → 0 ; false → 1 } ; cong = cong _ }
g₁ : setoid ℕ ⇒ setoid Bool
g₁ = record { _⟨$⟩_ = λ { 0 → true ; 1 → false ; (suc (suc _)) → true } ; cong = cong _ }
g₂ : setoid ℕ ⇒ setoid Bool
g₂ = record { _⟨$⟩_ = λ { 0 → true ; 1 → false ; (suc (suc _)) → false } ; cong = cong _ }
g₁∘f≈id : g₁ RetractOf f
g₁∘f≈id {false} refl = refl
g₁∘f≈id {true} refl = refl
g₂∘f≈id : g₂ RetractOf f
g₂∘f≈id {false} refl = refl
g₂∘f≈id {true} refl = refl
g₁≉g₂ : ¬ g₁ ≈ g₂
g₁≉g₂ g₁≈g₂ = contradiction true≡false (λ ())
where
open ≡-Reasoning
true≡false : true ≡ false
true≡false = g₁≈g₂ (refl {x = 3})
|
