Skip to content

Commit

Permalink
chore(category_theory/limits/creates): fix typo in docstring (#6738)
Browse files Browse the repository at this point in the history
  • Loading branch information
b-mehta committed Mar 17, 2021
1 parent 6e1143a commit 9507a34
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/category_theory/limits/creates.lean
Expand Up @@ -279,7 +279,7 @@ instance preserves_limits_of_creates_limits_and_has_limits (F : C ⥤ D) [create
category_theory.preserves_limit_of_shape_of_creates_limits_of_shape_and_has_limits_of_shape F }

/--
If `F` reflects isomorphisms and we can lift any limit cocone to a limit cocone,
If `F` reflects isomorphisms and we can lift any colimit cocone to a colimit cocone,
then `F` creates colimits.
In particular here we don't need to assume that F reflects colimits.
-/
Expand Down

0 comments on commit 9507a34

Please sign in to comment.