Re: [HoTT] Re: What is UF, what is HoTT and what is a univalent type theory?

[Vladimir Voevodsky <vlad...@ias.edu>]

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

Hi Andre,

1. Are you claiming for an "equivalent" definition "without sets"? Or for the "right"  type-theoretic counterpart of "their" notion(s)?

For the “right” type-theoretic counterpart of “their” notion. To make it equivalent (to show that there exists, in the weak sense, an equivalence) to the one constructed through sets one would have to add axiom of choice in the form that says that for any surjection T -> X where X is an h-set there exists, in the weak sense, a section X -> T. Maybe more axioms will be required but it is possible that this one will suffice.

2. And could you further say something about what you would accept for "equivalent" or for "right”?

For the “right” I will accept a collection of theorems, including construction of examples, that shows that these objects behave in the way expected from (inty,1)-categories.

3. By the way, I suspect the definition you claim for would be formalized, and it would probably be quite involved.

It is very easy to formalize, for example in UniMath, the concept of a quasi-category.

Vladimir.






> On Jun 4, 2016, at 1:05 AM, andré hirschowitz <a...@unice.fr> wrote:
> 
> Hi,
> 
> 2016-06-03 21:29 GMT+02:00 Vladimir Voevodsky <vlad...@ias.edu <mailto: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 #1.2: Type: text/html, Size: 3694 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]