Notwithstanding that we're using a symmetric monoidal category rather than the weaker notion of a balanced monoidal category, and eliding the necessary reassociations, Joyal's law is something more like trace (id ⊗₁ σ⇒ ∘ f ⊗₁ g ∘ id ⊗ σ⇐) ≈ trace f ⊗₁ id than the library's trace (id ⊗₁ f) ≈ id ⊗₁ trace f, which seems to be a lot weaker.
In "A survey of graphical languages for monoidal categories", Selinger suggests an alternative to the superposing law, strength : trace (g ⊗₁ f) ≈ g ⊗₁ f, which looks related to but stronger than the law that we have.