∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} {adj₁ : F ⊣ G} {adj₂ : G ⊣ H} {adj₁_1 : F ⊣ G} {adj₂_1 : G ⊣ H},
  { adj₁ := adj₁, adj₂ := adj₂ } = { adj₁ := adj₁_1, adj₂ := adj₂_1 } → adj₁ = adj₁_1 ∧ adj₂ = adj₂_1