Dependent products of large posets

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

Created on 2023-05-09.
Last modified on 2024-04-11.

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

Imports
open import foundation.function-extensionality
open import foundation.large-binary-relations
open import foundation.universe-levels

open import order-theory.dependent-products-large-preorders
open import order-theory.large-posets
open import order-theory.large-preorders


Idea

Given a family P : I → Large-Poset α β indexed by a type I : UU l, the dependent product of the large posets P i is again a large poset.

Definitions

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

large-preorder-Π-Large-Poset :
Large-Preorder (λ l1 → α l1 ⊔ l) (λ l1 l2 → β l1 l2 ⊔ l)
large-preorder-Π-Large-Poset =
Π-Large-Preorder (λ i → large-preorder-Large-Poset (P i))

type-Π-Large-Poset : (l1 : Level) → UU (α l1 ⊔ l)
type-Π-Large-Poset =
type-Π-Large-Preorder (λ i → large-preorder-Large-Poset (P i))

leq-prop-Π-Large-Poset :
Large-Relation-Prop
( λ l1 l2 → β l1 l2 ⊔ l)
( type-Π-Large-Poset)
leq-prop-Π-Large-Poset =
leq-prop-Π-Large-Preorder (λ i → large-preorder-Large-Poset (P i))

leq-Π-Large-Poset :
Large-Relation
( λ l1 l2 → β l1 l2 ⊔ l)
( type-Π-Large-Poset)
leq-Π-Large-Poset =
leq-Π-Large-Preorder (λ i → large-preorder-Large-Poset (P i))

is-prop-leq-Π-Large-Poset :
is-prop-Large-Relation type-Π-Large-Poset leq-Π-Large-Poset
is-prop-leq-Π-Large-Poset =
is-prop-leq-Π-Large-Preorder (λ i → large-preorder-Large-Poset (P i))

refl-leq-Π-Large-Poset :
is-reflexive-Large-Relation type-Π-Large-Poset leq-Π-Large-Poset
refl-leq-Π-Large-Poset =
refl-leq-Π-Large-Preorder (λ i → large-preorder-Large-Poset (P i))

transitive-leq-Π-Large-Poset :
is-transitive-Large-Relation type-Π-Large-Poset leq-Π-Large-Poset
transitive-leq-Π-Large-Poset =
transitive-leq-Π-Large-Preorder (λ i → large-preorder-Large-Poset (P i))

antisymmetric-leq-Π-Large-Poset :
is-antisymmetric-Large-Relation type-Π-Large-Poset leq-Π-Large-Poset
antisymmetric-leq-Π-Large-Poset x y H K =
eq-htpy (λ i → antisymmetric-leq-Large-Poset (P i) (x i) (y i) (H i) (K i))

Π-Large-Poset : Large-Poset (λ l1 → α l1 ⊔ l) (λ l1 l2 → β l1 l2 ⊔ l)
large-preorder-Large-Poset Π-Large-Poset =
large-preorder-Π-Large-Poset
antisymmetric-leq-Large-Poset Π-Large-Poset =
antisymmetric-leq-Π-Large-Poset