English
Two objects F and G in ComposableArrows C n are equal if their objects agree componentwise and their maps agree under the appropriate compatibility conditions.
Русский
Два объекта F и G в ComposableArrows C n равны, если их компоненты объектов совпадают по координатам, и их отображения совпадают при соответствующих условиях совместимости.
LaTeX
$$$\forall F,G:\text{ComposableArrows}\ C\ n,\ (\forall i, F.obj i = G.obj i) \,\to \, (\forall i, hi, F.map' i (i+1) = (eqToHom (h i)) ≫ G.map' i (i+1) ≫ eqToHom (h i).symm) \Rightarrow F=G$$$
Lean4
theorem ext {F G : ComposableArrows C n} (h : ∀ i, F.obj i = G.obj i)
(w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) = eqToHom (h _) ≫ G.map' i (i + 1) ≫ eqToHom (h _).symm) : F = G :=
Functor.ext_of_iso (isoMk (fun i => eqToIso (h i)) (fun i hi => by simp [w i hi])) h
