Commit 2020-02-22 12:05 eabcd132
View on Github →feat(category_theory/limits): kernels (#1988)
- chore(category_theory): require morphisms live in Type
- move back to Type
- fixes
- feat(category_theory/limits): kernels
- finishing basic API for kernels
- update post #1412
- fix
- documentation
- documentation
- more docs
- replacing dumb code
- forall -> Pi
- removing all instances
- working on Reid's suggested lemmas
- experiments
- lots to do
- Show that equalizers are monomorphisms
- Show that equalizer of (f, f) is always an iso
- Show that an equalizer that is an epimorphism is an isomorphism
- Clean up
- Show that the kernel of a monomorphism is zero
- Fix
- Show that the kernel of a linear map is a kernel in the categorical sense
- Modify proof
- Compactify proof
- Various cleanup
- Some more cleanup
- Fix bibtex
- Address some issues raised during discussion of the PR
- Fix some more incorrect indentation
- Some more minor fixes
- Unify capitalization in Bibtex entries
- Replace equalizer.lift.uniq with equalizer.hom_ext
- Some more slight refactors
- Typo