Theorems · Definition

Equiv.piCongr

{α : Sort u_1} →
  {β : Sort u_4} →
    {W : α → Sort w} → {Z : β → Sort z} → (h₁ : α ≃ β) → ((a : α) → W a ≃ Z (h₁ a)) → ((a : α) → W a) ≃ ((b : β) → Z b)

Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibers.

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

9 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound