English
Let e: α ≃ β be a bijection and P a family of types over α. Then there is a natural bijection between the space of dependent functions ∀a, P(a) and the space ∀b, P(e^{-1}(b)). Concretely, f ↦ (b ↦ f(e^{-1}(b))) has inverse g ↦ (a ↦ g(e(a))).
Русский
Пусть e: α ≃ β — биекция, и P — семейство типов над α. Тогда существует естественное биективное соответствие между множеством зависимых функций ∀a, P(a) и множеством функций ∀b, P(e^{-1}(b)).
LaTeX
$$$(\forall a\, P(a)) \quad\cong\quad (\forall b\, P(e^{-1}(b))).$ Детальное определение: $\big( f\mapsto (b\mapsto f(e^{-1}(b))) \big)$ и $\big( g\mapsto (a\mapsto g(e(a))) \big)$ являются взаимно обратными.$$
Lean4
/-- Transport dependent functions through an equivalence of the base space.
-/
@[simps apply, simps -isSimp symm_apply]
def piCongrLeft' (P : α → Sort*) (e : α ≃ β) : (∀ a, P a) ≃ ∀ b, P (e.symm b)
where
toFun f x := f (e.symm x)
invFun f x := (e.symm_apply_apply x).ndrec (f (e x))
left_inv f := funext fun x => (by rintro _ rfl; rfl : ∀ {y} (h : y = x), h.ndrec (f y) = f x) (e.symm_apply_apply x)
right_inv
f :=
funext fun x =>
(by rintro _ rfl; rfl : ∀ {y} (h : y = x), (congr_arg e.symm h).ndrec (f y) = f x) (e.apply_symm_apply x)
