PD: Matt points out that there is an equation missing for the inclusion of the base category. Tags: effectful categories.
