English
The F-component of the map from the iterationObjRightIso to the iterationFunctor coincides with the iterationFunctor itself.
Русский
Компонента F сопоставления из iterationObjRightIso совпадает с самой iterationFunctor.
LaTeX
$$$\\text{(iterationObjRightIso I κ)}_{F} = \\text{iterationFunctor}(I,κ)$$$
Lean4
@[reassoc (attr := simp)]
theorem iterationFunctorObjObjRightIso_ιIteration_app_right (f : Arrow C) (j : κ.ord.toType) :
(iterationFunctorObjObjRightIso I κ f j).hom ≫ ((ιIteration I κ).app f).right =
(transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j :=
by simp [iterationFunctorObjObjRightIso, iterationObjRightIso]
