RE: [HoTT] Identity versus equality

["Joyal, André" <"joyal..."@uqam.ca>]

Thank you Thomas, Jon and Steve for answering my question.

You are very generous to an old man.
Let me pretend that I still have enough time to study the computational aspects of type theory.

By the way, if type theory is not very effective in practice, why do we insist that it should always compute? 
The dream of a formal system in which every proof leads to an actual computation may be far off.
Not that we should abandon it, new discoveries are always possible.  
Is there a version of type theory for proving and verifying, less for computing?
The notations of type theory are very useful in homotopy theory.
But the absence of simplicial types is a serious obstacle to applications.

Best,
André

________________________________________
From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
Sent: Saturday, May 09, 2020 4:28 AM
To: Joyal, André
Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

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