Def CategoryTheory.EqualizerSecondObjIso

Modification history

2023-11-17 00:15
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
refactor(CategoryTheory): simplify the proof of the characterisation of regular sheaves using the new arrows API (#8443)
Deleted CategoryTheory.EqualizerSecondObjIsoView on Github →
2023-11-13 12:59
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
fix: remove unused arguments (#8380) …
Modified CategoryTheory.EqualizerSecondObjIsoView on Github →
2023-10-20 14:35
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat: description of sheaves for regular sieves (#6919) …
Added CategoryTheory.EqualizerSecondObjIsoView on Github →