Skip to content

Commit

Permalink
Update theories/WildCat/Monoidal.v
Browse files Browse the repository at this point in the history
Co-authored-by: Dan Christensen <[email protected]>
  • Loading branch information
Alizter and jdchristensen authored Oct 21, 2024
1 parent 7f07801 commit f075c99
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/WildCat/Monoidal.v
Original file line number Diff line number Diff line change
Expand Up @@ -1060,7 +1060,7 @@ Class IsMonoidalFunctor {A B : Type}
(uncurry (fun a b => tensorB (F a) (F b)))
(uncurry (fun a b => F (tensorA a b)));

(** A morhpism [fmap_unit] relating the two unit objects. *)
(** A morphism [fmap_unit] relating the two unit objects. *)
fmap_unit : IB $-> F (IA);

(** Such that the following coherence conditions hold:
Expand Down

0 comments on commit f075c99

Please sign in to comment.