feat(category_theory/limits): strict initial objects are initial mono (…

…#8267)

- [x] depends on: #8094 
- [x] depends on: #8099

src/category_theory/limits/shapes/strict_initial.lean

@@ -78,6 +78,10 @@ lemma is_initial.subsingleton_to (hI : is_initial I) {A : C} :
   subsingleton (A ⟶ I) :=
 ⟨hI.strict_hom_ext⟩
 
+@[priority 100] instance initial_mono_of_strict_initial_objects : initial_mono_class C :=
+{ is_initial_mono_from := λ I A hI,
+  { right_cancellation := λ B g h i, hI.strict_hom_ext _ _ } }
+
 /-- If `I` is initial, then `X ⨯ I` is isomorphic to it. -/
 @[simps hom]
 noncomputable def mul_is_initial (X : C) [has_binary_product X I] (hI : is_initial I) :

src/category_theory/limits/shapes/terminal.lean

@@ -222,8 +222,7 @@ initial object, see `initial.mono_from`.
 Given a terminal object, this is equivalent to the assumption that the unique morphism from initial
 to terminal is a monomorphism, which is the second of Freyd's axioms for an AT category.
 
-TODO: This is a condition satisfied by categories with zero objects and morphisms, as well as
-categories with a strict initial object; though these conditions are essentially mutually exclusive.
+TODO: This is a condition satisfied by categories with zero objects and morphisms.
 -/
 class initial_mono_class (C : Type u) [category.{v} C] : Prop :=
 (is_initial_mono_from : ∀ {I} (X : C) (hI : is_initial I), mono (hI.to X))