Finality on Costructured Arrow categories

References

• [M. Kashiwara, P. Schapira, Categories and Sheaves][Kashiwara2006], Proposition 3.1.8(i)

theorem CategoryTheory.Functor.final_of_final_costructuredArrowToOver {A : Type u₁} [Category.{v₁, u₁} A] {B : Type u₂} [Category.{v₂, u₂} B] {T : Type u₃} [Category.{v₃, u₃} T] (L : Functor A T) (R : Functor B T) [R.Final] [hB : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final] : L.Final

A functor L : A ⥤ T is final if there is a final functor R : B ⥤ T such that for all b : B, the canonical functor CostructuredArrow L (R.obj b) ⥤ Over (R.obj b) is final.