From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aca:403:: with SMTP id 3mr8912050oie.166.1588895039050; Thu, 07 May 2020 16:43:59 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3104:: with SMTP id x4ls1881984oix.0.gmail; Thu, 07 May 2020 16:43:57 -0700 (PDT) X-Received: by 2002:aca:f182:: with SMTP id p124mr8747666oih.170.1588895037330; Thu, 07 May 2020 16:43:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588895037; cv=none; d=google.com; s=arc-20160816; b=Krbtb+KbG32IuUHMI4OQjbasuCmdLISDxlYNjZUkIbOyfc5xWSzj27Uu7RI86SPvZR H+Q+Gfu9ene+VS90QT7kWKLz/VuqSmtVGdeuLKkVKRv8q2+zRenZ+8ZM9ihQsFpsU2dW R3lUCLEZso5D75AneaMHzcWLhQv2dKg/tUEDjAc4csr//m23GWvod4iCoqeexRwQ9WfG qxSvOlevqpqcH3LzItkmCnXkOpzCq7ivcl2DW2NRqqEevYmzO1FBkTL+2zUQlZeX2aVJ zRTAMddNjFgpYDEgP5bMlMBP/DYA1etG/gWslu6mhU/x9HOVvJM+e2SMw0RW9LFWsOc4 ahLw== 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:cc:to :from:ironport-sdr; bh=oJn2I2cj4l7MSCOopnyszPaS1G+1K6vRliy/GHVw+wY=; b=HQcLvEPNSl7lhp4up2wQhwo4kRy1AO5IOs8kDUGYzRLzBBq4gAsdRqIgUzqhQhvmKT fcpIk01Iqf4RANh1ytxJVt8lm/kj71hUWR7kZ6UslZe5ZccLSVYVFgvdFTMetDFz7TlM tPLqpTt2YkJtcWGoMXoxAfwEXA85JlTZi3WL8xKPld2Tyl8Y0oKgj8VuHs3t7RzN5Wnj FcQkKnELkSJoH9+KnlCtAFqmMne58iJ7xjXo+nC1+bsT609BXuCUCJ971gbAcNU6xXc5 3cPIeamBJyH0LV7KeXbKutRRxvUmnORQGeFG54NHyHX5msO8wUAzaO4f0rZ4xiaw1fEM hFLw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail5.uqam.ca (mail5.uqam.ca. [132.208.246.108]) by gmr-mx.google.com with ESMTP id k65si495678oih.1.2020.05.07.16.43.57 for ; Thu, 07 May 2020 16:43:57 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) client-ip=132.208.246.108; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: RWu3xNWrMwACOQaHibI5A9w4U2MoNoHh+kNSFgHmPjruLsUPHdWwEuD/bcDDbkDKL9BHjAxF96 DfSA8fYVvHKFesLiIVq0n8F5yg449EdWdf3/+LYDrNwuph6x0cmbRjYrOoyrY/IdhE8SUprLEh o9YgQdneeX+/gp+6dUPPmVVB5pZkdJwjvB6ZQIpYBK1KaGWh6bY+RjcBpX/PDSedJ7PKpMA2w1 qAUXaj/ua+twWr/Bs/K3Ioqnl/RUvLQztCL3Tc+WgYiTTjF3Kf1hS06eSZqyOGf1ZarAlo1CIj Czc= X-IronPort-AV: E=Sophos;i="5.73,365,1583211600"; d="scan'208,217";a="11777464" Received: from unknown (HELO Billet.gst.uqam.ca) ([132.208.216.73]) by mail7.uqam.ca with ESMTP; 07 May 2020 19:43:57 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Billet.gst.uqam.ca ([169.254.5.38]) with mapi id 14.03.0439.000; Thu, 7 May 2020 19:43:56 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: David Roberts CC: Thomas Streicher , "Thorsten Altenkirch" , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOF Date: Thu, 7 May 2020 23:43:55 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> 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: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: multipart/alternative; boundary="_000_8C57894C7413F04A98DDF5629FEC90B1652F53A3Pligstuqamca_" MIME-Version: 1.0 --_000_8C57894C7413F04A98DDF5629FEC90B1652F53A3Pligstuqamca_ Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable 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)-category. 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) 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=E9 ________________________________ From: David Roberts [drober...@gmail.com] Sent: Thursday, May 07, 2020 5:41 PM To: Joyal, Andr=E9 Cc: Thomas Streicher; Thorsten Altenkirch; Michael Shulman; Steve Awodey; h= omotopyt...@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=E9 > wrote: Thank you all for your comments. Thomas wrote: <> 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 a= t 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=E9 ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] Sent: Thursday, May 07, 2020 6:09 AM To: Thorsten Altenkirch Cc: Joyal, Andr=E9; Michael Shulman; Steve Awodey; homotopyt...@googlegroup= s.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 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 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 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 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 e= mail to HomotopyT...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F5334%40Pli.gst.uqam.= ca. --_000_8C57894C7413F04A98DDF5629FEC90B1652F53A3Pligstuqamca_ Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable
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) 
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=E9

From: David Roberts [drober...@gmail.com]=
Sent: Thursday, May 07, 2020 5:41 PM
To: Joyal, Andr=E9
Cc: Thomas Streicher; Thorsten Altenkirch; Michael Shulman; Steve Aw= odey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

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

I'm sorry, but where does it say that? The whole point of ETCS wa= s to avoid an ambient set theory, no? Not to mention the original 'General = theory of natural equivalences' avoided defining categories using sets.

Humbly,
David


On Fri, 8 May 2020 at 01:43, Joyal, A= ndr=E9 <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 a= t 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=E9



________________________________________
From: Thomas Streicher [stre...@mathematik.tu-darm= stadt.de]
Sent: Thursday, May 07, 2020 6:09 AM
To: Thorsten Altenkirch
Cc: Joyal, Andr=E9; 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 from 1985.<= br> 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 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 HomotopyTypeTheory+unsu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5= 629FEC90B1652F5334%40Pli.gst.uqam.ca.
--_000_8C57894C7413F04A98DDF5629FEC90B1652F53A3Pligstuqamca_--