This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The precategory of posets

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

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 or posets of universe level l

Poset-Precategory : (l : Level) → Precategory (lsuc l) l
Poset-Precategory = precategory-Large-Precategory Poset-Large-Precategory