# Suplattices

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor and louismntnu.

Created on 2023-05-05.

module order-theory.suplattices where

Imports
open import foundation.binary-relations
open import foundation.dependent-pair-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 : is-antisymmetric leq-Suplattice
antisymmetric-leq-Suplattice =
antisymmetric-leq-Poset poset-Suplattice

transitive-leq-Suplattice : is-transitive leq-Suplattice
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)