mathlib documentation

category_theory.idempotents.simplicial_object

Idempotent completeness of categories of simplicial objects #

In this file, we provide an instance expressing that simplicial_object C and cosimplicial_object C are idempotent complete categories when the category C is.