∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.map₂ α β).obj X).hom =
    CategoryTheory.CategoryStruct.comp (α.app X.left) (CategoryTheory.CategoryStruct.comp (G.map X.hom) β)