Commit 2023-06-07 06:36 1a729bdb

View on Github →

feat: port CategoryTheory.Sites.Types (#4776)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Types.lean

added def CategoryTheory.discretePresieve

added def CategoryTheory.discreteSieve

added theorem CategoryTheory.discreteSieve_mem

added def CategoryTheory.eval

added theorem CategoryTheory.eval_app

added theorem CategoryTheory.eval_map

added theorem CategoryTheory.eval_typesGlue

added theorem CategoryTheory.generate_discretePresieve_mem

added theorem CategoryTheory.isSheaf_yoneda'

added theorem CategoryTheory.subcanonical_typesGrothendieckTopology

added theorem CategoryTheory.typesGlue_eval

added def CategoryTheory.typesGrothendieckTopology

added theorem CategoryTheory.typesGrothendieckTopology_eq_canonical

added def CategoryTheory.yoneda'

added theorem CategoryTheory.yoneda'_comp