The precategory of posets
Content created by Fredrik Bakke.
Created on 2023-10-16.
Last modified on 2024-03-11.
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
Recent changes
- 2024-03-11. Fredrik Bakke. Refactor category theory to use strictly involutive identity types (#1052).
- 2023-11-27. Fredrik Bakke. Refactor categories to carry a bidirectional witness of associativity (#945).
- 2023-10-16. Fredrik Bakke. The simplex precategory (#845).