The precategory of posets

Content created by Fredrik Bakke.

Created on 2023-10-16.
Last modified on 2024-11-20.

module order-theory.precategory-of-posets where
Imports 
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

open import order-theory.order-preserving-maps-posets
open import order-theory.posets

Idea

The (large) precategory of posets consists of posets and order preserving maps.

Definitions

The large precategory of posets

Remark. In this formalization we see a clear limit to our approach using large precategories. Large precategories are only designed to encapsulate structures that are universe polymorphic in a single universe level variable. However, posets are polymorphic in two universe level variables, leading to a shortcoming in the below formalization. Namely, we cannot capture the structure of all posets and morphisms between them. For instance, we can only capture morphisms between two posets of the form A : Poset (α l1) (β l1) and B : Poset (α l2) (β l2), and not arbitrary ones of the form A : Poset l1 l2 and B : Poset l3 l4.

parametric-Poset-Large-Precategory :
  (α β : Level → Level) →
  Large-Precategory
    ( λ l → lsuc (α l) ⊔ lsuc (β l))
    ( λ l1 l2 → α l1 ⊔ β l1 ⊔ α l2 ⊔ β l2)
parametric-Poset-Large-Precategory α β =
  λ where
    .obj-Large-Precategory l →
      Poset (α l) (β l)
    .hom-set-Large-Precategory →
      hom-set-Poset
    .comp-hom-Large-Precategory {X = X} {Y} {Z} →
      comp-hom-Poset X Y Z
    .id-hom-Large-Precategory {X = X} →
      id-hom-Poset X
    .involutive-eq-associative-comp-hom-Large-Precategory {X = X} {Y} {Z} {W} →
      involutive-eq-associative-comp-hom-Poset X Y Z W
    .left-unit-law-comp-hom-Large-Precategory {X = X} {Y} →
      left-unit-law-comp-hom-Poset X Y
    .right-unit-law-comp-hom-Large-Precategory {X = X} {Y} →
      right-unit-law-comp-hom-Poset X Y

Poset-Large-Precategory : Large-Precategory lsuc (_⊔_)
Poset-Large-Precategory = parametric-Poset-Large-Precategory (λ l → l) (λ l → l)

The precategory of posets at a universe level

Poset-Precategory : (l1 l2 : Level) → Precategory (lsuc l1 ⊔ lsuc l2) (l1 ⊔ l2)
Poset-Precategory l1 l2 =
  make-Precategory
    ( Poset l1 l2)
    ( hom-set-Poset)
    ( λ {P} {Q} {R} → comp-hom-Poset P Q R)
    ( id-hom-Poset)
    ( λ {P} {Q} {R} {S} → associative-comp-hom-Poset P Q R S)
    ( λ {P} {Q} → left-unit-law-comp-hom-Poset P Q)
    ( λ {P} {Q} → right-unit-law-comp-hom-Poset P Q)

Recent changes