Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed
From: David Roberts <drober...@gmail.com>
To: "Joyal, André" <"joyal..."@uqam.ca>
Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>,
Michael Shulman <shu...@sandiego.edu>,
Steve Awodey <awo...@cmu.edu>,
Subject: Re: [HoTT] Identity versus equality
Date: Fri, 8 May 2020 09:26:51 +0930	[thread overview]

[-- 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
> *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:
>
>>
>> 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é
>>
>>
>>
>> ________________________________________
>> Sent: Thursday, May 07, 2020 6:09 AM
>> To: Thorsten Altenkirch
>> Cc: Joyal, André; Michael Shulman; Steve Awodey;
>> 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
>> To view this discussion on the web visit
>> .
>>
>

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


Reply 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,

Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

switches of git-send-email(1):

git send-email \
--to="drober..."@gmail.com \
--cc="Thorsten...."@nottingham.ac.uk \
--cc="awo..."@cmu.edu \
--cc="joyal..."@uqam.ca \
--cc="shu..."@sandiego.edu \

This is a public inbox, see mirroring instructions
as well as URLs for NNTP newsgroup(s).`