Lean4
/-- Given a functor `K : J ⥤ Over X` and its extension `liftFromOver K : WithTerminal J ⥤ C`,
there is an obvious equivalence between cones of these two functors.
A cone of `K` is an object of `Over X`, so it has the form `t ⟶ X`.
Equivalently, a cone of `WithTerminal K` is an object `t : C`,
and we can recover the structure morphism as `π.app X : t ⟶ X`. -/
@[simps! functor_obj_pt functor_map_hom inverse_obj_pt_left inverse_obj_pt_right_as inverse_obj_pt_hom
inverse_obj_π_app_left inverse_map_hom_left unitIso_hom_app_hom_left unitIso_inv_app_hom_left
counitIso_hom_app_hom counitIso_inv_app_hom]
def coneEquiv : Cone K ≌ Cone (liftFromOver.obj K)
where
functor := coneLift
inverse := coneBack
unitIso := .refl _
counitIso := NatIso.ofComponents fun t ↦ Cones.ext <| .refl _
