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.
@[protected, instance]
@[protected, instance]