Re: [HoTT] Identity versus equality

[David Roberts <drober...@gmail.com>]

[-- 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 --]