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)