(C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi C) ≅
      (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)).comp
        (CategoryTheory.Idempotents.KaroubiKaroubi.inverse C)