Re: [HoTT] Identity versus equality

[Steve Awodey <awo...@cmu.edu>]

To elaborate a bit further in response to some private inquiries: 

Brunerie’s proof that pi_4(S^3) = Z_2 , which is an entirely formal proof within homotopy type theory, has two main parts:

(1) it is shown that there is a natural number n such that pi_4(S^3) = Z_n ,
(2) it is shown that n = 2.

Since the proof of (1) is constructive, it produces an actual term t : Nat .  
In a system of type theory with the canonicity property 
(like intensional MLTT w/o HITs or UA, or some of the more recent cubical type theories),
there is an algorithm which, from any such term t : Nat, will *compute* a numeral t* such that t* == t (definitionally).
This numeral t* denotes a natural number directly.  

Applying the algorithm to (the term representing) “Brunerie’s number” n in (1), 
we should be able to use it to *compute* that n = 2, avoiding the need for the (quite intricate) proof in part (2).  
This is the part that (up to now) has not been possible to do *in practice*, as Andre’ Joyal was pointing out.
Thus we still require the proof in (2) to know that n = 2.

The system of “Book HoTT” allows to formally prove many things that cannot be computed in that system, 
because terms coming from HITs or involving UA need not compute. 
An advantage of cubical systems is that all terms compute — in principle.
But more practical work seems to be required in order to take advantage of this feature in practice.

Regards,

Steve