7

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

gmvh
  • 2,758
João Alves Jr.
  • 173

2 Answers2

12

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.

Andrej Bauer
  • 47,834
2

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.

Dan Doel
  • 355
  • 1
    That only gives you equivalences, but you still need to convert them to paths and argue that there is no path between them. Which you cannot in pure Martin-Löf type theory. – Andrej Bauer Jan 30 '21 at 07:55
  • Oh yes. I mistakenly read the question as asking about a type theory where you can do that, not Martin-löf type theory in particular. – Dan Doel Jan 30 '21 at 17:05