# Total preorders

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, Victor Blanchi, fernabnor and louismntnu.

Created on 2022-03-16.

module order-theory.total-preorders where

Imports
open import foundation.binary-relations
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.preorders


## Idea

A total preorder is a preorder P such that for every two elements x y : P the disjunction (x ≤ y) ∨ (y ≤ x) holds. In other words, total preorders are totally ordered in the sense that any two elements can be compared.

## Definition

### Being a total preorder

module _
{l1 l2 : Level} (X : Preorder l1 l2)
where

incident-Preorder-Prop : (x y : type-Preorder X) → Prop l2
incident-Preorder-Prop x y =
(leq-Preorder-Prop X x y) ∨ (leq-Preorder-Prop X y x)

incident-Preorder : (x y : type-Preorder X) → UU l2
incident-Preorder x y = type-Prop (incident-Preorder-Prop x y)

is-prop-incident-Preorder :
(x y : type-Preorder X) → is-prop (incident-Preorder x y)
is-prop-incident-Preorder x y = is-prop-type-Prop (incident-Preorder-Prop x y)

is-total-Preorder-Prop : Prop (l1 ⊔ l2)
is-total-Preorder-Prop =
Π-Prop
( type-Preorder X)
( λ x → Π-Prop ( type-Preorder X) (λ y → incident-Preorder-Prop x y))

is-total-Preorder : UU (l1 ⊔ l2)
is-total-Preorder = type-Prop is-total-Preorder-Prop

is-prop-is-total-Preorder : is-prop is-total-Preorder
is-prop-is-total-Preorder = is-prop-type-Prop is-total-Preorder-Prop


### The type of total preorder

Total-Preorder : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Total-Preorder l1 l2 = Σ (Preorder l1 l2) is-total-Preorder

module _
{l1 l2 : Level} (X : Total-Preorder l1 l2)
where

preorder-Total-Preorder : Preorder l1 l2
preorder-Total-Preorder = pr1 X

is-total-preorder-Total-Preorder : is-total-Preorder preorder-Total-Preorder
is-total-preorder-Total-Preorder = pr2 X

type-Total-Preorder : UU l1
type-Total-Preorder = type-Preorder preorder-Total-Preorder

leq-Total-Preorder-Prop : (x y : type-Total-Preorder) → Prop l2
leq-Total-Preorder-Prop = leq-Preorder-Prop preorder-Total-Preorder

leq-Total-Preorder : (x y : type-Total-Preorder) → UU l2
leq-Total-Preorder = leq-Preorder preorder-Total-Preorder

is-prop-leq-Total-Preorder :
(x y : type-Total-Preorder) → is-prop (leq-Total-Preorder x y)
is-prop-leq-Total-Preorder = is-prop-leq-Preorder preorder-Total-Preorder

refl-leq-Total-Preorder : is-reflexive leq-Total-Preorder
refl-leq-Total-Preorder = refl-leq-Preorder preorder-Total-Preorder

transitive-leq-Total-Preorder : is-transitive leq-Total-Preorder
transitive-leq-Total-Preorder =
transitive-leq-Preorder preorder-Total-Preorder