This question is similar to (but more specific than) this one: [When are two proofs of the same theorem really different proofs](https://mathoverflow.net/questions/3776/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.)



Explicit different proofs of the same identity type in MLTT
Martin-Löf type theory contains no such type because it is consistent with [uniqueness of identity proofs](https://ncatlab.org/nlab/show/axiom+UIP) which states precisely that what you are looking for is not there.


Martin-Löf type theory is also consistent with the [univalence axiom](https://ncatlab.org/nlab/show/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](https://arxiv.org/abs/1301.3443) $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.


