CategoryTheory.CommaMorphism.ext

theorem CategoryTheory.CommaMorphism.ext : ∀ {A : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} A} {B : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} B} {T : Type u₃} {inst_2 : CategoryTheory.Category.{v₃, u₃} T} {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} (x y : CategoryTheory.CommaMorphism X Y), x.left = y.left → x.right = y.right → x = y

This theorem states that in category theory, given any two categories `A` and `B` with another category `T`, and two functors `L` from `A` to `T` and `R` from `B` to `T`, for any two objects `X` and `Y` in the comma category formed by `L` and `R`, if we have two morphisms `x` and `y` from `X` to `Y` in the comma category, then `x` and `y` are equal if and only if their left and right components are equal. This is essentially asserting that a morphism in the comma category is uniquely determined by its two components.

More concisely: In category theory, given functors L from category A to T and R from category B to T, morphisms x and y in the comma category L,R := {(f : A → T) | ∃ g : B → T, L(g)(f) = R(h)(f) for some h : B → A} are equal if and only if their left and right components are equal.