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

Inhabited finite total orders

module order-theory.inhabited-finite-total-orders where
Imports 
open import foundation.inhabited-types
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.finite-posets
open import order-theory.finite-total-orders
open import order-theory.posets
open import order-theory.total-orders

open import univalent-combinatorics.finite-types

Definitions

An inhabited finite total order is a finite total order of which the underlying type is inhabited.

module _
  {l1 l2 : Level} (P : Total-Order-𝔽 l1 l2)
  where

  is-inhabited-Total-Order-𝔽-Prop : Prop l1
  is-inhabited-Total-Order-𝔽-Prop = is-inhabited-Prop (type-Total-Order-𝔽 P)

  is-inhabited-Total-Order-𝔽 : UU (l1 ⊔ l2)
  is-inhabited-Total-Order-𝔽 = is-finite-Poset (poset-Total-Order-𝔽 P)

  is-property-is-inhabited-Total-Order-𝔽 : is-prop is-inhabited-Total-Order-𝔽
  is-property-is-inhabited-Total-Order-𝔽 =
    is-prop-is-finite-Poset (poset-Total-Order-𝔽 P)

  is-finite-type-is-inhabited-Total-Order-𝔽 :
    is-inhabited-Total-Order-𝔽 → is-finite (type-Total-Order-𝔽 P)
  is-finite-type-is-inhabited-Total-Order-𝔽 =
    is-finite-type-is-finite-Poset (poset-Total-Order-𝔽 P)

is-inhabited-finite-total-order-Poset-Prop :
  {l1 l2 : Level} (P : Poset l1 l2) → Prop (l1 ⊔ l2)
is-inhabited-finite-total-order-Poset-Prop P =
  product-Prop
    ( is-total-Poset-Prop P)
    ( product-Prop
      ( is-finite-Poset-Prop P)
      ( is-inhabited-Prop (type-Poset P)))