English
Let e be a bijection between α and β (an equivalence), and let P be a family of types over β. For any function f assigning to each a in α an element of P(e(a)), the left-conjugated package piCongrLeft applied to f at b ∈ β is obtained by transporting f(e⁻¹(b)) along the canonical equality e(e⁻¹(b)) = b.
Русский
Пусть e: α ≃ β, и пусть P : β → Type задаёт семейство типов. Для любой f : ∀ a ∈ α, P(e(a)) верно, что значение функции, полученной конъюгацией слева, в точке b ∈ β получается перенесением элемента f(e⁻¹(b)) вдоль равенства e(e⁻¹(b)) = b.
LaTeX
$$$\\text{For } e:\\alpha\\simeq\\beta,\\ P:\\beta\\to\\text{Sort},\\ f:(a:\\alpha)\\to P(e\\,a),\\ b:\\beta:\\quad (\\pi_{\\text{CongrLeft}} P\\,e\\,f)(b)=\\operatorname{cast}\\big(\\operatorname{congr_arg} P (e.\\text{apply_symm_apply } b)\\big)\\big( f(e.\\text{symm } b)\\big).$$$
Lean4
theorem piCongrLeft_apply_eq_cast {P : β → Sort v} {e : α ≃ β} (f : (a : α) → P (e a)) (b : β) :
piCongrLeft P e f b = cast (congr_arg P (e.apply_symm_apply b)) (f (e.symm b)) :=
eqRec_eq_cast _ _
