∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] {K : CategoryTheory.Functor J C} (Y : D)
  (t : ((CategoryTheory.cocones J D).obj (Opposite.op (K.comp F))).obj Y),
  adj.coconesIsoComponentHom Y t = { app := fun j => (adj.homEquiv (K.obj j) Y) (t.app j), naturality := ⋯ }