We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent a868975 commit 5beccabCopy full SHA for 5beccab
theories/Algebra/Categorical/MonoidObject.v
@@ -101,7 +101,7 @@ Section ComonoidObject.
101
:: IsCommutativeMonoidObject (A:=A^op) tensor unit x.
102
103
(** We can build cocommutative comonoid objects from the following data: *)
104
- Definition Build_IsCocommutatativeComonoidObject (x : A)
+ Definition Build_IsCocommutativeComonoidObject (x : A)
105
(** A comonoid. *)
106
`{!IsComonoidObject x}
107
(** Together with a proof of cocommutativity. *)
0 commit comments