From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Sun, 10 May 2020 05:53:21 -0700 (PDT) From: Ulrik Buchholtz To: Homotopy Type Theory Message-Id: In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> References: <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> <20200509082829.GA8417@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca>,<20200509184313.GB28841@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca> Subject: Re: [HoTT] Identity versus equality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1150_1896652001.1589115201911" ------=_Part_1150_1896652001.1589115201911 Content-Type: multipart/alternative; boundary="----=_Part_1151_803177174.1589115201911" ------=_Part_1151_803177174.1589115201911 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Dear Andr=C3=A9, On Saturday, May 9, 2020 at 10:18:11 PM UTC+2, joyal wrote: > But I find it frustrating that I cant do my everyday mathematics with it. > > For example, I cannot say=20 > > (1) Let X:\Delta^{op}---->Type be a simplicial type; > Let me remind everyone that we don't have a proof that it's impossible to= =20 define simplicial types in book HoTT! As long as we haven't settled this=20 question either way, the predicament we're in (and I agree it's a=20 predicament) is more an indictment of type theorists than of type theory.= =20 (And I include myself as a type theorist here.) Anyway, from your phrasing of (1), it looks like you're after a directed=20 type theory. Several groups are working on type theories where your (1) is= =20 valid syntax, but you have to write Space (or Anima or ...) to indicate the= =20 covariant universe of homotopy types and maps, rather than the full=20 universe. (2) Let G be a type equipped with a group structure;=20 > (3) Let BG be the classifying space of a group G; > (4) Let Gr be the category of groups; > Again, let me remind everyone, that groups are precisely one of the few=20 structures we know how to handle (along with grouplike E_n-types, and=20 connective/general spectra): To equip a type G with a group structure is to= =20 give a pointed connected type BG and an equivalence of G with the loop type= =20 of BG. The type of objects of Gr is the universe of pointed, connected=20 types. When you replace groups by monoids, it gets more embarrassing. Earlier (on May 7) you wrote: > At some level, all mathematics is based on some kind of set theory. > Is it not obvious? > We cannot escape Cantor's paradise! > That is exactly the question, isn't it? What HoTT/UF offers us is another axis of foundational variation, besides= =20 the old classical/constructive, impredicative/predicative,=20 infinitist/finitist, namely: everything is based on sets/general homotopy= =20 types are not reducible to sets. I don't know of catchy names for these positions, but I think that working= =20 with HoTT has a tendency of making the latter position more plausible: Why= =20 should there for any type be a set that surjects onto it? A question: Recall that if we assume the axiom of choice (AC) for sets,=20 then there is a surjection from a set onto Set, namely the map that takes a= =20 cardinal (or ordinal) to the set of ordinals below it. Is there (with AC for sets) also a surjection from a set to the type of=20 1-types? To the full universe? The 2-level type theories can be viewed as another way of making a type=20 theory that is faithful to the idea that everything is based on sets. I=20 like to think of the outer layer as an exoskeleton for type theory, giving= =20 it a bit of extra strength while we don't know how to use its own powers=20 fully, or whether indeed it is strong enough to effect constructions like= =20 that of simplicial types. Every type (which for me is a fibrant type, since= =20 that's the mathematically meaningful ones) has a corresponding exotype=20 (indeed an exoset), but there are more exotypes, such as the exonatural=20 numbers, which are sometimes useful. Best wishes, Ulrik ------=_Part_1151_803177174.1589115201911 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Dear Andr=C3=A9,

On Saturday= , May 9, 2020 at 10:18:11 PM UTC+2, joyal wrote:
But I find it frustrating that I cant do my everyda= y mathematics with it.

For example, I cannot =C2=A0say

(1) Let= X:\Delta^{op}---->Type be a simplicial type;

<= br>
Let me remind everyone that we don't have a proof that it= 's impossible to define simplicial types in book HoTT! As long as we ha= ven't settled this question either way, the predicament we're in (a= nd I agree it's a predicament) is more an indictment of type theorists = than of type theory. (And I include myself as a type theorist here.)
Anyway, from your phrasing of (1), it looks like you're after a direct= ed type theory. Several groups are working on type theories where your (1) = is valid syntax, but you have to write Space (or Anima or ...) to indicate = the covariant universe of homotopy types and maps, rather than the full uni= verse.

(2) Let G be a type equipped with a group structure;

=

(3) Let BG be the classifyi= ng space of a group G;
(4) Let Gr be the category of groups;


Again, let me remind everyone, that groups are= precisely one of the few structures we know how to handle (along with grou= plike E_n-types, and connective/general spectra): To equip a type G with a = group structure is to give a pointed connected type BG and an equivalence o= f G with the loop type of BG. The type of objects of Gr is the universe of = pointed, connected types.

When you replace gro= ups by monoids, it gets more embarrassing.

Ear= lier (on May 7) you wrote:
At some level, all mathematics is based on some kind of= set theory.
Is it not obvious?
We cannot escape Cantor's paradis= e!

That is exactly the question, isn't it?

W= hat HoTT/UF offers us is another axis of foundational variation, besides th= e old classical/constructive, impredicative/predicative, infinitist/finitis= t, namely: everything is based on sets/general homotopy types are not reduc= ible to sets.

I don't know of catchy names for these positions, = but I think that working with HoTT has a tendency of making the latter posi= tion more plausible: Why should there for any type be a set that surjects o= nto it?

A question: Recall that if we assume the axiom of choice (AC= ) for sets, then there is a surjection from a set onto Set, namely the map = that takes a cardinal (or ordinal) to the set of ordinals below it.
Is t= here (with AC for sets) also a surjection from a set to the type of 1-types= ? To the full universe?

The 2-level type theories can be viewed as a= nother way of making a type theory that is faithful to the idea that everyt= hing is based on sets. I like to think of the outer layer as an exoskeleton= for type theory, giving it a bit of extra strength while we don't know= how to use its own powers fully, or whether indeed it is strong enough to = effect constructions like that of simplicial types. Every type (which for m= e is a fibrant type, since that's the mathematically meaningful ones) h= as a corresponding exotype (indeed an exoset), but there are more exotypes,= such as the exonatural numbers, which are sometimes useful.
=
Best wishes,
Ulrik

------=_Part_1151_803177174.1589115201911-- ------=_Part_1150_1896652001.1589115201911--