From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a63:b604:: with SMTP id j4mr13367304pgf.124.1588895826700; Thu, 07 May 2020 16:57:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:55c3:: with SMTP id j186ls85610pfb.6.gmail; Thu, 07 May 2020 16:57:04 -0700 (PDT) X-Received: by 2002:a63:220a:: with SMTP id i10mr14385319pgi.364.1588895824439; Thu, 07 May 2020 16:57:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588895824; cv=none; d=google.com; s=arc-20160816; b=hzF/ZCqWLuVIXzj6GN3Nuc51rMUoZOaAEzDQS6Gc+OxjpIxDgEyolTxFoqMHEUJYhP +pVjRTPBG6jjXf0i4cP49H7YUVNlLZvyfy/VGwLDUgiAOq6hrQ9Dx3EOnmjX4N7xLdSG ArOr0eiPZzV3OgR5UsTbPVac1GbAeloCMBwXkdVNHvlq3R54zNPdKru/HAtLkQVKoQK/ dynmc2pgivu3Qd49lH2Qy0R/6JijOPhNoXJVAtTqNYiAYRMd5cozx1klE+gJtpdm/Cne dqZp2GsDMgV+FleVIVxRGZKvPReH9SD26RSWaxcbGv25Wwzjcj5OZMEFOrs7NgexNLmD Z0xg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=W9jgFEM0H8uSa5r2PRP25uzVmqoYdkLH1nhTBTjwj78=; b=K420j/UWN0i8/ue9hiUnOej6gmyhTsGPmWaT7HUQ7ALylV9vzT3t57dMF45NjjI9iM tqOjZxitspEL8jwmRdSO5nIfWcsl0kQSBXJE5mtkAXbmubjWV6LMEx/ShqJRkrzY1U69 OVkHmfYeKbjqHQ/01fmQ9RJoOsosoK8DZkC9m+CvpYOIN0KtTRaN1nxenJiFgzEGXx5d sdyX4ZMzHcueDS4diBJFwd762VLQivZJGpCu0uTuFsk8O2HpVy2Y1z5qXeZ8cv3nm1IZ rPpzgeSI5TLpFMRdn1yMh42AkAK+ppvxc3Fd4Z9P1e881LDUwl8gyXGS+Zo+VFG7atuB 4UuA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=YhldvYq2; spf=pass (google.com: domain of drober...@gmail.com designates 2607:f8b0:4864:20::b2c as permitted sender) smtp.mailfrom=drober...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yb1-xb2c.google.com (mail-yb1-xb2c.google.com. [2607:f8b0:4864:20::b2c]) by gmr-mx.google.com with ESMTPS id k13si214004pfd.0.2020.05.07.16.57.04 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 07 May 2020 16:57:04 -0700 (PDT) Received-SPF: pass (google.com: domain of drober...@gmail.com designates 2607:f8b0:4864:20::b2c as permitted sender) client-ip=2607:f8b0:4864:20::b2c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=YhldvYq2; spf=pass (google.com: domain of drober...@gmail.com designates 2607:f8b0:4864:20::b2c as permitted sender) smtp.mailfrom=drober...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-yb1-xb2c.google.com with SMTP id w19so431983ybs.5 for ; Thu, 07 May 2020 16:57:04 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=W9jgFEM0H8uSa5r2PRP25uzVmqoYdkLH1nhTBTjwj78=; b=YhldvYq2ToYDCbzvKtvwmTtc0mhrBv4CPOV6wEasm036A3gS8x9gpZOfuYQO/tu7YI hoalZMqfBhNZxhlze3DHaWSpqpop5yu0XGFY29zxgVOfSqOplLqPw+93lQuOXv69BF/z E+TxJTezUQewH/eZPxNe/eQMwIjMO6VRMrFvafqgF8HgvwDENewbgm12/rhHRt1B+JSX 0V8qCpZBda8EzBdUkbMmL4dN3SGxroFDrjQ8mUmsej6oDSJ3p2yVUgsPhI70x7KMyd8l AsOGFg82042tWexZLc/dQPPrsGrBKMBBwe+blO5bJEPeP7VxjwpbjRWdGgTz4H0rF6KG p+7w== X-Gm-Message-State: AGi0PuZpz9Xz9CxzCQX22LzPzqMpsmGWr6pX2zWxoVmM6uVWjIB6kRAi HObkTcveMck5e3oofu8cKauphwjT26ryBYDQplk= X-Received: by 2002:a25:7901:: with SMTP id u1mr128878ybc.301.1588895823527; Thu, 07 May 2020 16:57:03 -0700 (PDT) MIME-Version: 1.0 References: <8C57894C7413F04A98DDF5629FEC90B1652F515E@Pli.gst.uqam.ca> <05375057-883F-4487-8919-2579F5771AFC@cmu.edu> <952EF822-FD92-404C-A279-89502238BCDC@nottingham.ac.uk> <8C57894C7413F04A98DDF5629FEC90B1652F526C@Pli.gst.uqam.ca> <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> From: David Roberts Date: Fri, 8 May 2020 09:26:51 +0930 Message-ID: Subject: Re: [HoTT] Identity versus equality To: =?UTF-8?Q?Joyal=2C_Andr=C3=A9?= Cc: Thomas Streicher , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000258f2105a517a3ad" --000000000000258f2105a517a3ad Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear Andr=C3=A9, I merely meant that the definition of category only requires first-order logic as in (Eilenberg=E2=80=93Mac Lane 1945), or at best a low-level depen= dent type theory ( https://ncatlab.org/nlab/show/type-theoretic+definition+of+category). See also: https://ncatlab.org/nlab/show/fully+formal+ETCS#the_theory_etcs Regards, David David Roberts Webpage: https://ncatlab.org/nlab/show/David+Roberts Blog: https://thehighergeometer.wordpress.com On Fri, 8 May 2020 at 09:13, Joyal, Andr=C3=A9 wrote: > Dear David, > > This is getting controversial! > > As you know, there are many notions of category. > Let me say that an ordinary category with a "set" of objects > and a "set" of arrows lives on the ground floor. > There is then a notion of category internal to a category; > let me say that such categories live on the first floor. > By induction, there a notion of category for every floor. > Of course, one can introduce an abstract notion of category > without specifying the level. For example, one > could consider a type theory classifying the notion of (\infty,1)-categor= y. > But the type theory must be described by specifying a formal system. > The "predicates" in the formal system form a set, actually a countable se= t. > The syntactic category of any formal system lives on the ground floor. > Hence the generic category lives on the first floor. > > I would love to remove set theory (in a naive sense) > from the foundation of mathematics if that were possible. > Is that really desirable? > Maybe we should accept the situation > and use it to improve mathematics. > > Best, > Andr=C3=A9 > > ------------------------------ > *From:* David Roberts [drober...@gmail.com] > *Sent:* Thursday, May 07, 2020 5:41 PM > *To:* Joyal, Andr=C3=A9 > *Cc:* Thomas Streicher; Thorsten Altenkirch; Michael Shulman; Steve > Awodey; homotopyt...@googlegroups.com > *Subject:* Re: [HoTT] Identity versus equality > > >every category has a set of objects and a set of arrows. > > I'm sorry, but where does it say that? The whole point of ETCS was to > avoid an ambient set theory, no? Not to mention the original 'General > theory of natural equivalences' avoided defining categories using sets. > > Humbly, > David > > > David Roberts > Webpage: https://ncatlab.org/nlab/show/David+Roberts > Blog: https://thehighergeometer.wordpress.com > > > On Fri, 8 May 2020 at 01:43, Joyal, Andr=C3=A9 wrote: > >> Thank you all for your comments. >> >> Thomas wrote: >> >> <> or whatever). There judgemental equality gets interpreted as equality >> of morphism and propositional equality gets interpreted as being >> homotopic. >> Since the outer level of 2-level type theory is extensional there is >> no judgemental equality (as in extensional TT).>> >> >> I agree, there is some some kind of (weak) Quillen model structure >> associated to every model of type theory. >> All of higher category theory seems to be based on good old set theory. >> For example, a quasi-category is a simplicial set. >> The category of sets could be replaced by a topos, but a topos is a >> category >> and every category has a set of objects and a set of arrows. >> At some level, all mathematics is based on some kind of set theory. >> Is it not obvious? >> We cannot escape Kantor's paradise! >> Of course, we could possibly work exclusively with countable sets. >> The set of natural numbers is the socle on which all mathematics is >> constructed. >> Still, I would not want to refer constantly to recursion when I do >> mathematics. >> There is a hierarchy of mathematical languages, and Peano's arithmetic i= s >> at the ground level. >> Modern mathematics is mostly concerned with higher levels of abstraction= . >> Its usefulness is without questions, athough its foundation can be >> problematic. >> Type theory is the only theory I know which includes two levels in its >> formalism. >> Judgemental equality is at the lower level. It is not inferior, it is >> more fundamental. >> >> Best, >> Andr=C3=A9 >> >> >> >> ________________________________________ >> From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] >> Sent: Thursday, May 07, 2020 6:09 AM >> To: Thorsten Altenkirch >> Cc: Joyal, Andr=C3=A9; Michael Shulman; Steve Awodey; >> homotopyt...@googlegroups.com >> Subject: Re: [HoTT] Identity versus equality >> >> In my eyes the reason for the confusion (or rather different views) >> arises from the different situation we have in syntax and in semantics. >> >> In syntax the "real thing" is propositional equality and judgemental >> equality is just an auxiliary notion. In mathematics it's the well >> known difference between equality requiring proof (e.g. by induction) an= d >> checking equality by mere symbolic computation. The latter is just a >> technical device and not something conceptually basic. >> >> The situation is very different in models (be they simplicial, cubical >> or whatever). There judgemental equality gets interpreted as equality >> of morphism and propositional equality gets interpreted as being >> homotopic. >> Since the outer level of 2-level type theory is extensional there is >> no judgemental equality (as in extensional TT). >> >> This latter view is the view of people working in higher dimensional >> category theory as e.g. you, Andr'e when you are not posting on the >> list but write your beautiful texts on quasicats, Lurie or Cisinski >> (and quite a few others). In these works people are not afraid of >> refering to equality of objects, e.g. when defining the infinite >> dimensional analogue of Grothendieck fibrations. And this for very >> good reasons since there are important parts of category theory where >> equality of objects does play a role (typically Grothendieck fibrations)= . >> >> Fibered cats also often don't allow one to speak about equality of >> objects in the base but it is there. This is very clearly expressed so >> in the last paragraph of B'enabou's JSL article of fibered cats from 198= 5. >> I think this applies equally well to infinity cats mutatis mutandis. >> >> This phenomenon is not new. Consider good old topos theory. There are >> things expressible in the internal logic of a topos and there are >> things which can't be expressed in it as e.g. well pointedness or >> every epi splits. The first holds vacuously when (misleadingly) >> expressed in the internal language of a topos and the second amounts >> to so called internal AC (which amounts to epis being preserved by >> arbitrary exponentiation). This doesn't mean at all that internal >> language is >> a bad thing. It just means that that it has its limitations... >> >> Analogously, so in infinity category theory. Let us assume for a >> moment that HoTT were the internal language of infinity toposes (which >> I consider as problematic). There are many things which can be >> expressed in the internal language but not everything as e.g. being a >> Grothendieck fibration or being a mono... >> >> I mean these are facts which one has to accept. One might find them >> deplorable or a good thing but one has to accept them... >> >> One of the reasons why I do respect Voevodsky a lot is that although >> he developed HoTT (or better the "univalent view") he also suggested >> 2-level type theory when he saw its limitations. >> >> I hope you apologize but I can't supress the following analogy coming >> to my mind. After revolution in Russia and the civil war when economy >> lay down the Bolsheviks reintroduced a bit of market economy under the >> name NEP (at least that's the acronym in German) to help up the economy. >> (To finish the story NEP was abandoned by Stalin which lead to well know= n >> catastrophies like the forced collectivization...) >> >> Sorry for that but one has to be careful when changing things and >> think twice before throwing away old things...some of them might be >> still useful and even indispensible! >> >> Thomas >> >> >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyT...@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98D= DF5629FEC90B1652F5334%40Pli.gst.uqam.ca >> . >> > --000000000000258f2105a517a3ad Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Andr=C3=A9,

