Re: [HoTT] Identity versus equality

[Thomas Streicher <stre...@mathematik.tu-darmstadt.de>]

Dear Andr'e,

in most models of HoTT judgemental equality is equality of morphisms
and propositional equality is being homotopic.
But that is very different from its appearance in formal systems
where judgemental equality is much more restricted and just serves the
purpose of computation. There are artificial versions of type theory
with excessively few computation rules (only mere lambda calculus).

I fully understand why you find judgemental equality puzzling: it is
of very subjective nature. Mathematicians are typically interested in
equalities which are not decided by a rewrite system.
Judgemental equality has a very subjective nature because it
identifies a computational fragment of mathematics and there are many
different such. In Book HoTT one is as computational as traditional
intensional TT is and then adds univalence which lacks any
computational meaning. This is at least frivolous from the perspective
of a traditionalist type theorist... But it is ok and was implemented
in the NuPrl system.

Now for people who use type theory as a way of doing homotopy theory
synthetically the computational aspect is absolutely irrelevant a
priori. When one does ordinary math (including homotopy) computability
is a gimmick and no one would insist on everything being computable.

So if one has shown that the homotopy group of some pointed space is
Z_n for some n and one wants to know what n is then in Book HoTT you
have to guess n and then show that n equal your guess. In cubical type
theory in principle the n can be computed but it may take a very long
time (or the normalization proof is faulty :-)).

The main problem is that programs extracted from proofs are typically
not very efficient (well in rare cases they are but you have to be lucky).

Anyway, my brief answer to the question you raise is:
(1) conceptually judgemental equality is absolutely redundant
    and hopelessly subjective
(2) systems with a bare minimum of judgemental equality are not
    suitable for the various proof checkers in use since then every
    computation has to be done by hand.

Thomas