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 decidable total order of a standard finite type

module elementary-number-theory.decidable-total-order-standard-finite-types where

open import elementary-number-theory.inequality-standard-finite-types
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.propositional-truncations
open import foundation.universe-levels

open import order-theory.decidable-total-orders
open import order-theory.total-orders

Idea

The standard finite type of order k equipped with its standard ordering relation forms a decidable total order.

Definition

is-total-leq-Fin : (k : ℕ) → is-total-Poset (Fin-Poset k)
is-total-leq-Fin k n m = unit-trunc-Prop (linear-leq-Fin k n m)

Fin-Total-Order : ℕ → Total-Order lzero lzero
pr1 (Fin-Total-Order k) = Fin-Poset k
pr2 (Fin-Total-Order k) = is-total-leq-Fin k

Fin-Decidable-Total-Order : ℕ → Decidable-Total-Order lzero lzero
pr1 (Fin-Decidable-Total-Order k) = Fin-Poset k
pr1 (pr2 (Fin-Decidable-Total-Order k)) = is-total-leq-Fin k
pr2 (pr2 (Fin-Decidable-Total-Order k)) = is-decidable-leq-Fin k