Top elements in preorders

Content created by Egbert Rijke, Fredrik Bakke and Viktor Yudov.

Created on 2023-05-12.
Last modified on 2026-05-02.

module order-theory.top-elements-preorders where
Imports 
open import foundation.dependent-pair-types
open import foundation.dependent-products-propositions
open import foundation.propositions
open import foundation.universe-levels

open import order-theory.preorders

Idea

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

Definition

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

  is-top-element-prop-Preorder : type-Preorder X → Prop (l1 ⊔ l2)
  is-top-element-prop-Preorder x =
    Π-Prop (type-Preorder X) (λ y → leq-prop-Preorder X y x)

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

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

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

Recent changes