feat(category_theory/limits/terminal): constructor for is_terminal (#…

…6929)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/limits/shapes/terminal.lean

@@ -33,6 +33,14 @@ abbreviation is_terminal (X : C) := is_limit (as_empty_cone X)
 /-- `X` is initial if the cocone it induces on the empty diagram is colimiting. -/
 abbreviation is_initial (X : C) := is_colimit (as_empty_cocone X)
 
+/-- An object `Y` is terminal if for every `X` there is a unique morphism `X ⟶ Y`. -/
+def is_terminal.of_unique (Y : C) [h : Π X : C, unique (X ⟶ Y)] : is_terminal Y :=
+{ lift := λ s, (h s.X).default }
+
+/-- An object `X` is initial if for every `Y` there is a unique morphism `X ⟶ Y`. -/
+def is_initial.of_unique (X : C) [h : Π Y : C, unique (X ⟶ Y)] : is_initial X :=
+{ desc := λ s, (h s.X).default }
+
 /-- Give the morphism to a terminal object from any other. -/
 def is_terminal.from {X : C} (t : is_terminal X) (Y : C) : Y ⟶ X :=
 t.lift (as_empty_cone Y)