This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The precategory of decidable total orders

module order-theory.precategory-of-decidable-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.decidable-total-orders
open import order-theory.precategory-of-posets

Idea

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

Definitions

The large precategory of decidable total orders

parametric-Decidable-Total-Order-Full-Large-Subprecategory :
  (α β : Level → Level) →
  Full-Large-Subprecategory
    ( λ l → α l ⊔ β l)
    ( parametric-Poset-Large-Precategory α β)
parametric-Decidable-Total-Order-Full-Large-Subprecategory α β =
  is-decidable-total-prop-Poset

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

The precategory or total orders of universe level l

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