From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:6e02:801:: with SMTP id u1mr17997335ilm.167.1588887688509; Thu, 07 May 2020 14:41:28 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:3a05:: with SMTP id h5ls606597ila.1.gmail; Thu, 07 May 2020 14:41:27 -0700 (PDT) X-Received: by 2002:a92:d30c:: with SMTP id x12mr16436098ila.95.1588887687068; Thu, 07 May 2020 14:41:27 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588887687; cv=none; d=google.com; s=arc-20160816; b=pdH3YtXIdX7E7hzDTxQCiXb5BC5jNGYXtwOvrGTS2SQOqjHWC/iVsd7eI8gQ/yng5g XunKlK/Sj0+Jb+eyG+Q2rx1uWcMfLJh2Hv8EOPKzv9Y+QaSPf9Wc245A6oxBkN/MofMh CaRb4zf6lNTbEbvYfj5xys4kv/praQb4zhg2bRvvo4RJgEvbSWcEaVDmf3buM8am9I1I Z6MTWRcKresIGSYp471rOI89jujUxBDCs87XEG2lrRiOFl6cQOf8nCDCt8k0fRnXS+8O +fGfm6s9kexuladkmXgHP90K2QCmZmelWGEJIJQaFvCJFFD5r4TkdrJsM8urebRXzGZ0 X/kg== 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=uz+t2iXk/emTWDK+4eSIim1GZ58SaPHJ8sNeUzhkxOg=; b=lAXQzBYJB1zHtVs5abMgm3FaK6RzTDv5YRHViOhqPRrUMXslzrx2PP07LGHDaMVqwJ cHGqCsM4t8DG2gnHSQ3oL44dZvYgpZ5Z2y2iMWvTKDZIcBjuBxGsadxOZLLzW8CoXJb4 BgPI7xJN3hS/wtL8nHGPewYv9abbD+HmRlBmsAc2LtjfW6iTnsPPzsJbPr52TPnoQZ68 B+DMtRei376RKGa+FyENacN2CkXyyuOfbB+BGMexWAaANxFR7UY6gdXq9HyPZKhlh/mt JxrTkNZ/EWTkzDbXHdABppMct38dfZsLiac8IoXgnYiB3pEOEhUSEUuTz/UXFF1OYVeq i5HA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=obSWp+6a; spf=pass (google.com: domain of drober...@gmail.com designates 2607:f8b0:4864:20::b2b 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-xb2b.google.com (mail-yb1-xb2b.google.com. [2607:f8b0:4864:20::b2b]) by gmr-mx.google.com with ESMTPS id x4si564324iof.0.2020.05.07.14.41.27 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 07 May 2020 14:41:27 -0700 (PDT) Received-SPF: pass (google.com: domain of drober...@gmail.com designates 2607:f8b0:4864:20::b2b as permitted sender) client-ip=2607:f8b0:4864:20::b2b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=obSWp+6a; spf=pass (google.com: domain of drober...@gmail.com designates 2607:f8b0:4864:20::b2b as permitted sender) smtp.mailfrom=drober...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-yb1-xb2b.google.com with SMTP id w19so267442ybs.5 for ; Thu, 07 May 2020 14:41:27 -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=uz+t2iXk/emTWDK+4eSIim1GZ58SaPHJ8sNeUzhkxOg=; b=obSWp+6aNxWy1bjE6DtPlXeRAxU6d09/Xwp0piXCmqRZAhfGWP70+GwjVeg1OYXoDl iRzmlB5OTyWawUm+MZ66+x0K8foVNDo66jlXatqWTCwxDSVLOiXxORZ2r5XX1s790dhr UnihHQdX0VVixAHgUmkcIbmfleYCsZDx3CL9AXDnwGRjbq76jYPA5RZ4938kSI7Hu80n UsnkqvU4cBNRNsdzOln7JhVQo3UZeVqW2/cTIkFo4FrUCkYBkqwb2KJ5i8u1pu9eivLI 6Ox1oRlKUBaTeDn4LgHfhuMVT/rgJ3UGHNsq9I7/GHjs58myyqHlqdh+kUDyWggCcZlU KS9g== X-Gm-Message-State: AGi0PuYhtp2/QTGex5N72K0mWjOGlwcYdP0Gi7yX6hBk/UrtBzHF56Zy UzSyo/W5JDlsEtjdG6drnnJwWJBVUWjwYk6vzx4= X-Received: by 2002:a5b:50c:: with SMTP id o12mr25919956ybp.264.1588887686708; Thu, 07 May 2020 14:41:26 -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> In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> From: David Roberts Date: Fri, 8 May 2020 07:11:15 +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="000000000000277feb05a515be55" --000000000000277feb05a515be55 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable >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 homotopi= c. > 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 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 > 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 mor= e > 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) 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 homotopi= c. > 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 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 languag= e > 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 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 > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyT...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DD= F5629FEC90B1652F5334%40Pli.gst.uqam.ca > . > --000000000000277feb05a515be55 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
>every category has a set of objects and a set of arrow= s.

I'm sorry,=C2=A0but where does it say that? The w= hole point of ETCS was to avoid an ambient set theory, no? Not to mention t= he original 'General theory of natural equivalences' avoided defini= ng categories using sets.

Humbly,

On Fri, 8 May 2020 at 01:43, Joy= al, Andr=C3=A9 <joyal...@uqam.ca= > wrote:
Than= k 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-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 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.c= om/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F5334%40Pl= i.gst.uqam.ca.
--000000000000277feb05a515be55--