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
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


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.


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

  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 :
      ( λ 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 :
      ( λ 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 =
  antisymmetric-leq-Large-Poset Π-Large-Poset =

Recent changes