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é 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é 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 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 >> . >> >