Def CategoryTheory.Equalizer.Presieve.Arrows.SecondObj

Modification history

2024-05-12 16:16

Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

chore(CategoryTheory/Sites): generalise universes for extensive sheaves (#12801)

Modified CategoryTheory.Equalizer.Presieve.Arrows.SecondObj View on Github →

2023-11-03 09:34

Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

feat: categorical sheaf condition for presieves of arrows (#7918) …

Added CategoryTheory.Equalizer.Presieve.Arrows.SecondObj View on Github →