Theorems · Definition · category theory

CategoryTheory.Precoverage.ZeroHypercover.bind

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {T : C} →
        [J.IsStableUnderComposition] →
          (E : J.ZeroHypercover T) → ((i : E.I₀) → J.ZeroHypercover (E.X i)) → J.ZeroHypercover T

Refining each component of a 0-hypercover yields a refined 0-hypercover of the base.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

8 results in Mathlib

Foundations

Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Precoverage.IsStableUnderComposition