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

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.