English
Let a directed system of types with a family of equivalences below a limit ordinal be given. Then at the immediate successor step the pi-equivalence map aligns the second component with the map from the previous step, i.e., the explicit evaluation of piEquivSucc collapses to the second projection of e.
Русский
Пусть задана направленная система типов с семейством эквивалентностей ниже предела по порядку. Тогда на следующем шаге отображение piEquivSucc согласует вторую компоненту с отображением от предыдущего шага: явное вычисление piEquivSucc приводит к второй проекции e.
LaTeX
$$$\\piEquivSucc\\, equiv\\, e\\, hi\\, \\langle\\_, le\\_rfl\\rangle\\, x\\, \\langle i, lt\\_succ\\_of\\_not\\_isMax\\ hi\\rangle = (e\\, x).2$$$
Lean4
theorem piEquivSucc_self {x} : piEquivSucc equiv e hi ⟨_, le_rfl⟩ x ⟨i, lt_succ_of_not_isMax hi⟩ = (e x).2 := by
simp [piEquivSucc]
