The precategory of finite posets

Content created by Fredrik Bakke and Egbert Rijke.

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

module order-theory.precategory-of-finite-posets where
open import category-theory.full-large-subprecategories
open import category-theory.large-precategories
open import category-theory.precategories

open import foundation.universe-levels

open import order-theory.finite-posets
open import order-theory.precategory-of-posets


The (large) precategory of finite posets consists of finite posets and order preserving maps and is exhibited as a full subprecategory of the precategory of posets.


The large precategory of finite posets

parametric-Poset-𝔽-Full-Large-Subprecategory :
  (α β : Level  Level) 
    ( λ l  α l  β l)
    ( parametric-Poset-Large-Precategory α β)
parametric-Poset-𝔽-Full-Large-Subprecategory α β = is-finite-Poset-Prop

Poset-𝔽-Large-Precategory :
  Large-Precategory lsuc (_⊔_)
Poset-𝔽-Large-Precategory =
    ( Poset-Large-Precategory)
    ( parametric-Poset-𝔽-Full-Large-Subprecategory  l  l)  l  l))

The precategory of finite posets of universe level l

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

Recent changes