[FOM] An example in homotopy type theory

[Freek Wiedijk]

Hi Kevin,

>One way is to let Z = N + N, the disjoint union of two copies of the
>natural numbers, and define the operations by case analysis in the evident
>way.
>
>Another way is to let Z' = N * N / R for a certain equivalence relation R.
>
>We have thereby specified 4-tuples (Z, plus, negate, zero) and (Z', plus',
>negate', zero') corresponding to the two different definitions.
>
>In set theory there is no reason to expect these 4-tuples to be equal.
>
>In homotopy type theory it is a theorem that they are equal terms of the
>appropriate type.

This is all very nice, but the two _elements_ of those
types that represent the integer 1 are _not_ equal.  In fact
these two versions of the number one have different types,
so their equality cannot even be stated.

(And if one goes to heterogeneous "John Major" equality,
surely they'll be _unequal,_ as these structures have a
non-trivial automorphism?  If these two representations could
be proved equal, for the same reason one would be equal to
the minus one, which is surely something you don't want?)

Between these two number 1 representations one needs to
insert a "transport" to be able to prove them equal.  Which
means that one still needs to _explicitly_ navigate between
different representations of the same mathematical object.
Which means that I don't fully buy the HoTT propaganda
about not having to be confronted with representational
choices when using HoTT.

Freek