Be Careful with Duoidal Coherence
- Article (pdf).
Abstract: There may exist two different maps of type I⊲I → I constructed out of the structure maps of a duoidal category. This is well-known, but it is easy to get confused by the literature. In contrast, normal duoidal categories are coherent in the sense that there exists at most a unique map between any two distinctly typed expressions.