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>
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 07:11:15 +0930	[thread overview]
Message-ID: <CAFL+ZM-6k+ZCghasFyTyXfC-fGbraPThcdsMdzsgsLRiaw8Dcg@mail.gmail.com> (raw)
In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca>

[-- Attachment #1: Type: text/plain, Size: 6453 bytes --]

>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: 7722 bytes --]

  reply	other threads:[~2020-05-07 21:41 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 [this message]
2020-05-07 23:43                   ` Joyal, André
2020-05-07 23:56                     ` David Roberts
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,
  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-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAFL+ZM-6k+ZCghasFyTyXfC-fGbraPThcdsMdzsgsLRiaw8Dcg@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 the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).