English
Let F be a polynomial functor and M F its associated data type. If two elements x and y of M F have identical substructures along every path, then x and y are equal (provided M F is inhabited and F.A is decidable). In other words, equality of all path projections determines equality of the whole elements.
Русский
Пусть F — полиномиальная функторная конструкция и M F — связанный с ней тип данных. Если две элементы x и y из M F имеют идентичные подпостройки вдоль каждого пути, то x = y (при условии, что M F непуст и F.A разрешимо по равенству). Иными словами, совпадение во всех проекциях по путям определяет равенство самих элементов.
LaTeX
$$$\forall x,y\in M F$, $\left(\forall ps$, Path(F),\; \iselect(ps,x)=\iselect(ps,y)\right) \Rightarrow x=y$, при условии существования и разрешимости по соответствующим данным. $$
Lean4
theorem ext [Inhabited (M F)] [DecidableEq F.A] (x y : M F) (H : ∀ ps : Path F, iselect ps x = iselect ps y) : x = y :=
by
apply ext'; intro i
induction i with
| zero => subsingleton
| succ i i_ih =>
apply ext_aux x y x
· rw [← agree_iff_agree']
apply x.consistent
· rw [← agree_iff_agree', i_ih]
apply y.consistent
introv H'
dsimp only [iselect] at H
cases H'
apply H ps
