Commit 2020-09-01 04:50 7cd67b56

View on Github →

feat(category_theory/limits/shapes/terminal): is_terminal object (#3957) Add language to talk about when an object is terminal, and generalise some results to use this

Estimated changes

Modified src/category_theory/closed/cartesian.lean

added theorem category_theory.initial_mono

modified def category_theory.mul_zero

modified def category_theory.pow_zero

added def category_theory.strict_initial

modified def category_theory.zero_mul

Modified src/category_theory/limits/shapes/terminal.lean

added def category_theory.limits.as_empty_cocone

added def category_theory.limits.as_empty_cone

added def category_theory.limits.initial_is_initial

added theorem category_theory.limits.is_initial.epi_to

added theorem category_theory.limits.is_initial.hom_ext

added def category_theory.limits.is_initial.to

added def category_theory.limits.is_initial

added def category_theory.limits.is_terminal.from

added theorem category_theory.limits.is_terminal.hom_ext

added theorem category_theory.limits.is_terminal.mono_from

added def category_theory.limits.is_terminal

added def category_theory.limits.terminal_is_terminal