I merely meant that th= e definition of category only requires first-order logic as in (Eilenberg= =E2=80=93Mac Lane 1945), or at best a low-level dependent type theory (https://ncatlab.org/nlab/show/type-theoretic+definition+of+category). = See also:=C2=A0https://ncatlab.org/nlab/show/fully+formal+ETCS#the_theory_= etcs

Regards,
David

On Fri, 8 May 2020 at 09:13, Joyal, Andr=C3=A9 <joyal...@uqam.ca> wrote:
Dear David,

This is getting controversial!

As you know, there are many notions of category.
Let me say that an ordinary category with a "set" of objects=
and a "set" of arrows lives on the ground floor.
There is then a notion of category internal to a category;
let me say that such categories live on the first floor.
By induction, there a notion of category for every floor.
Of course, one can introduce an abstract notion of category
without specifying the level. For example, one
could consider a type theory classifying the notion of (\infty,1)-cate= gory.
But the type theory must be described by specifying a formal system.
The "predicates" in the formal system form a set, actually a= countable set.
The syntactic category of any formal system lives on the ground floor.=
Hence the generic category lives on the first floor.

I would love to remove set theory (in a naive sense)=C2=A0
from the foundation of mathematics if that were possible.
Is that really desirable?
Maybe we should accept the situation
and use it to improve mathematics.

Best,
Andr=C3=A9

From: David Robe= rts [drober...@gma= il.com]
Sent: Thursday, May 07, 2020 5:41 PM
To: Joyal, Andr=C3=A9
Cc: Thomas Streicher; Thorsten Altenkirch; Michael Shulman; Steve Aw= odey; ho= motopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

>every category has a set of objects and a set of arrow= s.

I'm sorry,=C2=A0but where does it say that? The whole point of ETC= S was to avoid an ambient set theory, no? Not to mention the original '= General theory of natural equivalences' avoided defining categories usi= ng sets.

Humbly,
David


On Fri, 8 May 2020 at 01:43, Joyal, A= ndr=C3=A9 <joyal...@uqam.ca> wrote:
Thank you all for your comments.

Thomas wrote:

<<The situation is very different in models (be they simplicial, cubi= cal
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.=
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).>>

I agree, there is some some kind of (weak) Quillen model structure associat= ed to every model of type theory.
All of higher category theory seems to be based on good old set theory.
For example, a quasi-category is a simplicial set.
The category of sets could be replaced by a topos, but a topos is a categor= y
and every category has a set of objects and a set of arrows.
At some level, all mathematics is based on some kind of set theory.
Is it not obvious?
We cannot escape Kantor's paradise!
Of course, we could possibly work exclusively with countable sets.
The set of natural numbers is the socle on which all mathematics is constru= cted.
Still, I would not want to refer constantly to recursion when I do mathemat= ics.
There is a hierarchy of mathematical languages, and Peano's arithmetic = is at the ground level.
Modern mathematics is mostly concerned with higher levels of abstraction. Its usefulness is without questions, athough its foundation can be problema= tic.
Type theory is the only theory I know which includes two levels in its form= alism.
Judgemental equality is at the lower level. It is not inferior, it is more = fundamental.

Best,
Andr=C3=A9



________________________________________
From: Thomas Streicher [stre...@mathematik.tu-darm= stadt.de]
Sent: Thursday, May 07, 2020 6:09 AM
To: Thorsten Altenkirch
Cc: Joyal, Andr=C3=A9; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

In my eyes the reason for the confusion (or rather different views)
arises from the different situation we have in syntax and in semantics.

In syntax the "real thing" is propositional equality and judgemen= tal
equality is just an auxiliary notion. In mathematics it's the well
known difference between equality requiring proof (e.g. by induction) and checking equality by mere symbolic computation. The latter is just a
technical device and not something conceptually basic.

The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.=
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).

