English
For any morphism φ in κ.ord.toType and any arrow f, the right-hand component of ((iterationFunctor I κ).map φ).app f is an isomorphism.
Русский
Для любого морфизма φ в κ.ord.toType и любого стрелочного объекта f правая часть применённого функтором iterationFunctor I κ отображения на φ является изоморфизмом.
LaTeX
$$$\\forall φ:\\kappa.ord.toType,\\; f:\\mathrm{Arrow}(C),\\; IsIso\\Bigl(((\\text{iterationFunctor}(I,\\kappa).\\mathrm{map} φ).\\mathrm{app} f)\\mathrm{right}}\\Bigr)$$$
Lean4
instance {j₁ j₂ : κ.ord.toType} (φ : j₁ ⟶ j₂) (f : Arrow C) : IsIso (((iterationFunctor I κ).map φ).app f).right :=
inferInstanceAs (IsIso ((transfiniteCompositionOfShapeιIterationAppRight I κ f).F.map φ))
