Skip to main content
1 of 3
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

No, sorry, but you haven't got the point of HoTT.

$x \equiv y$ means "$x$ is the same as $y$", so they are terms such that one can be transformed into the other by "rewrite rules" such as expanding or invoking the meaning of a definition, changing the names of bound variables, $\beta$-reduction, etc.

I suspect that you have a pure maths background rather than one in computer science (or category theory). In that case you should think of $Id(x,y)$, not as equality, but as the fundamental group. the space of paths from $x$ to $y$.

When there is a path from $x$ to $y$, it does not mean that $x$ and $y$ are the same.

Moreover, when $p$ and $q$ are paths from $x$ to $y$, $p$ and $q$ don't have to be the same, or even homotopic.

Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58