Dependent products of large equivalence relations

Content created by Louis Wasserman.

Created on 2026-02-21.
Last modified on 2026-02-21.

module foundation.dependent-products-large-equivalence-relations where
Imports 
open import foundation.dependent-products-large-binary-relations
open import foundation.large-binary-relations
open import foundation.large-equivalence-relations
open import foundation.universe-levels

Idea

The dependent product of a family of large equivalence relations is a large equivalence relation.

Definition

module _
  {α : Level → Level}
  {β : Level → Level → Level}
  {l0 : Level}
  (I : UU l0)
  (X : I → (l : Level) → UU (α l))
  (R : (i : I) → Large-Equivalence-Relation β (X i))
  where

  Π-Large-Equivalence-Relation :
    Large-Equivalence-Relation (λ l1 l2 → l0 ⊔ β l1 l2) (λ l → (i : I) → X i l)
  Π-Large-Equivalence-Relation =
    λ where
      .sim-prop-Large-Equivalence-Relation →
        Π-Large-Relation-Prop I X
          ( λ i → sim-prop-Large-Equivalence-Relation (R i))
      .refl-sim-Large-Equivalence-Relation →
        is-reflexive-Π-Large-Relation I X
          ( λ i → sim-Large-Equivalence-Relation (R i))
          ( λ i → refl-sim-Large-Equivalence-Relation (R i))
      .symmetric-sim-Large-Equivalence-Relation →
        is-symmetric-Π-Large-Relation I X
          ( λ i → sim-Large-Equivalence-Relation (R i))
          ( λ i → symmetric-sim-Large-Equivalence-Relation (R i))
      .transitive-sim-Large-Equivalence-Relation →
        is-transitive-Π-Large-Relation I X
          ( λ i → sim-Large-Equivalence-Relation (R i))
          ( λ i → transitive-sim-Large-Equivalence-Relation (R i))

Recent changes