If the stronger type theory is not conservative, you generally can't draw mathematical conclusions on the basis of those computations, though.

On Saturday, February 9, 2019 at 6:57:51 AM UTC-5, 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.

--
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.