On 09/02/2019 11:57, Felix Rech wrote:> 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.

Yes, this is what I meant by the sentence that follows the one quoted

above, which I quote below. Also, you don't need to compute by

reducing equalities. In fact, most functional languages (e.g. Haskell)

when compiled *do not* compute by unfolding definitional equalities.

On 08/02/2019 21:19, 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.

> But, again, in principle we can think of a dependent type theory with no

> definitional equalities and instead an existence property like e.g. in

> Lambek and Scott's "introduction to higher-order categorical logic". And

> like was discussed in a relatively recent message by Thierry Coquand in

> this list,)

Martin