Explicit different proofs of the same identity type in MLTT This question is similar to (but more specific than) this one: When are two proofs of the same theorem really different proofs
I do not know very much about homotopy type theory, but I am trying to understand how essentially different proofs of the same identity claim may naturally appear in Martin-Löf's intentional intuitionistic type theory.
So, I am looking for an (explicit, as simple as possible) example of a type $A$ with terms $a,b: A$ and identity proofs $p,q: \mathrm{Id}_A(a,b)$ such that the type $\mathrm{Id}_{\mathrm{Id}_A(a,b)}(p,q)$ is empty. (I am not sure I have by this correctly formulated my original intention. Homotopically, I want two non-equivalent paths, but I want it in type theory form.)
 A: Let $A = \mathcal U$, $a = b = \mathsf{Bool}$. There are two equivalences from $\mathsf{Bool}$ to itself. One is the reflexive equivalence, and transporting by it is the identity. The other swaps $\mathsf{true}$ and $\mathsf{false}$ when you transport by it. Here is a proof in cubical Agda.
A: Martin-Löf type theory contains no such type because it is consistent with uniqueness of identity proofs which states precisely that what you are looking for is not there.
Martin-Löf type theory is also consistent with the univalence axiom. In the presence of this axiom we may convert the two equivalences $\mathrm{id} : \mathrm{bool} \to \mathrm{bool}$ and $\mathrm{not} : \mathrm{bool} \to \mathrm{bool}$ to terms $\mathrm{ua}(\mathrm{id}), \mathrm{ua}(\mathrm{not}) : \mathrm{Id}_{\mathcal{U}}(\mathrm{bool}, \mathrm{bool})$. Then the identity type
$$\mathrm{Id}_{\mathrm{Id}_{\mathcal{U}}(\mathrm{bool}, \mathrm{bool})}(\mathrm{ua}(\mathrm{id}), \mathrm{ua}(\mathrm{not}) )$$
is empty: given any $p$ of this type, we may obtain from it to a proof of equality of $\mathrm{id}$ and $\mathrm{not}$ and from that we would get an element of $\mathrm{Id}_{\mathrm{bool}}(\mathrm{false}, \mathrm{true})$.
Another possibility is to use the circle $S^1$ in which case there is no path between $\ell$ and $\ell \circ \ell$, where $\ell : \mathrm{Id}_{S^1}(\mathrm{base}, \mathrm{base})$ is the generating loop.
