Dependent products of large suplattices

module order-theory.dependent-products-large-suplattices where

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

open import order-theory.dependent-products-large-posets
open import order-theory.large-posets
open import order-theory.large-suplattices
open import order-theory.least-upper-bounds-large-posets

Idea

Families of least upper bounds of families of elements in dependent products of large posets are again least upper bounds. Therefore it follows that dependent products of large suplattices are again large suplattices.

Definitions

module _
  {α : Level → Level} {β : Level → Level → Level}
  {l1 : Level} {I : UU l1} (L : I → Large-Suplattice α β)
  where

  large-poset-Π-Large-Suplattice :
    Large-Poset (λ l2 → α l2 ⊔ l1) (λ l2 l3 → β l2 l3 ⊔ l1)
  large-poset-Π-Large-Suplattice =
    Π-Large-Poset (λ i → large-poset-Large-Suplattice (L i))

  is-large-suplattice-Π-Large-Suplattice :
    is-large-suplattice-Large-Poset large-poset-Π-Large-Suplattice
  sup-has-least-upper-bound-family-of-elements-Large-Poset
    ( is-large-suplattice-Π-Large-Suplattice {l2} {l3} {J} a) i =
    sup-Large-Suplattice (L i) (λ j → a j i)
  is-least-upper-bound-sup-has-least-upper-bound-family-of-elements-Large-Poset
    ( is-large-suplattice-Π-Large-Suplattice {l2} {l3} {J} a) =
    is-least-upper-bound-Π-Large-Poset
      ( λ i → large-poset-Large-Suplattice (L i))
      ( a)
      ( λ i → sup-Large-Suplattice (L i) (λ j → a j i))
      ( λ i →
        is-least-upper-bound-sup-Large-Suplattice (L i) (λ j → a j i))

  Π-Large-Suplattice :
    Large-Suplattice (λ l2 → α l2 ⊔ l1) (λ l2 l3 → β l2 l3 ⊔ l1)
  large-poset-Large-Suplattice Π-Large-Suplattice =
    large-poset-Π-Large-Suplattice
  is-large-suplattice-Large-Suplattice Π-Large-Suplattice =
    is-large-suplattice-Π-Large-Suplattice

  set-Π-Large-Suplattice : (l : Level) → Set (α l ⊔ l1)
  set-Π-Large-Suplattice =
    set-Large-Suplattice Π-Large-Suplattice

  type-Π-Large-Suplattice : (l : Level) → UU (α l ⊔ l1)
  type-Π-Large-Suplattice =
    type-Large-Suplattice Π-Large-Suplattice

  is-set-type-Π-Large-Suplattice :
    {l : Level} → is-set (type-Π-Large-Suplattice l)
  is-set-type-Π-Large-Suplattice =
    is-set-type-Large-Suplattice Π-Large-Suplattice

  leq-Π-Large-Suplattice-Prop :
    {l2 l3 : Level}
    (x : type-Π-Large-Suplattice l2) (y : type-Π-Large-Suplattice l3) →
    Prop (β l2 l3 ⊔ l1)
  leq-Π-Large-Suplattice-Prop =
    leq-Large-Suplattice-Prop Π-Large-Suplattice

  leq-Π-Large-Suplattice :
    {l2 l3 : Level}
    (x : type-Π-Large-Suplattice l2) (y : type-Π-Large-Suplattice l3) →
    UU (β l2 l3 ⊔ l1)
  leq-Π-Large-Suplattice =
    leq-Large-Suplattice Π-Large-Suplattice

  is-prop-leq-Π-Large-Suplattice :
    {l2 l3 : Level}
    (x : type-Π-Large-Suplattice l2) (y : type-Π-Large-Suplattice l3) →
    is-prop (leq-Π-Large-Suplattice x y)
  is-prop-leq-Π-Large-Suplattice =
    is-prop-leq-Large-Suplattice Π-Large-Suplattice

  refl-leq-Π-Large-Suplattice :
    {l2 : Level} (x : type-Π-Large-Suplattice l2) →
    leq-Π-Large-Suplattice x x
  refl-leq-Π-Large-Suplattice =
    refl-leq-Large-Suplattice Π-Large-Suplattice

  antisymmetric-leq-Π-Large-Suplattice :
    {l2 : Level}
    (x : type-Π-Large-Suplattice l2) (y : type-Π-Large-Suplattice l2) →
    leq-Π-Large-Suplattice x y → leq-Π-Large-Suplattice y x → x ＝ y
  antisymmetric-leq-Π-Large-Suplattice =
    antisymmetric-leq-Large-Suplattice Π-Large-Suplattice

  transitive-leq-Π-Large-Suplattice :
    {l2 l3 l4 : Level}
    (x : type-Π-Large-Suplattice l2)
    (y : type-Π-Large-Suplattice l3)
    (z : type-Π-Large-Suplattice l4) →
    leq-Π-Large-Suplattice y z → leq-Π-Large-Suplattice x y →
    leq-Π-Large-Suplattice x z
  transitive-leq-Π-Large-Suplattice =
    transitive-leq-Large-Suplattice Π-Large-Suplattice

  sup-Π-Large-Suplattice :
    {l2 l3 : Level} {J : UU l2} (x : J → type-Π-Large-Suplattice l3) →
    type-Π-Large-Suplattice (l2 ⊔ l3)
  sup-Π-Large-Suplattice =
    sup-Large-Suplattice Π-Large-Suplattice

  is-upper-bound-family-of-elements-Π-Large-Suplattice :
    {l2 l3 l4 : Level} {J : UU l2} (x : J → type-Π-Large-Suplattice l3)
    (y : type-Π-Large-Suplattice l4) → UU (β l3 l4 ⊔ l1 ⊔ l2)
  is-upper-bound-family-of-elements-Π-Large-Suplattice =
    is-upper-bound-family-of-elements-Large-Suplattice Π-Large-Suplattice

  is-least-upper-bound-family-of-elements-Π-Large-Suplattice :
    {l2 l3 l4 : Level} {J : UU l2} (x : J → type-Π-Large-Suplattice l3) →
    type-Π-Large-Suplattice l4 → UUω
  is-least-upper-bound-family-of-elements-Π-Large-Suplattice =
    is-least-upper-bound-family-of-elements-Large-Suplattice Π-Large-Suplattice

  is-least-upper-bound-sup-Π-Large-Suplattice :
    {l2 l3 : Level} {J : UU l2} (x : J → type-Π-Large-Suplattice l3) →
    is-least-upper-bound-family-of-elements-Π-Large-Suplattice x
      ( sup-Π-Large-Suplattice x)
  is-least-upper-bound-sup-Π-Large-Suplattice =
    is-least-upper-bound-sup-Large-Suplattice Π-Large-Suplattice