RE: [HoTT] Identity versus equality

["Joyal, André" <"joyal..."@uqam.ca>]

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

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<mailto: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<mailto: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<mailto: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<mailto:HomotopyTypeTheo...@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: 10220 bytes --]