Suplattices

module order-theory.suplattices where

Imports

open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import order-theory.least-upper-bounds-posets
open import order-theory.posets

Idea

An l-suplattice is a poset which has all least upper bounds of families of elements indexed by a type of universe level l.

Definitions

The predicate on posets of being an `l`-suplattice

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

  is-suplattice-Poset-Prop : Prop (l1 ⊔ l2 ⊔ lsuc l3)
  is-suplattice-Poset-Prop =
    Π-Prop
      (UU l3)
      (λ I →
        Π-Prop
          ( I → type-Poset P)
          ( λ f → has-least-upper-bound-family-of-elements-Poset-Prop P f))

  is-suplattice-Poset : UU (l1 ⊔ l2 ⊔ lsuc l3)
  is-suplattice-Poset = type-Prop is-suplattice-Poset-Prop

  is-prop-suplattice-Poset : is-prop is-suplattice-Poset
  is-prop-suplattice-Poset = is-prop-type-Prop is-suplattice-Poset-Prop

module _
  {l1 l2 l3 : Level} (P : Poset l1 l2) (H : is-suplattice-Poset l3 P)
  where

  sup-is-suplattice-Poset :
    {I : UU l3} → (I → type-Poset P) → type-Poset P
  sup-is-suplattice-Poset {I} x = pr1 (H I x)

  is-least-upper-bound-sup-is-suplattice-Poset :
    {I : UU l3} (x : I → type-Poset P) →
    is-least-upper-bound-family-of-elements-Poset P x
      ( sup-is-suplattice-Poset x)
  is-least-upper-bound-sup-is-suplattice-Poset {I} x = pr2 (H I x)

`l`-Suplattices

Suplattice : (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
Suplattice l1 l2 l3 = Σ (Poset l1 l2) (λ P → is-suplattice-Poset l3 P)

module _
  {l1 l2 l3 : Level} (A : Suplattice l1 l2 l3)
  where

  poset-Suplattice : Poset l1 l2
  poset-Suplattice = pr1 A

  type-Suplattice : UU l1
  type-Suplattice = type-Poset poset-Suplattice

  leq-Suplattice-Prop : (x y : type-Suplattice) → Prop l2
  leq-Suplattice-Prop = leq-Poset-Prop poset-Suplattice

  leq-Suplattice : (x y : type-Suplattice) → UU l2
  leq-Suplattice = leq-Poset poset-Suplattice

  is-prop-leq-Suplattice :
    (x y : type-Suplattice) → is-prop (leq-Suplattice x y)
  is-prop-leq-Suplattice = is-prop-leq-Poset poset-Suplattice

  refl-leq-Suplattice :
    (x : type-Suplattice) → leq-Suplattice x x
  refl-leq-Suplattice = refl-leq-Poset poset-Suplattice

  antisymmetric-leq-Suplattice :
    (x y : type-Suplattice) →
    leq-Suplattice x y → leq-Suplattice y x → x ＝ y
  antisymmetric-leq-Suplattice =
    antisymmetric-leq-Poset poset-Suplattice

  transitive-leq-Suplattice :
    (x y z : type-Suplattice) →
    leq-Suplattice y z → leq-Suplattice x y →
    leq-Suplattice x z
  transitive-leq-Suplattice = transitive-leq-Poset poset-Suplattice

  is-set-type-Suplattice : is-set type-Suplattice
  is-set-type-Suplattice = is-set-type-Poset poset-Suplattice

  set-Suplattice : Set l1
  set-Suplattice = set-Poset poset-Suplattice

  is-suplattice-Suplattice :
    is-suplattice-Poset l3 poset-Suplattice
  is-suplattice-Suplattice = pr2 A

  sup-Suplattice :
    {I : UU l3} → (I → type-Suplattice) → type-Suplattice
  sup-Suplattice =
    sup-is-suplattice-Poset
      ( poset-Suplattice)
      ( is-suplattice-Suplattice)

  is-least-upper-bound-sup-Suplattice :
    {I : UU l3} (x : I → type-Suplattice) →
    is-least-upper-bound-family-of-elements-Poset poset-Suplattice x
      ( sup-Suplattice x)
  is-least-upper-bound-sup-Suplattice =
    is-least-upper-bound-sup-is-suplattice-Poset
      ( poset-Suplattice)
      ( is-suplattice-Suplattice)