blob: 30b5264fc30d08d689872864870bf94e4a04d3ee (
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
|
{-# OPTIONS --safe --without-K #-}
module CatTheory.Exercise1.Contradiction.PreordersEqualEqLessEqual where
open import Categories.Category using (Category)
import Categories.Morphism as Morphism
import Categories.Morphism.Properties as Morphismₚ
open import CatTheory.Category.Instance.Preorders using (Preorders)
open import Data.Fin using (Fin; zero; suc)
open import Data.Fin.Properties using (≤-preorder)
open import Data.Nat using (z≤n)
open import Function using (_$_)
open import Function.Equality using (_⟨$⟩_)
open import Level using (0ℓ)
open import Relation.Binary.Morphism.Bundles using (PreorderHomomorphism)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using (contradiction)
open Category (Preorders 0ℓ 0ℓ 0ℓ)
open Morphism (Preorders 0ℓ 0ℓ 0ℓ)
open Morphismₚ (Preorders 0ℓ 0ℓ 0ℓ)
open PreorderHomomorphism using (⟦_⟧; mono)
≡≇≤ : ¬ preorder (Fin 2) ≅ ≤-preorder 2
≡≇≤ ≡≅≤ = contradiction helper λ ()
where
open _≅_ ≡≅≤
open ≡-Reasoning
helper : zero {1} ≡ suc zero
helper = begin
zero ≡˘⟨ isoʳ ⟩
⟦ from ⟧ (⟦ to ⟧ zero) ≡⟨ cong ⟦ from ⟧ (mono to z≤n) ⟩
⟦ from ⟧ (⟦ to ⟧ (suc zero)) ≡⟨ isoʳ ⟩
suc zero ∎
|
