∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ L₃ : CategoryTheory.Functor C D} {R₁ R₂ R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (adj₃ : L₃ ⊣ R₃) (α : L₂ ⟶ L₁) (β : L₃ ⟶ L₂) {Z : CategoryTheory.Functor D C} (h : R₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₂ adj₃) β) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.conjugateEquiv adj₁ adj₃) (CategoryTheory.CategoryStruct.comp β α)) h