Dear Ulrik,

You wrote:

<<The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets. I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.>>

I like the idea of calling exo-skeleton the outer layer of a type theory.

Category theorists like to distinguish between the internal and the external properties of a category.

Logician are distinguishing a formal theory from its meta-theory.

A theory and its meta-theory may interact as in Gödel's incompleteness theorem.

There are two layers interacting in ML type theory.

Is it possible to interpret the outer layer internally, as in Gödel's incompleteness theorem?

You wrote:

<<Again, let me remind everyone, that groups are precisely one of the few structures we know how to handle (along with grouplike E_n-types, and connective/general spectra): To equip a type G with a group structure is to give a pointed connected type BG and an equivalence of G with the loop type of BG. The type of objects of Gr is the universe of pointed, connected types.>>

I like the idea of studying groups via the equivalence between groups and pointed connected spaces.

It is one of the great miracle of homotopy theory (discovered by Kan).

It is quite amazing if you think about it: (non-abelian) groups were introduced for the purpose

of studying symmetries, mostly in Galois theory. The fundamental group of a space was introduced

by Poincaré to study covering spaces in connection with the Klein-Poincaré

uniformisation theorem for Riemann surfaces. The loop space of a pointed space

is a kind of beef-up version of the fundamental group; the fact that it contains

all the homotopy invariant informations about that space is a great marvel.

Topologists are interested in nilpotent groups (ex. the work of Hilton) and

the connection with Lie algebras (the Whitehead bracket).

By a theorem of Quillen, connected differential graded Lie algebras are rational models of simply connected spaces.

Also, in Goodwillie's calculus, the derivative of the identity functor is the Lie algebra operad.

I am afraid the equivalence between groups and pointed connected spaces

will be meaningless (tautological) if the former is defined to be the latter.

Best,

André

From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ulrik Buchholtz [ulrikbu...@gmail.com]
Sent: Sunday, May 10, 2020 8:53 AM
To: Homotopy Type Theory
Subject: Re: [HoTT] Identity versus equality

Dear André,

On Saturday, May 9, 2020 at 10:18:11 PM UTC+2, joyal wrote:

But I find it frustrating that I cant do my everyday mathematics with it.

For example, I cannot say

(1) Let X:\Delta^{op}---->Type be a simplicial type;

Let me remind everyone that we don't have a proof that it's impossible to define simplicial types in book HoTT! As long as we haven't settled this question either way, the predicament we're in (and I agree it's a predicament) is more an indictment of type theorists than of type theory. (And I include myself as a type theorist here.)

Anyway, from your phrasing of (1), it looks like you're after a directed type theory. Several groups are working on type theories where your (1) is valid syntax, but you have to write Space (or Anima or ...) to indicate the covariant universe of homotopy types and maps, rather than the full universe.

(2) Let G be a type equipped with a group structure;

(3) Let BG be the classifying space of a group G;
(4) Let Gr be the category of groups;

Again, let me remind everyone, that groups are precisely one of the few structures we know how to handle (along with grouplike E_n-types, and connective/general spectra): To equip a type G with a group structure is to give a pointed connected type BG and an equivalence of G with the loop type of BG. The type of objects of Gr is the universe of pointed, connected types.

When you replace groups by monoids, it gets more embarrassing.

Earlier (on May 7) you wrote:

At some level, all mathematics is based on some kind of set theory.
Is it not obvious?
We cannot escape Cantor's paradise!

That is exactly the question, isn't it?

What HoTT/UF offers us is another axis of foundational variation, besides the old classical/constructive, impredicative/predicative, infinitist/finitist, namely: everything is based on sets/general homotopy types are not reducible to sets.

I don't know of catchy names for these positions, but I think that working with HoTT has a tendency of making the latter position more plausible: Why should there for any type be a set that surjects onto it?

A question: Recall that if we assume the axiom of choice (AC) for sets, then there is a surjection from a set onto Set, namely the map that takes a cardinal (or ordinal) to the set of ordinals below it.
Is there (with AC for sets) also a surjection from a set to the type of 1-types? To the full universe?

The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets. I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.

Best wishes,

Ulrik

--
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 HomotopyTypeTheory+unsu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/e47e6263-d0eb-4882-ab07-e31483095bd4%40googlegroups.com.