English
The transport-construction piCongr relates families of dependent functions by composing transports along the base equivalence and the fiber equivalences.
Русский
Конструкция переноса piCongr устанавливает взаимосвязь между семействами зависимых функций через переносы вдоль базовой эквивалентности и эквивалентностей волокон.
LaTeX
$$$\\pi\\text{Congr}: (\\forall a, W a) \\to (\\forall b, Z b)\\;\\text{is transported by } h_1, h_2.$$$
Lean4
/-- Transport dependent functions through
an equivalence of the base spaces and a family
of equivalences of the matching fibers.
-/
def piCongr : (∀ a, W a) ≃ ∀ b, Z b :=
(Equiv.piCongrRight h₂).trans (Equiv.piCongrLeft _ h₁)
