Re: [HoTT] Identity versus equality

[Michael Shulman <shu...@sandiego.edu>]

On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
> 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.

Exactly!

> 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?

As far as I know, it is an open question whether AC for sets implies
these stronger principles (although I'd be surprised if it were true).
Those principles are true, of course, in the model of simplicial sets
based on ZFC, and there are models in which they fail, but I don't
know of a model in which they fail but AC for sets holds.  Although I
don't think I've really tried to look for one either; has anyone?

There is however the theorem stated at
https://ncatlab.org/nlab/show/n-types+cover#relation_to_other_axioms,
that AC for sets together with the axiom "every type is surjected onto
by a set" is equivalent to the "oo-AC" that "every surjection onto a
set has a section".

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

While I kind of see how one could say this, I think it's misleading
especially in light of the above dichotomy, becuase 2LTT doesn't imply
any of the *internal* "types are based on sets" axioms for the fibrant
layer.  As you know, 2LTT without additional axioms is conservative
over HoTT, while even with stronger axioms it can still be modeled in
many or all higher toposes.

> 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 think "exo-" is a great prefix for the outer layer!