I: 1: b: show ≡ ≇ ≤ in Preorders

1 files changed, 38 insertions, 0 deletions

diff --git a/src/CatTheory/Exercise1/Contradiction/PreordersEqualEqLessEqual.agda b/src/CatTheory/Exercise1/Contradiction/PreordersEqualEqLessEqual.agda
new file mode 100644
index 0000000..30b5264
--- /dev/null
+++ b/src/CatTheory/Exercise1/Contradiction/PreordersEqualEqLessEqual.agda
@@ -0,0 +1,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                    ∎