{-# 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                    ∎