# The precategory of posets

Content created by Fredrik Bakke.

Created on 2023-10-16.

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