1lab
1lab copied to clipboard
plt-amy
wip: elementary topos nonsense
New pages
- Cat.Instances.Sheaf.Omega (+439, -0)
- Cat.Diagram.Omega (+362, -0)
- Cat.Instances.Presheaf.Omega (+259, -0)
- Cat.Instances.Presheaf.Limits (+214, -0)
- Cat.Displayed.Instances.Subobjects.Reasoning (+141, -0)
- Cat.Instances.Presheaf.Exponentials (+129, -0)
- Cat.Diagram.Pullback.Along (+125, -0)
- Cat.Instances.FinSets.Omega (+118, -0)
- Cat.Instances.Presheaf.Colimits (+110, -0)
- Cat.Instances.Sheaf.Limits.Finite (+96, -0)
Changed pages
- Cat.Displayed.Instances.Subobjects (+43, -24)
- Cat.Instances.Sheaves (+6, -53)
- Cat.Diagram.Pullback (+16, -0)
- Cat.Functor.Morphism (± 8)
- Cat.Morphism (+14, -0)
- Topoi.Reasoning (± 6)
- Cat.Displayed.Instances.Comma (+6, -5)
- Cat.Instances.Sheaf.Exponentials (± 5)
What needs to be done to take this out of draft status? Working on injective objects right now, and I'd like to show that every subobject classifier is injective 🙂
