Theorems · Inductive type · category theory

CategoryTheory.Precoverage.ZeroHypercover

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → C → Type (max (max u v) (w + 1))

The type of 0-hypercovers of an object S : C in a category equipped with a coverage J. This can be constructed from a covering of S.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

81 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category