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

Commit 74b65e2

Browse files
kim-emdigama0
authored andcommitted
fix(category_theory/limits): change argument order on
cones.precompose/whisker
1 parent 4b0a82c commit 74b65e2

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

category_theory/limits/cones.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -90,11 +90,11 @@ namespace cone
9090
{ X := X,
9191
π := c.extensions.app X f }
9292

93-
def postcompose {G : J ⥤ C} (c : cone F) (α : F ⟹ G) : cone G :=
93+
def postcompose {G : J ⥤ C} (α : F ⟹ G) (c : cone F) : cone G :=
9494
{ X := c.X,
9595
π := c.π ⊟ α }
9696

97-
def whisker (c : cone F) {K : Type v} [small_category K] (E : K ⥤ J) : cone (E ⋙ F) :=
97+
def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cone F) : cone (E ⋙ F) :=
9898
{ X := c.X,
9999
π := whisker_left E c.π }
100100

@@ -112,11 +112,11 @@ namespace cocone
112112
{ X := X,
113113
ι := c.extensions.app X f }
114114

115-
def precompose {G : J ⥤ C} (c : cocone F) (α : G ⟹ F) : cocone G :=
115+
def precompose {G : J ⥤ C} (α : G ⟹ F) (c : cocone F) : cocone G :=
116116
{ X := c.X,
117117
ι := α ⊟ c.ι }
118118

119-
def whisker (c : cocone F) {K : Type v} [small_category K] (E : K ⥤ J) : cocone (E ⋙ F) :=
119+
def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cocone F) : cocone (E ⋙ F) :=
120120
{ X := c.X,
121121
ι := whisker_left E c.ι }
122122

0 commit comments

Comments
 (0)