English
Given a heterogeneous equality hargs between a1 and a2, a compatible ht relating β1 and β2 on related indices, and an hf transporting along α1 = α2 and β1 ≃ β2, one obtains f1(a1) ≃ f2(a2) (heterogeneous equality).
Русский
Пусть имеются гетерогенные равенства между a1 и a2, совместимый ht для β1 и β2 на соответствующих индексах и hf, переносящий по равенству α1 = α2 и эквивалентности β1 ≃ β2; тогда f1(a1) эквивалентны f2(a2) в гетерогенном смысле.
LaTeX
$$$f_1(a_1) \\; \\overset{HEq}{\\equiv} \\; f_2(a_2) \\text{ при заданных условиях } hargs, ht, hf.$$$
Lean4
theorem dcongr_heq.{u, v} {α₁ α₂ : Sort u} {β₁ : α₁ → Sort v} {β₂ : α₂ → Sort v} {f₁ : ∀ a, β₁ a} {f₂ : ∀ a, β₂ a}
{a₁ : α₁} {a₂ : α₂} (hargs : a₁ ≍ a₂) (ht : ∀ t₁ t₂, t₁ ≍ t₂ → β₁ t₁ = β₂ t₂) (hf : α₁ = α₂ → β₁ ≍ β₂ → f₁ ≍ f₂) :
f₁ a₁ ≍ f₂ a₂ := by
cases hargs
cases funext fun v => ht v v .rfl
cases hf rfl .rfl
rfl
