Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?

[Ulrik Buchholtz <ulrikbuchholtz@gmail.com>]

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

On Tuesday, November 26, 2019 at 1:25:37 AM UTC+1, Michael Shulman wrote:
>
> On Sun, Nov 24, 2019 at 10:11 AM Kevin Buzzard 
> > However my *current* opinion is that it is not as easy as this, because 
> I believe that the correct "axiom" is that "canonically" isomorphic objects 
> are equal and that the HoTT axiom is too strong. 
>
> This doesn't really make sense to me; I can't figure out what you mean 
> by "too strong".
>

Of course I agree with Mike that univalence is not “too strong”: it merely 
implements the mathematically right notion of identity for types and other 
structures built from types, such as rings, etc.

But if I may venture a guess, I'd say that Kevin wants a “canonical 
reflection rule”: canonical identifications should correspond to judgmental 
equalities. We've had some discussions before about the underlying meaning 
of judgmental equality (invoking Frege's Sinn/Bedeutung distinction among 
other ideas), but I don't know whether we tried saying 
judgmental/definitional equality should include canonical equality, 
whatever that is.

This might be really useful, but I think we're still some ways off before 
we can implement this idea. The first question is whether “all diagrams of 
canonical identifications commute”. (Besides the obvious question of 
defining canonical identifications in the first place :-)

But the adventurous can start by playing around by adding canonical 
identities as rewriting rules in Agda: see Jesper Cockx' recent blog post: 
https://jesper.sikanda.be/posts/hack-your-type-theory.html

Ulrik

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/2f61877b-b4ef-405a-99cc-85da227c70bc%40googlegroups.com.

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