I motivate a variation (due to K. Szlachányi) of monoidal categories called skewmonoidal categories where the unital and associativity laws are not required to be isomorphisms, only natural transformations. Coherence has to be formulated differently than in the wellknown monoidal case. In my (to my knowledge new) version it becomes a statement of uniqueness of normalizing rewrites. I present a proof of this coherence theorem and also formalize it fully in the dependently typed programming language Agda.
