Help with reversing an application of `sym` to `ua` and `isoToEquiv` about cubical HOT 5 CLOSED

Forgetting about isomorphisms, what you want to prove is that symmetry of equivalences and symmetry of paths are invariant under univalence. You can find this lemma straight after the univalence axiom is introduced in 2.10.3 in the HoTT book.

For cubical type theory, this should be even easier.

from cubical.

Thanks, @Alizter ! You probably mean ua(f)^{−1} = ua(f^{−1})? I will try to implement this in cubical type theory.

from cubical.

@wvhulle It should be fairly direct from EquivJ

from cubical.

I proved this now: #147

from cubical.

@mortberg , that's very friendly! :) This was my solution for my particular problem:

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 

Unfortunately, normalizing the endresult of the rest of my code (a transport of some proof) results in a memory leak, but i should probably make a separate issue for that.

from cubical.