∀ (T : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} T],
  Function.LeftInverse (fun x => CategoryTheory.Arrow.mk x.snd.snd) fun f =>
    ⟨(CategoryTheory.Functor.id T).obj f.left, ⟨(CategoryTheory.Functor.id T).obj f.right, f.hom⟩⟩