# Bottom elements in preorders

Content created by Egbert Rijke.

Created on 2023-05-12.

module order-theory.bottom-elements-preorders where

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

open import order-theory.preorders


## Idea

A bottom element in a preorder P is an element b such that b ≤ x holds for every element x : P.

## Definition

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

is-bottom-element-Preorder-Prop : type-Preorder X → Prop (l1 ⊔ l2)
is-bottom-element-Preorder-Prop x =
Π-Prop (type-Preorder X) (leq-Preorder-Prop X x)

is-bottom-element-Preorder : type-Preorder X → UU (l1 ⊔ l2)
is-bottom-element-Preorder x = type-Prop (is-bottom-element-Preorder-Prop x)

is-prop-is-bottom-element-Preorder :
(x : type-Preorder X) → is-prop (is-bottom-element-Preorder x)
is-prop-is-bottom-element-Preorder x =
is-prop-type-Prop (is-bottom-element-Preorder-Prop x)

has-bottom-element-Preorder : UU (l1 ⊔ l2)
has-bottom-element-Preorder = Σ (type-Preorder X) is-bottom-element-Preorder