Dependent products of large meet-semilattices
module order-theory.dependent-products-large-meet-semilattices where
Imports
open import foundation.identity-types 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 : {l1 l2 : Level} → type-Π-Large-Meet-Semilattice l1 → type-Π-Large-Meet-Semilattice l2 → UU (β l1 l2 ⊔ l) leq-Π-Large-Meet-Semilattice = leq-Large-Meet-Semilattice Π-Large-Meet-Semilattice refl-leq-Π-Large-Meet-Semilattice : {l1 : Level} → (x : type-Π-Large-Meet-Semilattice l1) → leq-Π-Large-Meet-Semilattice x x refl-leq-Π-Large-Meet-Semilattice = refl-leq-Large-Meet-Semilattice Π-Large-Meet-Semilattice antisymmetric-leq-Π-Large-Meet-Semilattice : {l1 : Level} → (x y : type-Π-Large-Meet-Semilattice l1) → leq-Π-Large-Meet-Semilattice x y → leq-Π-Large-Meet-Semilattice y x → x ＝ y antisymmetric-leq-Π-Large-Meet-Semilattice = antisymmetric-leq-Large-Meet-Semilattice Π-Large-Meet-Semilattice transitive-leq-Π-Large-Meet-Semilattice : {l1 l2 l3 : Level} (x : type-Π-Large-Meet-Semilattice l1) (y : type-Π-Large-Meet-Semilattice l2) (z : type-Π-Large-Meet-Semilattice l3) → leq-Π-Large-Meet-Semilattice y z → leq-Π-Large-Meet-Semilattice x y → leq-Π-Large-Meet-Semilattice x z 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