∀ {T : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X)
  {X_1 Y : T} (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y), map := fun {X_2 Y} f => CategoryTheory.Over.homMk f ⋯,
                map_id := ⋯, map_comp := ⋯ }.comp
            (CategoryTheory.Over.forget X)).map
        f)
      ((fun x =>
            CategoryTheory.Iso.refl
              (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y),
                        map := fun {X_2 Y} f => CategoryTheory.Over.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp
                    (CategoryTheory.Over.forget X)).obj
                x))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.Iso.refl
              (({ obj := fun Y => CategoryTheory.Over.mk (hX.from Y),
                        map := fun {X_2 Y} f => CategoryTheory.Over.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }.comp
                    (CategoryTheory.Over.forget X)).obj
                x))
          X_1).hom
      ((CategoryTheory.Functor.id T).map f)