From: Stefan Monnier <monnier@iro.umontreal.ca>
To: "Martín Hötzel Escardó" <escardo.martin@gmail.com>
Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'?
Date: Tue, 05 Nov 2019 19:06:04 -0500 [thread overview]
Message-ID: <jwvbltpan88.fsf-monnier+INBOX@gnu.org> (raw)
In-Reply-To: <cb153658-548a-4fe9-91ed-fc2e3db33723@googlegroups.com> (=?windows-1252?Q?=22Mart=EDn=09H=F6tzel_Escard=F3=22's?= message of "Tue, 5 Nov 2019 15:14:07 -0800 (PST)")
> members of this list. The constructivity of univalence was an open problem
> for a number of year, and I would say that, even if it is solved via the
> cubical model, it is far from being fully understood.
In my case, I still find it odd in a situation such as:
data Foo : Set -> Set where
bar : Foo UnaryNat
since transport supposedly allows us to take a proof of equivalence
between UnaryNat and BinaryNat and turn a `bar` into something of type
`Foo BinaryNat` although I can't see any way to directly construct an
object of this type.
Stefan
next prev parent reply other threads:[~2019-11-06 0:06 UTC|newest]
Thread overview: 32+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-10-27 14:41 Nicolas Alexander Schmidt
2019-10-27 17:22 ` Bas Spitters
2019-11-03 11:38 ` Bas Spitters
2019-11-03 11:52 ` David Roberts
2019-11-03 19:13 ` Michael Shulman
2019-11-03 19:45 ` Valery Isaev
2019-11-03 22:23 ` Martín Hötzel Escardó
2019-11-04 23:20 ` Nicolas Alexander Schmidt
2019-11-24 18:11 ` Kevin Buzzard
2019-11-26 0:25 ` Michael Shulman
2019-11-26 8:08 ` Ulrik Buchholtz
2019-11-26 19:14 ` Martín Hötzel Escardó
2019-11-26 19:53 ` Kevin Buzzard
2019-11-26 20:40 ` Martín Hötzel Escardó
2019-11-26 22:18 ` Michael Shulman
2019-11-27 0:16 ` Joyal, André
2019-11-27 2:28 ` Stefan Monnier
2019-11-27 1:41 ` Daniel R. Grayson
2019-11-27 8:22 ` N. Raghavendra
2019-11-27 10:12 ` Thorsten Altenkirch
2019-11-27 16:37 ` Michael Shulman
2019-11-27 20:21 ` Nicolas Alexander Schmidt
2019-11-04 18:42 ` Kevin Buzzard
2019-11-04 21:10 ` Michael Shulman
2019-11-04 23:26 ` David Roberts
2019-11-05 15:43 ` Daniel R. Grayson
2019-11-05 20:29 ` Yuhao Huang
2019-11-06 23:59 ` Daniel R. Grayson
2019-11-05 23:14 ` Martín Hötzel Escardó
2019-11-06 0:06 ` Stefan Monnier [this message]
2019-11-11 18:26 ` Licata, Dan
2019-11-03 7:29 ` Michael Shulman
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=jwvbltpan88.fsf-monnier+INBOX@gnu.org \
--to=monnier@iro.umontreal.ca \
--cc=HomotopyTypeTheory@googlegroups.com \
--cc=escardo.martin@gmail.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).