Theorems · Inductive type · category theory

CategoryTheory.GrothendieckTopology.OneHypercover

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

The type of 1-hypercovers of an object S : C in a category equipped with a Grothendieck topology J. This can be constructed from a covering of S and a covering of the fibre products of the objects in this covering (see OneHypercover.mk').

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

44 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category