Contractible Čech complexes

A member of a cover receiving a map from a terminal object contracts the positive-degree Čech complex of every presheaf on that cover.

theorem CategoryTheory.cechComplex_exactAt_succ_of_isTerminal {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] {A : Type u'} [Category.{v', u'} A] [Abelian A] [Limits.HasProducts A] {ι : Type w} (U : ι → C) {T : C} (hT : Limits.IsTerminal T) {i₀ : ι} (d : T ⟶ U i₀) (P : Functor Cᵒᵖ A) (n : ℕ) : HomologicalComplex.ExactAt ((cechComplexFunctor U).obj P) (n + 1)

A member of a family receiving a map from a terminal object contracts the positive-degree Čech complex of every presheaf on that family.