# Dependent products of large meet-semilattices

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor, Gregor Perčič and louismntnu.

Created on 2023-05-09.

module order-theory.dependent-products-large-meet-semilattices where

Imports
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.greatest-lower-bounds-large-posets
open import order-theory.large-meet-semilattices
open import order-theory.large-posets
open import order-theory.top-elements-large-posets


## Idea

Meets in dependent products of large posets are computed pointwise. This implies that the dependent product of a large meet-semilattice is again a large meet-semilattice.

## Definitions

### Meets in dependent products of large posets that have meets

module _
{α : Level → Level} {β : Level → Level → Level}
{l : Level} {I : UU l} (P : I → Large-Poset α β)
where

has-meets-Π-Large-Poset :
((i : I) → has-meets-Large-Poset (P i)) →
has-meets-Large-Poset (Π-Large-Poset P)
meet-has-meets-Large-Poset (has-meets-Π-Large-Poset H) x y i =
meet-has-meets-Large-Poset (H i) (x i) (y i)
is-greatest-binary-lower-bound-meet-has-meets-Large-Poset
( has-meets-Π-Large-Poset H) x y =
is-greatest-binary-lower-bound-Π-Large-Poset P x y
( λ i → meet-has-meets-Large-Poset (H i) (x i) (y i))
( λ i →
is-greatest-binary-lower-bound-meet-has-meets-Large-Poset
( H i)
( x i)
( y i))


### Large meet-semilattices

module _
{α : Level → Level} {β : Level → Level → Level}
{l : Level} {I : UU l} (L : I → Large-Meet-Semilattice α β)
where

large-poset-Π-Large-Meet-Semilattice :
Large-Poset (λ l1 → α l1 ⊔ l) (λ l1 l2 → β l1 l2 ⊔ l)
large-poset-Π-Large-Meet-Semilattice =
Π-Large-Poset (λ i → large-poset-Large-Meet-Semilattice (L i))

has-meets-Π-Large-Meet-Semilattice :
has-meets-Large-Poset large-poset-Π-Large-Meet-Semilattice
has-meets-Π-Large-Meet-Semilattice =
has-meets-Π-Large-Poset
( λ i → large-poset-Large-Meet-Semilattice (L i))
( λ i → has-meets-Large-Meet-Semilattice (L i))

has-top-element-Π-Large-Meet-Semilattice :
has-top-element-Large-Poset large-poset-Π-Large-Meet-Semilattice
has-top-element-Π-Large-Meet-Semilattice =
has-top-element-Π-Large-Poset
( λ i → large-poset-Large-Meet-Semilattice (L i))
( λ i → has-top-element-Large-Meet-Semilattice (L i))

is-large-meet-semilattice-Π-Large-Meet-Semilattice :
is-large-meet-semilattice-Large-Poset
large-poset-Π-Large-Meet-Semilattice
has-meets-is-large-meet-semilattice-Large-Poset
is-large-meet-semilattice-Π-Large-Meet-Semilattice =
has-meets-Π-Large-Meet-Semilattice
has-top-element-is-large-meet-semilattice-Large-Poset
is-large-meet-semilattice-Π-Large-Meet-Semilattice =
has-top-element-Π-Large-Meet-Semilattice

Π-Large-Meet-Semilattice :
Large-Meet-Semilattice (λ l1 → α l1 ⊔ l) (λ l1 l2 → β l1 l2 ⊔ l)
large-poset-Large-Meet-Semilattice Π-Large-Meet-Semilattice =
large-poset-Π-Large-Meet-Semilattice
is-large-meet-semilattice-Large-Meet-Semilattice Π-Large-Meet-Semilattice =
is-large-meet-semilattice-Π-Large-Meet-Semilattice

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

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

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

leq-Π-Large-Meet-Semilattice :
Large-Relation
( λ l1 l2 → β l1 l2 ⊔ l)
( type-Π-Large-Meet-Semilattice)
leq-Π-Large-Meet-Semilattice =
leq-Large-Meet-Semilattice Π-Large-Meet-Semilattice

refl-leq-Π-Large-Meet-Semilattice :
is-reflexive-Large-Relation
( type-Π-Large-Meet-Semilattice)
( leq-Π-Large-Meet-Semilattice)
refl-leq-Π-Large-Meet-Semilattice =
refl-leq-Large-Meet-Semilattice Π-Large-Meet-Semilattice

antisymmetric-leq-Π-Large-Meet-Semilattice :
is-antisymmetric-Large-Relation
( type-Π-Large-Meet-Semilattice)
( leq-Π-Large-Meet-Semilattice)
antisymmetric-leq-Π-Large-Meet-Semilattice =
antisymmetric-leq-Large-Meet-Semilattice Π-Large-Meet-Semilattice

transitive-leq-Π-Large-Meet-Semilattice :
is-transitive-Large-Relation
( type-Π-Large-Meet-Semilattice)
( leq-Π-Large-Meet-Semilattice)
transitive-leq-Π-Large-Meet-Semilattice =
transitive-leq-Large-Meet-Semilattice Π-Large-Meet-Semilattice

meet-Π-Large-Meet-Semilattice :
{l1 l2 : Level}
(x : type-Π-Large-Meet-Semilattice l1)
(y : type-Π-Large-Meet-Semilattice l2) →
type-Π-Large-Meet-Semilattice (l1 ⊔ l2)
meet-Π-Large-Meet-Semilattice =
meet-Large-Meet-Semilattice Π-Large-Meet-Semilattice

is-greatest-binary-lower-bound-meet-Π-Large-Meet-Semilattice :
{l1 l2 : Level}
(x : type-Π-Large-Meet-Semilattice l1)
(y : type-Π-Large-Meet-Semilattice l2) →
is-greatest-binary-lower-bound-Large-Poset
( large-poset-Π-Large-Meet-Semilattice)
( x)
( y)
( meet-Π-Large-Meet-Semilattice x y)
is-greatest-binary-lower-bound-meet-Π-Large-Meet-Semilattice =
is-greatest-binary-lower-bound-meet-Large-Meet-Semilattice
Π-Large-Meet-Semilattice

top-Π-Large-Meet-Semilattice :
type-Π-Large-Meet-Semilattice lzero
top-Π-Large-Meet-Semilattice =
top-has-top-element-Large-Poset
has-top-element-Π-Large-Meet-Semilattice

is-top-element-top-Π-Large-Meet-Semilattice :
{l1 : Level} (x : type-Π-Large-Meet-Semilattice l1) →
leq-Π-Large-Meet-Semilattice x top-Π-Large-Meet-Semilattice
is-top-element-top-Π-Large-Meet-Semilattice =
is-top-element-top-has-top-element-Large-Poset
has-top-element-Π-Large-Meet-Semilattice