# Dependent products of large suplattices ```agda module order-theory.dependent-products-large-suplattices where ``` <details><summary>Imports</summary> ```agda open import foundation.large-binary-relations 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 ``` </details> ## 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 ```agda module _ {α : Level → 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-prop-Π-Large-Suplattice : Large-Relation-Prop ( λ l2 l3 → β l2 l3 ⊔ l1) ( type-Π-Large-Suplattice) leq-prop-Π-Large-Suplattice = leq-prop-Large-Suplattice Π-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 : is-prop-Large-Relation type-Π-Large-Suplattice leq-Π-Large-Suplattice is-prop-leq-Π-Large-Suplattice = is-prop-leq-Large-Suplattice Π-Large-Suplattice refl-leq-Π-Large-Suplattice : is-reflexive-Large-Relation type-Π-Large-Suplattice leq-Π-Large-Suplattice refl-leq-Π-Large-Suplattice = refl-leq-Large-Suplattice Π-Large-Suplattice antisymmetric-leq-Π-Large-Suplattice : is-antisymmetric-Large-Relation ( type-Π-Large-Suplattice) ( leq-Π-Large-Suplattice) antisymmetric-leq-Π-Large-Suplattice = antisymmetric-leq-Large-Suplattice Π-Large-Suplattice transitive-leq-Π-Large-Suplattice : is-transitive-Large-Relation ( type-Π-Large-Suplattice) ( leq-Π-Large-Suplattice) 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 ```