From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:90a:d98e:: with SMTP id d14mr19032386pjv.178.1589133870070; Sun, 10 May 2020 11:04:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90b:4d05:: with SMTP id mw5ls14813011pjb.1.canary-gmail; Sun, 10 May 2020 11:04:28 -0700 (PDT) X-Received: by 2002:a17:90b:2385:: with SMTP id mr5mr18823972pjb.172.1589133868447; Sun, 10 May 2020 11:04:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589133868; cv=none; d=google.com; s=arc-20160816; b=ZnoPCghHlbsk7tnb3Mj9N8GzcsGiJwafpsNq1aa76glt/L/xr1hLhyM236qlB1fQrB 4xFFU6NPbNX9j3V0/47sGg+n4rzfd0+ZXadRvDw/3JSsJ4x3mns/w67wzMEhVLRD1Nsh +yHU06n0ZvW6E0erm5o8CIR4BNAHD1R/KMGIbpIYdPYRhRLjCCEDZtA/r3Hbz5N9E86w yb8F/GvEtfb5n0pNxXcFZCIhZywmHQU8tbiwfYtN6nGo5PAUh1Wpuc/4VNHSO+3LaO7h ujTccLbSe3IipHVU5wTZlUY9UBOgqMy9NhtFQfa2NUPyaS0XfiNc2PAOCPIgB7IPo5cT ZxCw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:to :from:ironport-sdr; bh=t1eyMIN3k+llNoz44LpKPbN/iYLAO35BymeLYGFczpU=; b=0dBNlfmnoRwf+XT2PaWp4S1SZ25+WZBoU/3XIwfQRXq1oRIyiOPE5FhZGIKjPZMwSx DxOx8szUBReBB6bvS1TlhV3YUmUNmrWE56Xkqz3mCfFS+QFo7QETVRPzR4V3qqLwyp/a xflFpdk/+x7jOSyXfoF4I2ZneHMte4YjBRsh+RPyna+kwGpQBLzevwpvrHrWi2+XGg/n eN7liM/3TBbqfkfqHrPghkUmwFy+qp5mwq10sIpA6u8XVyzJE3qvsL9/XIjjpZGSBRF9 RS/rN/NSub6A60NB9P/GIj72cUsZJlz95d6INi5UrKw2dahHPDoO95vPeymP1QXSSHRG yiUQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail6.uqam.ca (mail.uqam.ca. [132.208.246.231]) by gmr-mx.google.com with ESMTP id w15si683429pff.1.2020.05.10.11.04.28 for ; Sun, 10 May 2020 11:04:28 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) client-ip=132.208.246.231; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: xSo3+M1j55cBm9SO/mFCuuAMxxNn9g48kM1JCYTjpeqLxt2BIlWBe6wxpamNEbvNkeoQkRUMkl Fq93wj8BenivAU9Z0B4PQPrtRfXzDh0Adr2hmZTt681IQ5IUDl0huHKhZk9+6edVysbrmnhip2 6O6p5qBv1zDfh1RiQPcNkdTpmzgWCYFPqkRFBIudwyzLIzIc4CrgVugfFKgZmlgvA8Tb+/G7Sh DaJlBTrxO7j5VkXM6t/7VTMyh5vU2lAObRzoko04kyNOfXpHW1243+qs9lqTXTwmnVp/ipG9FS fPo= X-IronPort-AV: E=Sophos;i="5.73,376,1583211600"; d="scan'208,217";a="10629578" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.216.70]) by mail6.uqam.ca with ESMTP; 10 May 2020 14:04:27 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Message.gst.uqam.ca ([169.254.1.218]) with mapi id 14.03.0439.000; Sun, 10 May 2020 14:04:26 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Ulrik Buchholtz , Homotopy Type Theory Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOFgABhQICAAHDSgIAAmhfJgAEWX4CAAC1BFIAAfoCA///K+0gALLNAgP//8k6K Date: Sun, 10 May 2020 18:04:25 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F5753@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>, In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: multipart/alternative; boundary="_000_8C57894C7413F04A98DDF5629FEC90B1652F5753Pligstuqamca_" MIME-Version: 1.0 --_000_8C57894C7413F04A98DDF5629FEC90B1652F5753Pligstuqamca_ Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable Dear Ulrik, You wrote: <> I like the idea of calling exo-skeleton the outer layer of a type theory. Category theorists like to distinguish between the internal and the externa= l properties of a category. Logician are distinguishing a formal theory from its meta-theory. A theory and its meta-theory may interact as in G=F6del's incompleteness th= eorem. There are two layers interacting in ML type theory. Is it possible to interpret the outer layer internally, as in G=F6del's inc= ompleteness theorem? You wrote: <> I like the idea of studying groups via the equivalence between groups and p= ointed connected spaces. It is one of the great miracle of homotopy theory (discovered by Kan). It is quite amazing if you think about it: (non-abelian) groups were introd= uced for the purpose of studying symmetries, mostly in Galois theory. The fundamental group of a= space was introduced by Poincar=E9 to study covering spaces in connection with the Klein-Poincar= =E9 uniformisation theorem for Riemann surfaces. The loop space of a pointed sp= ace is a kind of beef-up version of the fundamental group; the fact that it con= tains all the homotopy invariant informations about that space is a great marvel. Topologists are interested in nilpotent groups (ex. the work of Hilton) and the connection with Lie algebras (the Whitehead bracket). By a theorem of Quillen, connected differential graded Lie algebras are rat= ional models of simply connected spaces. Also, in Goodwillie's calculus, the derivative of the identity functor is t= he Lie algebra operad. I am afraid the equivalence between groups and pointed connected spaces will be meaningless (tautological) if the former is defined to be the latte= r. Best, Andr=E9 ________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf of Ulrik Buchholtz [ulrikbu...@gmail.com] Sent: Sunday, May 10, 2020 8:53 AM To: Homotopy Type Theory Subject: Re: [HoTT] Identity versus equality Dear Andr=E9, 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 (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 d= efine simplicial types in book HoTT! As long as we haven't settled this que= stion either way, the predicament we're in (and I agree it's a predicament)= is more an indictment of type theorists than of type theory. (And I includ= e myself as a type theorist here.) Anyway, from your phrasing of (1), it looks like you're after a directed ty= pe theory. Several groups are working on type theories where your (1) is va= lid syntax, but you have to write Space (or Anima or ...) to indicate the c= ovariant universe of homotopy types and maps, rather than the full universe= . (2) Let G be a type equipped with a group structure; (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 str= uctures we know how to handle (along with grouplike E_n-types, and connecti= ve/general spectra): To equip a type G with a group structure is to give a = pointed connected type BG and an equivalence of G with the loop type of BG.= The type of objects of Gr is the universe of pointed, connected 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 t= he old classical/constructive, impredicative/predicative, infinitist/finiti= st, namely: everything is based on sets/general homotopy types are not redu= cible 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 position more plausible: Why = 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, the= n there is a surjection from a set onto Set, namely the map that takes a ca= rdinal (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 1-t= ypes? To the full universe? The 2-level type theories can be viewed as another way of making a type the= ory that is faithful to the idea that everything is based on sets. I like t= o think of the outer layer as an exoskeleton for type theory, giving it a b= it of extra strength while we don't know how to use its own powers fully, o= r whether indeed it is strong enough to effect constructions like that of s= implicial types. Every type (which for me is a fibrant type, since that's t= he mathematically meaningful ones) has a corresponding exotype (indeed an e= xoset), but there are more exotypes, such as the exonatural numbers, which = are sometimes useful. Best wishes, Ulrik -- 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 e= mail to HomotopyT...@googlegroups.com= . To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/e47e6263-d0eb-4882-ab07-e31483095bd4%40googlegroups.com<= https://groups.google.com/d/msgid/HomotopyTypeTheory/e47e6263-d0eb-4882-ab0= 7-e31483095bd4%40googlegroups.com?utm_medium=3Demail&utm_source=3Dfooter>. --_000_8C57894C7413F04A98DDF5629FEC90B1652F5753Pligstuqamca_ Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable
Dear Ulrik,

