We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent c6c8c8d commit a868975Copy full SHA for a868975
theories/Algebra/Categorical/MonoidObject.v
@@ -106,7 +106,7 @@ Section ComonoidObject.
106
`{!IsComonoidObject x}
107
(** Together with a proof of cocommutativity. *)
108
(cco_cocomm : braid x x $o co_comult $== co_comult)
109
- : IsCocommuativeComonoidObject x.
+ : IsCocommutativeComonoidObject x.
110
Proof.
111
snrapply Build_IsCommutativeMonoidObject.
112
- exact _.
0 commit comments