Maximal elements in posets

Content created by Viktor Yudov.

Created on 2023-11-10.
Last modified on 2024-05-03.

module order-theory.maximal-elements-posets where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.identity-types
open import foundation-core.propositions

open import order-theory.posets

Idea

TODO

Definition

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

  is-maximal-element-Poset-Prop : type-Poset X → Prop (l1 ⊔ l2)
  is-maximal-element-Poset-Prop x =
    Π-Prop
      ( type-Poset X)
      ( λ y →
        ( function-Prop (leq-Poset X x y) (y ＝ x , is-set-type-Poset X y x)))

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

  is-prop-is-maximal-element-Poset :
    (x : type-Poset X) → is-prop (is-maximal-element-Poset x)
  is-prop-is-maximal-element-Poset x =
    is-prop-type-Prop (is-maximal-element-Poset-Prop x)

Recent changes