English
Noncomputable definition of a ComposableArrows object built from given obj and mapSucc, ensuring derivation of maps i→i+1.
Русский
Не вычисляемое определение объекта ComposableArrows, построенного из заданного obj и mapSucc, обеспечивающее вывод отображений i→i+1.
LaTeX
$${C : Type u_1} → [Category C] → {n : Nat} → (obj : Fin (n+1) → C) → ((i : Fin n) → obj i.castSucc ⟶ obj i.succ) → ComposableArrows C n$$
Lean4
/-- Given `obj : Fin (n + 1) → C` and `mapSucc i : obj i.castSucc ⟶ obj i.succ`
for all `i : Fin n`, this is `F : ComposableArrows C n` such that `F.obj i` is
definitionally equal to `obj i` and such that `F.map' i (i + 1) = mapSucc ⟨i, hi⟩`. -/
noncomputable def mkOfObjOfMapSucc : ComposableArrows C n :=
(mkOfObjOfMapSucc_exists obj mapSucc).choose.copyObj obj (mkOfObjOfMapSucc_exists obj mapSucc).choose_spec.choose
