|Maintainer||Edward Kmett <firstname.lastname@example.org>|
NB: this contradicts another common meaning for an
Category, which is one
where the pentagonal condition does not hold, but for which there is an identity.
A category with an associative bifunctor satisfying Mac Lane's pentagonal coherence identity law:
bimap id associate . associate . bimap associate id = associate . associate
A category with a coassociative bifunctor satisyfing the dual of Mac Lane's pentagonal coherence identity law:
bimap coassociate id . coassociate . bimap id coassociate = coassociate . coassociate