8.1.4 The encode-decode proof
We begin with the functionΒ (LABEL:eq:pi1s1-encode) that maps paths to codes:
Definition 8.1.1.
Encode is defined by lifting a path into the universal cover, which
determines an equivalence, and then applying the resulting equivalence
to .
The interesting thing about this function is that it computes a concrete
number from a loop on the circle, when this loop is represented using
the abstract groupoidal framework of homotopy type theory. To gain an
intuition for how it does this, observe that by the above lemmas,
is the successor
map and is the predecessor map.
Further, is functorial (\autorefcha:basics), so
is
and so on. Thus, when is a composition like
will compute a composition of functions like
Applying this composition of functions to 0 will compute the
winding number of the pathβhow many times it goes around the
circle, with orientation marked by whether it is positive or negative,
after inverses have been canceled. Thus, the computational behavior of
follows from the reduction
rules for higher-inductive types and
univalence, and the action of on compositions and inverses.
Note that the instance has type . This will be one half of our desired equivalence; indeed, it is exactly the function defined in \autorefsec:pi1s1-initial-thoughts.
Similarly, the functionΒ (LABEL:eq:pi1s1-decode) is a generalization of the function from \autorefsec:pi1s1-initial-thoughts.
Definition 8.1.2.
Define by
circle induction on . It suffices to give a function
, for which we use , and
to show that respects the loop.
Proof.
To show that respects the loop, it suffices to give a path from to itself that lies over . By the definition of dependent paths, this means a path from
to . We define such a path as follows:
On the first line, we apply the characterization of
when the outer connective
of the fibration
is , which
reduces the to pre- and post-composition with
at the domain and codomain types. On the second line,
we apply the characterization of when the type family
is , which is post-composition of paths. On the third line,
we use the action of on from
\autoreflem:transport-s1-code. And on the fourth line, we simply
reduce the function composition. Thus, it suffices to show that for all
, , which is an easy
induction, using the groupoid
laws.
β
We can now show that and are quasi-inverses. What used to be the difficult direction is now easy!
Lemma 8.1.3.
For all for all and , .
Proof.
By path induction, it suffices to show that But and . β
The other direction is not much harder.
Lemma 8.1.4.
For all and , we have .
Proof.
The proof is by circle induction. It suffices to show the case for , because the case for is a path between paths in , which is immediate because is a set.
Thus, it suffices to show, for all , that
The proof is by induction, using \crefthm:looptothe.
-
β’
In the case for , the result is true by definition.
-
β’
In the case for ,
(by definition of $\mathsf{loop}^{\mathord{\hskip1.0pt\text{--}\hskip1.0pt}}$) (by definition of $\mathsf{encode}$) (by functoriality) (by \autoreflem:transport-s1-code) (by the inductive hypothesis) -
β’
The case for negatives is analogous. β
Finally, we conclude the theorem.
Theorem 8.1.5.
There is a family of equivalences .
Proof.
The maps and are quasi-inverses by \autoreflem:s1-decode-encode,\autoreflem:s1-decode-encode. β
Instantiating at gives
Corollary 8.1.6.
.
A simple induction shows that this equivalence takes addition to
composition, so that as groups.
Corollary 8.1.7.
, while for .
Proof.
For , we sketched the proof from \autorefcor:omega-s1 above. For , we have . And since is a set, is contractible, so this is trivial. β
Title | 8.1.4 The encode-decode proof |
---|---|
\metatable |