Formalizing equivalences without tears

TL;DR

This paper presents two practical techniques in homotopy type theory for proving that a map is an equivalence, simplifying the process through decomposition and the 3-for-2 property, with illustrative examples.

Contribution

It introduces two convenient methods for formalizing equivalences in homotopy type theory, enhancing proof strategies and formalization ease.

Findings

Techniques effectively decompose complex equivalences.

Refinement using 3-for-2 property simplifies proofs.

Illustrated with a fundamental synthetic homotopy theory result.

Abstract

This expository note describes two convenient techniques in the context of homotopy type theory for proving and formalizing that a given map is an equivalence. The first technique decomposes the map as a series of basic equivalences, while the second refines this approach using the 3-for-2 property of equivalences. The techniques are illustrated by proving a basic result in synthetic homotopy theory.