Homotopy type theory

In the homotopy interpretation, what is the identity type $a =_A b$?

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)?

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 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?

Which Lean statement expresses that univalence fails in Lean, for the type Bool?

In the encode–decode proof that $(\mathsf{base} = \mathsf{base}) \simeq \Z$, where is the univalence axiom used?

Which principles are consistent with (or follow from) univalence? (Choose all that apply.)

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.)

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))$.)