# The precategory of inhabited finite total orders

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-16.

module order-theory.precategory-of-inhabited-finite-total-orders where

Imports
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.inhabited-finite-total-orders
open import order-theory.precategory-of-posets


## Idea

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

## Definitions

### The large precategory of inhabited finite total orders

parametric-Inhabited-Total-Order-𝔽-Full-Large-Subprecategory :
(α β : Level → Level) →
Full-Large-Subprecategory
( λ l → α l ⊔ β l)
( parametric-Poset-Large-Precategory α β)
parametric-Inhabited-Total-Order-𝔽-Full-Large-Subprecategory α β =
is-inhabited-finite-total-order-Poset-Prop

Inhabited-Total-Order-𝔽-Large-Precategory : Large-Precategory lsuc (_⊔_)
Inhabited-Total-Order-𝔽-Large-Precategory =
large-precategory-Full-Large-Subprecategory
( Poset-Large-Precategory)
( parametric-Inhabited-Total-Order-𝔽-Full-Large-Subprecategory
( λ l → l)
( λ l → l))


### The precategory of finite total orders of universe level l

Inhabited-Total-Order-𝔽-Precategory : (l : Level) → Precategory (lsuc l) l
Inhabited-Total-Order-𝔽-Precategory =
precategory-Large-Precategory Inhabited-Total-Order-𝔽-Large-Precategory