Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

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 Apr 2, 2021
1 parent 881ee5b commit c850a9c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/category_theory/limits/creates.lean
Original file line number Diff line number Diff line change
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 c850a9c

Please sign in to comment.