∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] (X : T) ⦃X_1 Y : CategoryTheory.Over X⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.forget X).map f) Y.hom =
    CategoryTheory.CategoryStruct.comp X_1.hom (((CategoryTheory.Functor.const (CategoryTheory.Over X)).obj X).map f)