From: "andré hirschowitz" <"a..."@unice.fr>
To: Vladimir Voevodsky <vlad...@ias.edu>
Cc: Andrew Polonsky <andrew....@gmail.com>,
Martin Escardo <m.es...@cs.bham.ac.uk>,
Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?
Date: Sat, 4 Jun 2016 00:05:09 +0200 [thread overview]
Message-ID: <CAHPPr6zxGA=i2HBuhyCjs1ZmetT2funLRHpsCh346Mtnk0XTyw@mail.gmail.com> (raw)
In-Reply-To: <A9CC94F9-0983-4087-9DF6-DC18A8891FB7@ias.edu>
[-- Attachment #1: Type: text/plain, Size: 1010 bytes --]
Hi,
2016-06-03 21:29 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu>:
> They don’t take us seriously so far because we can not define
> (infty,1)-categories. As soon as we find a language that can be used to
> define them and work with them directly without going through sets they
> will all start to turn their heads in our direction.
I can believe it is reachable to define "their" notion(s) of infty-cats
within UF "through sets". Are you claiming for an "equivalent" definition
"without sets"? Or for the "right" type-theoretic counterpart of "their"
notion(s)?
And could you further say something about what you would accept for
"equivalent" or for "right"?
Anyway, why would "they" turn their heads? They have no need, do they?
By the way, I suspect the definition you claim for would be formalized, and
it would probably be quite involved. Except if you require (and prove) a
characteristic property, it would be a hard (human) task to check that it
is reasonable.
ah
[-- Attachment #2: Type: text/html, Size: 1481 bytes --]
next prev parent reply other threads:[~2016-06-03 22:05 UTC|newest]
Thread overview: 23+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-06-02 21:29 Martin Escardo
2016-06-03 11:53 ` Andrew Polonsky
2016-06-03 12:49 ` [HoTT] " Vladimir Voevodsky
2016-06-03 14:12 ` Andrew Polonsky
2016-06-03 19:29 ` Vladimir Voevodsky
2016-06-03 22:05 ` andré hirschowitz [this message]
2016-06-04 8:38 ` Vladimir Voevodsky
2016-06-04 9:56 ` andré hirschowitz
2016-06-06 8:10 ` [HoTT] " Vladimir Voevodsky
2016-06-04 6:11 ` [HoTT] " Urs Schreiber
2016-06-06 7:14 ` Vladimir Voevodsky
2016-06-06 7:32 ` David Roberts
2016-06-06 10:56 ` [HoTT] " Vladimir Voevodsky
2016-06-06 11:40 ` David Roberts
2016-06-03 20:17 ` [HoTT] " Martin Escardo
[not found] ` <CAOvivQxw34SKUatt4aW-u4bLjgSq=K58i8E6+sBBAh6OzvzANg@mail.gmail.com>
2016-06-05 20:40 ` [HoTT] " Martin Escardo
[not found] ` <CAOvivQx0BHg2KCbWzav+0aW9knbEq521gxXBA3pDrFDxt8J0qA@mail.gmail.com>
2016-06-08 10:14 ` Martín Hötzel Escardó
2016-06-14 21:46 ` Michael Shulman
2016-06-14 22:15 ` Martin Escardo
2016-06-14 22:30 ` Michael Shulman
2016-06-14 23:33 ` Martin Escardo
2016-06-15 3:04 ` Michael Shulman
2016-06-08 14:37 ` Fwd: " 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='CAHPPr6zxGA=i2HBuhyCjs1ZmetT2funLRHpsCh346Mtnk0XTyw@mail.gmail.com' \
--to="a..."@unice.fr \
--cc="HomotopyT..."@googlegroups.com \
--cc="andrew...."@gmail.com \
--cc="m.es..."@cs.bham.ac.uk \
--cc="vlad..."@ias.edu \
/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).