∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} {adj₁ : L ⊣ F} {adj₂ : F ⊣ G} {adj₃ : G ⊣ R} {adj₁_1 : L ⊣ F} {adj₂_1 : F ⊣ G}
  {adj₃_1 : G ⊣ R},
  { adj₁ := adj₁, adj₂ := adj₂, adj₃ := adj₃ } = { adj₁ := adj₁_1, adj₂ := adj₂_1, adj₃ := adj₃_1 } →
    adj₁ = adj₁_1 ∧ adj₂ = adj₂_1 ∧ adj₃ = adj₃_1