Reversing an application of `sym` to `ua` and `isoToEquiv` in cubical type theory
The original  statement in my question 
sym (ua (isoToEquiv fIso)) ≡ ua (isoToEquiv (invIso fIso))
is a valid statement in Homotopy Type Theory but because (homotopy-) isomorphisms are a special case of equivalences, the statement can be generalized to

sym (ua fEquiv) ≡ (ua (invEquiv fEquiv)) (*)

It is one of the properties of ua that are informally proven in the Univalent Foundations book in section 2.10.

Solution

The results from 1 have been implemented and proven in the lemmas in the Agda Cubical library. The function uaInvEquiv of those lemmas in particular solves my problem (*). For future applications it is better to use 4 because they are more general than my own approach below.



Historical solution

Using the hint to use EquivJ, I gave a proof for the theorem that may not be the most efficient one but it worked (typechecked) for my specific case:

baseIndLemma : (A : Type ℓ-zero) → (λ i → ua (idEquiv A) (~ i)) ≡ ua (invEquiv (idEquiv A))
baseIndLemma A = 
  sym ( ua (idEquiv A) ) ≡⟨ uaIdEquiv ⟩
  sym refl ≡⟨ refl ⟩
  refl ≡⟨ sym uaIdEquiv ⟩
  ua (idEquiv A) ≡⟨ cong ua (equivEq (idEquiv A) (invEquiv (idEquiv A)) refl) ⟩
  ua (invEquiv (idEquiv A)) ∎

myUaInvEquiv : sym (ua fEquiv) ≡ (ua (invEquiv fEquiv))
myUaInvEquiv = EquivJ
  (λ _ _ e → sym (ua e) ≡ ua (invEquiv e)) (λ A → baseIndLemma A) ℕ₀ ℕ fEquiv