Skip to content

Commit

Permalink
chore(category_theory/whiskering): Fix docstring (#8533)
Browse files Browse the repository at this point in the history
  • Loading branch information
adamtopaz committed Aug 4, 2021
1 parent d24faea commit ee8e447
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/category_theory/whiskering.lean
Expand Up @@ -104,7 +104,7 @@ rfl

/--
If `α : G ≅ H` then
`iso_whisker_right α F : (G ⋙ F) ≅ (G ⋙ F)` has components `F.map_iso (α.app X)`.
`iso_whisker_right α F : (G ⋙ F) ≅ (H ⋙ F)` has components `F.map_iso (α.app X)`.
-/
def iso_whisker_right {G H : C ⥤ D} (α : G ≅ H) (F : D ⥤ E) : (G ⋙ F) ≅ (H ⋙ F) :=
((whiskering_right C D E).obj F).map_iso α
Expand Down

0 comments on commit ee8e447

Please sign in to comment.