mathlib documentation

category_theory.idempotents.karoubi_karoubi

Idempotence of the Karoubi envelope #

In this file, we construct the equivalence of categories karoubi_karoubi.equivalence C : karoubi C ≌ karoubi (karoubi C) for any category C.