From 729a483d9ab25b0cfb2471b22d723960c7f21b0d Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 5 Jan 2022 15:51:09 +0000
Subject: I: 1: b: show ≡ ≇ ≤ in Preorders
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../Contradiction/PreordersEqualEqLessEqual.agda   | 38 ++++++++++++++++++++++
 1 file changed, 38 insertions(+)
 create mode 100644 src/CatTheory/Exercise1/Contradiction/PreordersEqualEqLessEqual.agda

(limited to 'src')

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                    ∎
-- 
cgit v1.2.3