English
Let (α_i) be a family of types indexed by i in a set I. Form the dependent product by applying the identity on each component, i.e. take the pi-construction of the family of identity equivalences. This yields the identity equivalence on the dependent product ∀ i, α_i.
Русский
Пусть {α_i} — семейство типов, индексируемых по i из множества I. Применив по компонентам тождественные эквивалентности, получаемPi-операцию. Тогда полученная частичная эквивалентность на зависимом произведении ∀ i, α_i i является тождественной эквививалентностью.
LaTeX
$$$Eq\\left(\\PartialEquiv.pi(\\lambda i.\\PartialEquiv.refl(\\alpha_i i))\\right)\\left(\\PartialEquiv.refl\\left(\\forall i, \\alpha_i i\\right)\\right)$$
Lean4
@[simp, mfld_simps]
theorem pi_refl : (PartialEquiv.pi fun i ↦ PartialEquiv.refl (αi i)) = .refl (∀ i, αi i) := by ext <;> simp
