Theorems · Inductive type · category theory

CategoryTheory.Precoverage

(C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max u_1 v_1)

A precoverage is a collection of covering presieves on every object X : C. See CategoryTheory.Coverage and CategoryTheory.Pretopology for common extensions of this.

Defined in

Mathlib.CategoryTheory.Sites.Precoverage

Cited by

204 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category