(C : Type u_1) →
  (D : Type u_2) →
    (E : Type u_3) →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            (F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)) →
              (G : CategoryTheory.Functor D (CategoryTheory.Idempotents.Karoubi E)) →
                (CategoryTheory.Idempotents.functorExtension₁ C E).obj
                    (F.comp ((CategoryTheory.Idempotents.functorExtension₁ D E).obj G)) ≅
                  ((CategoryTheory.Idempotents.functorExtension₁ C D).obj F).comp
                    ((CategoryTheory.Idempotents.functorExtension₁ D E).obj G)