https://github.com/math-comp/hierarchy-builder/blob/e4e487dde779430360567533e3169c3bd3f8b556/examples/cat/cat.v#L889 `PreCat_IsMonoidal` looks like a typo and `PreCat_IsPreMonoidal` would be more consistent. (Or is this intentionally `PreCat_IsMonoidal`?)
hierarchy-builder/examples/cat/cat.v
Line 889 in e4e487d
PreCat_IsMonoidallooks like a typo andPreCat_IsPreMonoidalwould be more consistent.(Or is this intentionally
PreCat_IsMonoidal?)