```
From: David Roberts <drober...@gmail.com>
To: "Joyal, André" <"joyal..."@uqam.ca>
Cc: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>,
Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>,
Michael Shulman <shu...@sandiego.edu>,
Steve Awodey <awo...@cmu.edu>,
"homotopyt...@googlegroups.com" <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Identity versus equality
Date: Fri, 8 May 2020 09:26:51 +0930 [thread overview]
Message-ID: <CAFL+ZM-X6tkX+666LTkfPqG1ALeytO=5-7A1XUn8f5q8AdgNqA@mail.gmail.com> (raw)
In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca>
[-- Attachment #1: Type: text/plain, Size: 8596 bytes --]
Dear André,
I merely meant that the definition of category only requires first-order
logic as in (Eilenberg–Mac Lane 1945), or at best a low-level dependent
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é <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)-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é
>
> ------------------------------
> *From:* David Roberts [drober...@gmail.com]
> *Sent:* Thursday, May 07, 2020 5:41 PM
> *To:* Joyal, André
> *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é <joyal...@uqam.ca> wrote:
>
>> Thank you all for your comments.
>>
>> Thomas wrote:
>>
>> <<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).>>
>>
>> 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
>> more fundamental.
>>
>> Best,
>> André
>>
>>
>>
>> ________________________________________
>> From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
>> Sent: Thursday, May 07, 2020 6:09 AM
>> To: Thorsten Altenkirch
>> Cc: Joyal, André; 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
>> 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
>> email to HomotopyT...@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F5334%40Pli.gst.uqam.ca
>> .
>>
>
[-- Attachment #2: Type: text/html, Size: 11466 bytes --]
```

next prev parent reply other threads:[~2020-05-07 23:57 UTC|newest]Thread overview:61+ messages / expand[flat|nested] mbox.gz Atom feed top 2020-05-05 8:47 Ansten Mørch Klev 2020-05-06 16:02 ` [HoTT] " Joyal, André 2020-05-06 19:01 ` Steve Awodey 2020-05-06 19:18 ` Michael Shulman 2020-05-06 19:31 ` Steve Awodey 2020-05-06 20:30 ` Joyal, André 2020-05-06 22:52 ` Thorsten Altenkirch 2020-05-06 22:54 ` Thorsten Altenkirch 2020-05-06 23:29 ` Joyal, André 2020-05-07 6:11 ` Egbert Rijke 2020-05-07 6:58 ` Thorsten Altenkirch 2020-05-07 9:04 ` Ansten Mørch Klev 2020-05-07 10:09 ` Thomas Streicher 2020-05-07 16:13 ` Joyal, André 2020-05-07 21:41 ` David Roberts 2020-05-07 23:43 ` Joyal, André2020-05-07 23:56 ` David Roberts [this message]2020-05-08 6:40 ` Thomas Streicher 2020-05-08 21:06 ` Joyal, André 2020-05-08 23:44 ` Steve Awodey 2020-05-09 2:46 ` Joyal, André 2020-05-09 3:09 ` Jon Sterling [not found] ` <CADZEZBY+3z6nrRwsx9p-HqYuTxAnwMUHv7JasHy8aoy1oaGPcw@mail.gmail.com> 2020-05-09 2:50 ` Steve Awodey 2020-05-09 8:28 ` Thomas Streicher 2020-05-09 15:53 ` Joyal, André 2020-05-09 18:43 ` Thomas Streicher 2020-05-09 20:18 ` Joyal, André 2020-05-09 21:27 ` Jon Sterling 2020-05-10 2:19 ` Joyal, André 2020-05-10 3:04 ` Jon Sterling 2020-05-10 9:09 ` Thomas Streicher 2020-05-10 11:59 ` Thorsten Altenkirch 2020-05-10 11:46 ` Thorsten Altenkirch 2020-05-10 14:01 ` Michael Shulman 2020-05-10 14:20 ` Nicolai Kraus 2020-05-10 14:34 ` Michael Shulman 2020-05-10 14:52 ` Nicolai Kraus 2020-05-10 15:16 ` Michael Shulman 2020-05-10 15:23 ` Nicolai Kraus 2020-05-10 16:13 ` Nicolai Kraus 2020-05-10 16:28 ` Michael Shulman 2020-05-10 18:18 ` Nicolai Kraus 2020-05-10 19:15 ` Thorsten Altenkirch 2020-05-10 19:20 ` Thorsten Altenkirch 2020-05-10 12:53 ` Ulrik Buchholtz 2020-05-10 14:01 ` Michael Shulman 2020-05-10 14:27 ` Nicolai Kraus 2020-05-10 15:35 ` Ulrik Buchholtz 2020-05-10 16:30 ` Michael Shulman 2020-05-10 18:56 ` Nicolai Kraus 2020-05-10 18:04 ` Joyal, André 2020-05-11 7:33 ` Thomas Streicher 2020-05-11 14:54 ` Joyal, André 2020-05-11 16:37 ` stre... 2020-05-11 16:42 ` Michael Shulman 2020-05-11 17:27 ` Thomas Streicher 2020-05-10 16:51 ` Nicolai Kraus 2020-05-10 18:57 ` Michael Shulman 2020-05-10 19:18 ` Nicolai Kraus 2020-05-10 20:22 ` Michael Shulman 2020-05-10 22:08 ` Joyal, André

Be sure your reply has aReply instructions:You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the--to,--cc, and--in-reply-toswitches of git-send-email(1): git send-email \ --in-reply-to='CAFL+ZM-X6tkX+666LTkfPqG1ALeytO=5-7A1XUn8f5q8AdgNqA@mail.gmail.com' \ --to="drober..."@gmail.com \ --cc="Thorsten...."@nottingham.ac.uk \ --cc="awo..."@cmu.edu \ --cc="homotopyt..."@googlegroups.com \ --cc="joyal..."@uqam.ca \ --cc="shu..."@sandiego.edu \ --cc="stre..."@mathematik.tu-darmstadt.de \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).