Lean4
/-- Given a functor `K : J ⥤ Under X` and its extension `liftFromUnder K : WithInitial J ⥤ C`,
there is an obvious equivalence between cocones of these two functors.
A cocone of `K` is an object of `Under X`, so it has the form `X ⟶ t`.
Equivalently, a cocone of `WithInitial K` is an object `t : C`,
and we can recover the structure morphism as `ι.app X : X ⟶ t`. -/
@[simps! functor_obj_pt functor_map_hom inverse_obj_pt_right inverse_obj_pt_left_as inverse_obj_pt_hom
inverse_obj_ι_app_right inverse_map_hom_right unitIso_hom_app_hom_right unitIso_inv_app_hom_right
counitIso_hom_app_hom counitIso_inv_app_hom]
def coconeEquiv : Cocone K ≌ Cocone (liftFromUnder.obj K)
where
functor := coconeLift
inverse := coconeBack
unitIso := .refl _
counitIso := NatIso.ofComponents fun t ↦ Cocones.ext <| .refl _
