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

["N. Raghavendra" <raghu@hri.res.in>]

At 2019-11-26T14:18:34-08:00, Michael Shulman wrote:

> Personally, I'm doubtful that one can ascribe any precise meaning to
> "canonical isomorphism", and therefore doubtful that one will be able
> to implement a computer proof assistant that can distinguish a
> "canonical isomorphism" from an arbitrary one.

I have usually assumed that canonical isomorphism meant functorial
isomorphism, i.e., an isomorphism between an appropriate pair of
functors (which are generally left unspecified).  As has been mentioned,
there is no functorial isomorphism from an arbitrary finite-dimensional
vector space V to its dual, whereas the usual isomorphism from V to
double dual is functorial, so the former is non-canonical, and the
latter canonical.

Another explanation I've often come across is that a canonical object is
independent of the choices (if any) that were made in its definition.  I
guess the notion of independence depends on the context.

Raghu.

-- 
N. Raghavendra <raghu@hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

-- 
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/87k17lafu9.fsf%40hri.res.in.