Idempotent completeness of categories of simplicial objects

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

instance CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObjectInstCategorySimplicialObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.IsIdempotentComplete C] : CategoryTheory.IsIdempotentComplete (CategoryTheory.SimplicialObject C)

Equations

• ⋯ = ⋯

instance CategoryTheory.Idempotents.instIsIdempotentCompleteCosimplicialObjectInstCategoryCosimplicialObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.IsIdempotentComplete C] : CategoryTheory.IsIdempotentComplete (CategoryTheory.CosimplicialObject C)

Equations

• ⋯ = ⋯