Definition. Poset [ag-000F]

{-# OPTIONS --safe --without-K #-}
module ag-000F where

open import MLTT.Spartan
open import UF.Sets
open import UF.SubtypeClassifier

Order is a binary relation ≤.

order-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
order-structure {𝓤} A = A → A → Ω 𝓤

A poset A is a pair (A,  ≤ )

1. x ≤ x for all x ∈ A
2. x ≤ y and y ≤ z implies x ≤ z for all x, y, z ∈ A
3. x ≤ y and y ≤ x implies x = y for all x, y ∈ A

poset-axioms : (A : 𝓤 ̇ ) → order-structure A → 𝓤 ̇
poset-axioms A _≤_ = is-set A
                    × ((x : A) → (x ≤ x) holds)
                    × ((x y z : A) → (x ≤ y) holds → (y ≤ z) holds → (x ≤ z) holds)
                    × ((x y : A) → (x ≤ y) holds → (y ≤ x) holds → x ＝ y)

Poset-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
Poset-structure A = Σ _≤_ ꞉ order-structure A , (poset-axioms A _≤_)

Poset : (𝓤 : Universe) → 𝓤 ⁺ ̇
Poset 𝓤 = Σ A ꞉ 𝓤 ̇ , Poset-structure A

We can add a helper to extract underlying set

⟨_⟩ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → 𝓤 ̇
⟨ X , s ⟩ = X

order-of : (P : Poset 𝓤) → ⟨ P ⟩ → ⟨ P ⟩ → Ω 𝓤
order-of (X , _≤_ , _) x y = x ≤ y

syntax order-of P x y = x ≤⟨ P ⟩ y

posets-are-sets : (P : Poset 𝓤) → is-set ⟨ P ⟩
posets-are-sets (X , _≤_ , i , rfl , trans , ir) = i

A hom from a poset to another, is a map that preserves the order

is-hom : (P : Poset 𝓤) (Q : Poset 𝓥) → (⟨ P ⟩ → ⟨ Q ⟩) → 𝓤 ⊔ 𝓥 ̇
is-hom P Q f = ∀ {x y} → (x ≤⟨ P ⟩ y) holds → (f x ≤⟨ Q ⟩ f y) holds

Identity map is a hom

id-is-hom : (P : Poset 𝓤) → is-hom P P id
id-is-hom P x≤y = x≤y

The composition of homs is a hom

∘-is-hom : (P : Poset 𝓤) (Q : Poset 𝓥) (R : Poset 𝓦)
            (f : ⟨ P ⟩ → ⟨ Q ⟩) (g : ⟨ Q ⟩ → ⟨ R ⟩)
          → is-hom P Q f → is-hom Q R g → is-hom P R (g ∘ f)
∘-is-hom P Q R f g f-is-hom g-is-hom x≤y = g-is-hom (f-is-hom x≤y)