English
There is a natural equivalence between the category of type-based cocones for F and the categorical cocones over F. Concretely, given a type-based cocone with point in Type u, one obtains a cocone over F by taking the same point and using the component maps; conversely, from a cocone over F one recovers a type-based cocone by taking the underlying point and composing with the universal maps.
Русский
Существует естественное эквивалентность между категорией коконов типа над F и категорией коконов над F. Конкретно: имея кокон типа с точкой в Type u, получаем кокон над F, используя те же отображения; обратно — из кокона над F восстанавливаем кокон типа, взяв базовую точку и композицию с универсальными отображениями.
LaTeX
$$$$ \text{coconeTypesEquiv} : \CoconeTypes(F) \simeq \Cocone(F). $$$$
Lean4
/-- If `F : J ⥤ Type u`, then the data of a "type-theoretic" cocone of `F`
with a point in `Type u` is the same as the data of a cocone (in a categorical sense). -/
@[simps]
def coconeTypesEquiv : CoconeTypes.{u} F ≃ Cocone F
where
toFun
c :=
{ pt := c.pt
ι := { app j := c.ι j } }
invFun
c :=
{ pt := c.pt
ι j := c.ι.app j
ι_naturality := c.w }
left_inv _ := rfl
right_inv _ := rfl
