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
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
