tricocycloid axioms from a guarded pentagon

Tags: Coherence for monoidal categories, rewriting, tricocycloids, guarded command language.