On Friday, 8 February 2019 22:19:24 UTC+1, Martín Hötzel Escardó wrote:
I do understand that they are used to compute, and so if you are interested in constructive mathematics (like I am) then they are useful.
I agree that the ability to compute canonical forms for terms is essential but one does not need to integrate computation into the type system to do that. At least, one can alway interprete terms of a type theory without an equality judgment in a stronger type theory that has judgmental equalities and do the computations there.