English
If index types α and α' are equal and pointwise heterogeneous-equivalence holds between f and f', then f and f' are heterogeneous-equivalent.
Русский
Если индексы α и α' равны и по точке выполняется гетерогенная эквивалентность между f и f', то функции эквивалентны по гетерогенной эквивалентности.
LaTeX
$$$$ f \\simeq f' \\\\text{ under } α=α' \\\\text{ and } \\forall a,a', a \\sim a' \Rightarrow f(a) \\sim f'(a'). $$$$
Lean4
theorem hfunext {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : ∀ a, β a} {f' : ∀ a, β' a} (hα : α = α')
(h : ∀ a a', a ≍ a' → f a ≍ f' a') : f ≍ f' := by
subst hα
have : ∀ a, f a ≍ f' a := fun a ↦ h a a (HEq.refl a)
have : β = β' := by funext a; exact type_eq_of_heq (this a)
subst this
grind
