[HoTT] Re: Why do we need judgmental equality?

["Martín Hötzel Escardó" <escardo.martin@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 1740 bytes --]

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


-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 2261 bytes --]