This latter view is the view of people working in higher dimensional
category theory as e.g. you, Andr'e when you are not posting on the
list but write your beautiful texts on quasicats, Lurie or Cisinski
(and quite a few others). In these works people are not afraid of
refering to equality of objects, e.g. when defining the infinite
dimensional analogue of Grothendieck fibrations. And this for very
good reasons since there are important parts of category theory where
equality of objects does play a role (typically Grothendieck fibrations).
Fibered cats also often don't allow one to speak about equality of
objects in the base but it is there. This is very clearly expressed so
in the last paragraph of B'enabou's JSL article of fibered cats fro= m 1985.
I think this applies equally well to infinity cats mutatis mutandis.

This phenomenon is not new. Consider good old topos theory. There are
things expressible in the internal logic of a topos and there are
things which can't be expressed in it as e.g. well pointedness or
every epi splits. The first holds vacuously when (misleadingly)
expressed in the internal language of a topos and the second amounts
to so called internal AC (which amounts to epis being preserved by
arbitrary exponentiation). This doesn't mean at all that internal langu= age is
a bad thing. It just means that that it has its limitations...

Analogously, so in infinity category theory. Let us assume for a
moment that HoTT were the internal language of infinity toposes (which
I consider as problematic). There are many things which can be
expressed in the internal language but not everything as e.g. being a
Grothendieck fibration or being a mono...

I mean these are facts which one has to accept. One might find them
deplorable or a good thing but one has to accept them...

One of the reasons why I do respect Voevodsky a lot is that although
he developed HoTT (or better the "univalent view") he also sugges= ted
2-level type theory when he saw its limitations.

I hope you apologize but I can't supress the following analogy coming to my mind. After revolution in Russia and the civil war when economy
lay down the Bolsheviks reintroduced a bit of market economy under the
name NEP (at least that's the acronym in German) to help up the economy= .
(To finish the story NEP was abandoned by Stalin which lead to well known catastrophies like the forced collectivization...)

Sorry for that but one has to be careful when changing things and
think twice before throwing away old things...some of them might be
still useful and even indispensible!

Thomas



--
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 HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5= 629FEC90B1652F5334%40Pli.gst.uqam.ca.
--000000000000258f2105a517a3ad--