∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {T : Type u_2}
  (F : CategoryTheory.Functor C (CategoryTheory.Discrete T)) (t : T) [inst_1 : Subsingleton T]
  {X Y : CategoryTheory.CostructuredArrow F { as := t }} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow F { as := t })).map f)
      ((fun x =>
            CategoryTheory.CostructuredArrow.isoMk
              (CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow F { as := t })).obj x).left)
              ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            CategoryTheory.CostructuredArrow.isoMk
              (CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow F { as := t })).obj x).left)
              ⋯)
          X).hom
      (((CategoryTheory.CostructuredArrow.proj F { as := t }).comp
            { obj := fun X => CategoryTheory.CostructuredArrow.mk (CategoryTheory.eqToHom ⋯),
              map := fun {X Y} f => CategoryTheory.CostructuredArrow.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }).map
        f)