Function large equivalence relations

Content created by Louis Wasserman.

Created on 2025-11-16.
Last modified on 2026-02-21.

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

Idea

Given a large equivalence relation on X and a type A, there is an induced large equivalence relation on A → X.

Definition

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

  function-Large-Equivalence-Relation :
    Large-Equivalence-Relation
      ( λ l2 l3 → l1 ⊔ β l2 l3)
      ( λ l → A → X l)
  function-Large-Equivalence-Relation =
    Π-Large-Equivalence-Relation A (λ _ → X) (λ _ → R)

Recent changes