Upper sets of large posets

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module order-theory.upper-sets-large-posets where
Imports 
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-subposets

Idea

An upper set or upwards closed set in a large poset is a large subposet that is upwards closed, i.e., that satisfies the condition that

  ∀ (x y : P), (x ≤ y) → x ∈ S → y ∈ S.

Definitions

The predicate of being an upper set

module _
  {α γ : Level → Level} {β : Level → Level → Level}
  (P : Large-Poset α β) (S : Large-Subposet γ P)
  where

  is-upper-set-Large-Subposet : UUω
  is-upper-set-Large-Subposet =
    {l1 l2 : Level} (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
    leq-Large-Poset P x y →
    is-in-Large-Subposet P S x → is-in-Large-Subposet P S y

Upper sets of a large poset

module _
  {α : Level → Level} {β : Level → Level → Level} (γ : Level → Level)
  (P : Large-Poset α β)
  where

  record
    upper-set-Large-Poset : UUω
    where
    field
      large-subposet-upper-set-Large-Poset :
        Large-Subposet γ P
      is-upper-set-upper-set-Large-Poset :
        is-upper-set-Large-Subposet P large-subposet-upper-set-Large-Poset

  open upper-set-Large-Poset public

See also

Recent changes