∀ {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₂ 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 (CategoryTheory.CategoryStruct.comp l l')).obj X).left).hom)
      (((CategoryTheory.Comma.mapLeft R l').comp (CategoryTheory.Comma.mapLeft R l)).obj X).hom =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.comp l l')).obj X).hom
      (R.map
        (CategoryTheory.Iso.refl
            ((CategoryTheory.Comma.mapLeft R (CategoryTheory.CategoryStruct.comp l l')).obj X).right).hom)