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

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

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



On Tuesday, 26 November 2019 19:53:19 UTC, Kevin Buzzard wrote:
>
> What I meant by my earlier post was that the `=` I have run into in Lean's 
> type theory is too weak (canonically isomorphic things can't be proved to 
> be equal) but the one I have run into in HoTT seems too strong 
> (non-canonically isomorphic things are equal).
>

Given a *specific* isomorphism, in HoTT you get  a *specific* element of 
the identity type. 

Let me say this explicitly: equality in HoTT is not truth-valued. It 
collects all the possible ways to identify things. In the case of equality 
of types, the identity type collects the equivalences between them (rather 
than being the truth value expressing whether they are equivalent).

In fact, canonicity is at the heart of the univalence axiom: there is a 
canonical one-to-one correspondence between elements of the equality type 
(i.e. the identity type) and elements of the types of equivalences.

So, the univalence axiom just says that the elements of the good, old 
identity type can be understood to be precisely the equivalences. 

You may wonder what the bonus of this is. This is the content of my last 
two bullet points in my message.

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/77829d67-ed64-43eb-aaf0-d673df419080%40googlegroups.com.

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