Commit 2021-06-27 13:01 2dcc307e
View on Github →feat(category_theory/limits): morphism to terminal is split mono (#8084)
A generalisation of existing results: we already have an instance split_mono to mono so this is strictly more general.
feat(category_theory/limits): morphism to terminal is split mono (#8084)
A generalisation of existing results: we already have an instance split_mono to mono so this is strictly more general.