∀ {A : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{u_4, u_2} B] {T : Type u_6} [inst_2 : CategoryTheory.Category.{u_3, u_6} T]
  (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T) {X Y : (CategoryTheory.Comma R.op L.op)ᵒᵖ}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Comma.unopFunctor R L).leftOp.comp (CategoryTheory.Comma.opFunctor L R)).map f)
      ((fun X =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.Comma.unopFunctor R L).leftOp.comp (CategoryTheory.Comma.opFunctor L R)).obj X))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            CategoryTheory.Iso.refl
              (((CategoryTheory.Comma.unopFunctor R L).leftOp.comp (CategoryTheory.Comma.opFunctor L R)).obj X))
          X).hom
      ((CategoryTheory.Functor.id (CategoryTheory.Comma R.op L.op)ᵒᵖ).map f)