English
If the universal morphism colimit.pre (coyoneda.obj(op d)) F is an isomorphism, then colimit (F ⋙ coyoneda.obj(op d)) ≅ PUnit.
Русский
Если универсальный морфизм colimit.pre (coyoneda.obj(op d)) F является изоморфизмом, тогда colimit (F ⋙ coyoneda.obj(op d)) ≅ PUnit.
LaTeX
$$$\\forall d, [\\operatorname{IsIso}(\\operatorname{colimit.pre}(\\operatorname{coyoneda.obj}(\\operatorname{op} d)) F)] \\Rightarrow \\operatorname{colimit}(F \\circ \\operatorname{coyoneda.obj}(\\operatorname{op} d)) \\cong PUnit.$$
Lean4
/-- If the universal morphism `colimit (F ⋙ coyoneda.obj (op d)) ⟶ colimit (coyoneda.obj (op d))`
is an isomorphism (as it always is when `F` is final),
then `colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit`
(simply because `colimit (coyoneda.obj (op d)) ≅ PUnit`).
-/
def colimitCompCoyonedaIso (d : D) [IsIso (colimit.pre (coyoneda.obj (op d)) F)] :
colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit :=
asIso (colimit.pre (coyoneda.obj (op d)) F) ≪≫ Coyoneda.colimitCoyonedaIso (op d)
