feat(category_theory): formally adjoined initial objects are strict (#…

…7222)
leanprover-community · Apr 17, 2021 · 560a009 · 560a009
1 parent 89c16a7
commit 560a009
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/category_theory/with_terminal.lean b/src/category_theory/with_terminal.lean
@@ -202,6 +202,9 @@ lift_unique F (λ z, hZ.from _) (λ x y f, hZ.hom_ext _ _) G h hG (λ x, hZ.hom_
 @[simp]
 def hom_from (X : C) : incl.obj X ⟶ star := star_terminal.from _
 
+instance is_iso_of_from_star {X : with_terminal C} (f : star ⟶ X) : is_iso f :=
+by tidy
+
 end with_terminal
 
 namespace with_initial
@@ -361,6 +364,9 @@ lift_unique F (λ z, hZ.to _) (λ x y f, hZ.hom_ext _ _) G h hG (λ x, hZ.hom_ex
 @[simp]
 def hom_to (X : C) : star ⟶ incl.obj X := star_initial.to _
 
+instance is_iso_of_to_star {X : with_initial C} (f : X ⟶ star) : is_iso f :=
+by tidy
+
 end with_initial
 
 end category_theory