English
The value of lift₂ on a pair is given by the universal construction, equating the result with ih i applied to the images under f₁ and f₂.
Русский
Значение lift₂ на пару задаётся универсальным построением, и равно ih i применённому к образам через f₁ и f₂.
LaTeX
$$$\\mathrm{lift\\_2\\_def}\\;(x,y,i,hxi,hyi) : \\mathrm{DirectLimit.lift\\_2}\\; f_1\\; f_2\\; ih\\; compat\\; ⟦x⟧ ⟦y⟧ = ih i (f_1 \\_ \\_ hxi x.2) (f_2 \\_ \\_ hyi y.2)$$$
Lean4
theorem map₂_def (i x y) : map₂ f₁ f₂ f ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ⟦⟨i, ih i x y⟩⟧ :=
lift₂_def ..