∀ {A : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} A] {B : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} B] {T : Type u_2} [inst_2 : CategoryTheory.Category.{u_1, u_2} T]
  (R : CategoryTheory.Functor B T) {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₁ ⟶ L₂),
  l = l' →
    ∀ (X : CategoryTheory.Comma L₂ R),
      CategoryTheory.CategoryStruct.comp
          (L₁.map (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapLeft R l).obj X).left).hom)
          ((CategoryTheory.Comma.mapLeft R l').obj X).hom =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Comma.mapLeft R l).obj X).hom
          (R.map (CategoryTheory.Iso.refl ((CategoryTheory.Comma.mapLeft R l).obj X).right).hom)