The precategory of posets

Content created by Fredrik Bakke.

Created on 2023-10-16.
Last modified on 2023-11-27.

module order-theory.precategory-of-posets where
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


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


The large precategory of posets

parametric-Poset-Large-Precategory :
  (α β : Level  Level) 
    ( λ 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
    .associative-comp-hom-Large-Precategory {X = X} {Y} {Z} {W} 
      associative-comp-hom-Poset X Y Z W
    .inv-associative-comp-hom-Large-Precategory {X = X} {Y} {Z} {W} 
      inv-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

Recent changes