Finality of Projections in Comma Categories

We show that fst L R is final if R is and that snd L R is initial if L is.

instance CategoryTheory.Comma.final_fst {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [R.Final] : (CategoryTheory.Comma.fst L R).Final

Equations

• ⋯ = ⋯

instance CategoryTheory.Comma.initial_snd {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) [L.Initial] : (CategoryTheory.Comma.snd L R).Initial

Equations

• ⋯ = ⋯