Reversing an application of `sym` to `ua` and `isoToEquiv` in cubical type theory

I am proving a kind of structure invariance principle for magmas in Cubical Type Theory with the Agda/Cubical library. This is done by constructing a path between two simple magmas and then transporting proofs of simple properties about this path. I have already obtained most of the proof (see my code repository) but did not manage yet to complete the following lemma.

At some point in the proof I have the following given:

• A bijection between types: `f : ℕ → ℕ₀`
• The isomorphism constructed with `f`: `fIso : Iso ℕ ℕ₀`
• A function that gives the inverse isomorphism of an isomorphism: `invIso : Iso A B → Iso B A`

Now, I would like to prove that:

``sym (ua (isoToEquiv fIso)) ≡ ua (isoToEquiv (invIso fIso)) ``

There are two parts to my question:

• Is this a valid theorem in HoTT? Although this statement seems valid, maybe I have produced a false statement?
• Are there built-in functions in the Agda/Cubical that may help in the proof?