The Lumenary · Research pathways

Homotopy type theory

Name: ______________________

Date: ______________________

You will learn to

Explain identity types and their reading as path spaces, and derive transport, the action of functions on paths and the groupoid laws by path induction
Define equivalences of types, state the univalence axiom, and prove that it is incompatible with uniqueness of identity proofs for the universe
Define the circle as a higher inductive type and outline the encode–decode proof that its loop space is equivalent to $\Z$
Describe the models of homotopy type theory and separate established results from open questions
Use Lean to see precisely where an ordinary proof assistant departs from homotopy type theory

1.
In the homotopy interpretation, what is the identity type $a =_A b$ ?
- A.The space of paths in $A$ from $a$ to $b$
- B.A truth value: true if $a$ and $b$ are equal, false otherwise
- C.The set $\{a, b\}$
- D.The set of isomorphisms between $a$ and $b$ , by definition
2.
Assume univalence. How many elements does the identity type $\mathsf{Fin}(3) = \mathsf{Fin}(3)$ have (it is a set, so count elements up to paths)?
3.
Let $P(x) :\equiv (a = x)$ for a fixed $a : A$ . For $p : b = c$ and $q : a = b$ , what is $\mathsf{tr}^P(p, q) : a = c$ ?
- A. $q \cdot p$
- B. $p \cdot q$
- C. $q$ , since transport is just substitution
- D. $p^{-1} \cdot q$
4.
A student argues: 'Let $p : a = a$ . By path induction we may assume $p$ is $\mathsf{refl}_a$ , so every loop equals $\mathsf{refl}_a$ .' What is wrong?
- A.Path induction applies only to families over paths with a free endpoint, $\Pi_{x}\Pi_{p : a = x} C(x, p)$ ; here both endpoints are fixed at $a$
- B.Nothing: this is a valid proof of uniqueness of identity proofs
- C.The argument forgot to use symmetry of equality
- D.Path induction requires function extensionality
5.
Which Lean statement expresses that univalence fails in Lean, for the type Bool?
- A.¬ Function.Surjective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool))
- B.¬ Nonempty (Paths Bool Bool)
- C.Function.Injective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool))
- D.¬ (Bool ≃ Bool)
6.
In the encode–decode proof that $(\mathsf{base} = \mathsf{base}) \simeq \Z$ , where is the univalence axiom used?
- A.To define the universal cover $\mathsf{code}$ , sending $\mathsf{loop}$ to the path $\mathsf{ua}(\mathsf{succ}) : \Z = \Z$ in the universe
- B.To prove $\mathsf{decode}(\mathsf{encode}(p)) = p$
- C.To prove $\mathsf{succ}^n(0) = n$ by induction on $n$
- D.Nowhere; the higher inductive circle suffices
7.
Which principles are consistent with (or follow from) univalence? (Choose all that apply.)
- A.Excluded middle for propositions
- B.The axiom of choice for sets
- C.Function extensionality
- D.Uniqueness of identity proofs for all types, including the universe
- E.Excluded middle for all types, $\Pi_{A : \mathcal{U}} (A + \neg A)$
8.
In homotopy type theory with univalence and the higher inductive circle, which of these types are sets (all of their identity types are propositions)? (Choose all that apply.)
- A. $\mathbb{N}$
- B. $\mathsf{Bool}$
- C. $\mathsf{base} = \mathsf{base}$ in $S^1$
- D. $S^1$
- E.The universe $\mathcal{U}$
9.
Loops in the circle built from $\mathsf{loop}$ ( $+1$ ) and $\mathsf{loop}^{-1}$ ( $-1$ ) are words, e.g. (1, 1, -1). The groupoid laws let us cancel an adjacent pair 1, -1 or -1, 1. Write reduce_word(word) returning the fully reduced word as a tuple. (The tests check that your reduced word is always $\mathsf{decode}(\mathsf{encode}(w))$ .)
Computational — Practice

Answer key — Homotopy type theory

1.
$a =_A b$ is read as the space of paths from $a$ to $b$ . Reflexivity is the constant path, symmetry is reversal, transitivity is concatenation, and paths between paths are homotopies.
2.
By univalence the paths are the self-equivalences of $\mathsf{Fin}(3)$ , i.e. the $3! = 6$ permutations. So the universe 'remembers' the symmetric group $S_3$ as the loop space of the type of 3-element types, which is $BS_3$ .
3.
$\mathsf{tr}^P(p, q) = q \cdot p$ . By path induction on $p$ it suffices to treat $p \equiv \mathsf{refl}_b$ , where transport is the identity and $q \cdot \mathsf{refl} \equiv q$ . This is the type-theoretic form of 'lifting a path to the path fibration'.
4.
Path induction proves statements $\Pi_{x : A}\Pi_{p : a = x} C(x, p)$ in which the endpoint $x$ varies. To apply it to loops one would need a family $C(x, p)$ that only makes sense when $x \equiv a$ , which is not available. The conclusion is axiom K (UIP), independent of Martin-Löf type theory (Hofmann–Streicher) and refuted by univalence.
5.
¬ Function.Surjective (idtoeqv : Paths Bool Bool → (Bool ≃ Bool)). Lean proves that Paths Bool Bool has at most one element (paths_subsingleton, using proof irrelevance of Eq), while Bool ≃ Bool has two different elements, so idtoeqv cannot hit both.
6.
Univalence is used to build $\mathsf{code} : S^1 \to \mathcal{U}$ , with $\mathsf{ap}_{\mathsf{code}}(\mathsf{loop}) = \mathsf{ua}(\mathsf{succ})$ , and through its computation rule $\mathsf{tr}^{\mathsf{code}}(\mathsf{loop}, -) = \mathsf{succ}$ . The other steps use path induction, circle induction and arithmetic.
7.
Excluded middle for propositions, choice for sets, and function extensionality are all compatible with univalence (the last is a consequence). UIP for the universe and excluded middle for all types contradict it.
8.
$\mathbb{N}$ , $\mathsf{Bool}$ and $\Omega(S^1) \simeq \Z$ are sets. $S^1$ is a 1-type but not a set, and the univalent universe is not a set (it is not even a 1-type once it contains types with non-trivial path spaces).
9.
```
def reduce_word(word):
    stack = []
    for step in word:
        if stack and stack[-1] == -step:
            stack.pop()
        else:
            stack.append(step)
    return tuple(stack)
```
A reduced word in one generator is $\mathsf{loop}^n$ for a unique $n \in \Z$ , namely its winding number. That reduced words are classified by $\Z$ is the combinatorial shadow of $(\mathsf{base} = \mathsf{base}) \simeq \Z$ ; the type-theoretic proof (encode–decode) shows it for all loops, not only those built from words.