# 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?
• I got help on the Agda/Cubical issue tracker. Apparently, it is better to use equivalence induction. Now, I only have to prove the simplified base case (λ i → ua (idEquiv A) (~ i)) ≡ ua (invEquiv (idEquiv A)). – sryscad May 27 '19 at 10:52
• Since $ua(f^{-1}) = ua(f)^{-1}$ holds (HoTT book, just below UA in Sect 2.10), your statement should hold. Note that $f^{-1}$ is the inverse equivalence, while $ua(f)^{-1}$ is the inverse path. As long as iso inverses are equivalence inverses, everything should be OK. (The part about the built-in functions looks off-topic here, unfortunately -- I don't know much about that library anyway) – chi May 27 '19 at 13:00
• @chi, Thank you! I found that statement in the book as well. To prove it, I switched from isomorphisms to equivalences and used equivalence induction from the Agda Cubical library. I will try to post a full answer to my question below to mark this question as solved. – sryscad May 28 '19 at 13:12

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