This PR implements Kernels and Normal Monomorphisms, which moves us closer to being able to use agda-categories to do some group theory!
Notes
I took this opportunity to split up equalizers into a bundled and predicate form, as this is going to be useful when we start working with regular morphisms (of which normal morphisms are a subset).
TOTBWF
commented
3 years ago
Patch Description
This PR implements Kernels and Normal Monomorphisms, which moves us closer to being able to use
agda-categoriesto do some group theory!Notes
I took this opportunity to split up equalizers into a bundled and predicate form, as this is going to be useful when we start working with regular morphisms (of which normal morphisms are a subset).
References:
https://ncatlab.org/nlab/show/kernel https://ncatlab.org/nlab/show/normal+monomorphism