You wrote:

<<The 2-level type theories can be viewed as another way of maki= ng a type theory that is faithful to the idea that everything is based on s= ets. 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 str= ong enough to effect constructions like that of simplicial types. Every typ= e (which for me is a fibrant type, since that's the mathematically meaningf= ul ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural nu= mbers, which are sometimes useful.>>

I like the idea of calling exo-skeleton the outer layer of a type theo= ry.
Category theorists like to distinguish between the internal and the ex= ternal properties of a category.
Logician are distinguishing a formal theory from its meta-theory.
A theory and its meta-theory may interact as in G=F6del's incompletene= ss theorem.
There are two layers interacting in ML type theory.
Is it possible to interpret the outer layer internally, as in G=F6del'= s incompleteness theorem?


You wrote:

<<Again, let me remind everyone, that groups are precisely one o= f the few structures we know how to handle (along with grouplike 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 of G with the loop type of BG. The type of objects of G= r is the universe of pointed, connected types.>>

I like the idea of studying groups via the equivalence between groups = and pointed connected spaces.
It is one of the great miracle of homotopy theory (discovered by Kan).=
It is quite amazing if you think about it: (non-abelian) groups were i= ntroduced for the purpose
of studying symmetries, mostly in Galois theory. The fundamental group= of a space was introduced
by Poincar=E9 to study covering spaces in connection with the Klein-Po= incar=E9
uniformisation theorem for Riemann surfaces. The loop space of a point= ed space
is a kind of beef-up version of the fundamental group; the fact that i= t contains
all the homotopy invariant informations about that space is a great ma= rvel.
Topologists are interested in nilpotent groups (ex. the work of Hilton= ) and
the connection with Lie algebras (the Whitehead bracket).
By a theorem of Quillen, connected differential graded Lie algebras ar= e rational models of simply connected spaces.
Also, in Goodwillie's calculus, the derivative of the identity functor= is the Lie algebra operad.

I am afraid the equivalence between groups and pointed connected space= s
will be meaningless (tautological) if the former is defined to be the = latter.

Best,
Andr=E9


From: homotopyt...@googlegroups.com [homo= topyt...@googlegroups.com] on behalf of Ulrik Buchholtz [ulrikbu...@gmail.c= om]
Sent: Sunday, May 10, 2020 8:53 AM
To: Homotopy Type Theory
Subject: Re: [HoTT] Identity versus equality

Dear Andr=E9,

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

(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 define simplicial types in book HoTT! As long as we haven't settled thi= s question either way, the predicament we're in (and I agree it's a predica= ment) is more an indictment of type theorists than of type theory. (And I include myself as a type theorist he= re.)

Anyway, from your phrasing of (1), it looks like you're after a directed ty= pe theory. Several groups are working on type theories where your (1) is va= lid syntax, but you have to write Space (or Anima or ...) to indicate the c= ovariant universe of homotopy types and maps, rather than the full universe.

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

(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 fe= w structures we know how to handle (along with grouplike E_n-types, and con= nective/general spectra): To equip a type G with a group structure is to gi= ve a pointed connected type BG and an equivalence of G with the loop type of BG. The type of objects of Gr is= the universe of pointed, connected 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 t= he old classical/constructive, impredicative/predicative, infinitist/finiti= st, namely: everything is based on sets/general homotopy types are not redu= cible 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 position more plausible: Why = 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, the= n there is a surjection from a set onto Set, namely the map that takes a ca= rdinal (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 1-t= ypes? To the full universe?

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

Best wishes,
Ulrik

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e47e6263-d0eb-4882-ab0= 7-e31483095bd4%40googlegroups.com.
--_000_8C57894C7413F04A98DDF5629FEC90B1652F5753Pligstuqamca_--