6
$\begingroup$

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?
$\endgroup$
  • $\begingroup$ 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)). $\endgroup$ – sryscad May 27 at 10:52
  • 1
    $\begingroup$ 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) $\endgroup$ – chi May 27 at 13:00
  • $\begingroup$ @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. $\endgroup$ – sryscad May 28 at 13:12
3
$\begingroup$

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 
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.