(1-topos) theory in set theory vs HoTT

[Matt Oliveri]

I have two related questions about how the facts of ordinary (1-) categorical logic play out in set theory vs in HoTT. These questions have to do with the fact that in HoTT there's a difference between strict categories and univalent categories, while in set theory, there isn't. (Or, if you insist, there's no such thing as a univalent category.) So I don't think it matters whether, for example, the set theory is classical; you can just compare to an analogous HoTT. It seems like a lot of papers on toposes use Grothendieck fibrations, and (I learned somewhat recently) these only make sense for strict categories. So here are the questions:

1) Has a lot of categorical logic already been worked out for an alternative notion of fibration, such that it ought to be straightforward to port the development to speak of univalent categories in HoTT?

2) If so, is there some big handy theorem saying that everything works out essentially the same as with Grothendieck fibrations?

I ask because if it's not the case that the answer to both questions is "yes", then it seems to me like strict categorical logic and univalent categorical logic need to be pessimistically considered distinct subjects. (And I wouldn't be sure what to do about that or if I would even care; I'm just curious.)

[Matt Oliveri]

I changed the question to be about categorical logic, rather than topos theory, but I forgot to change the subject line. Sorry. The question is really about categorical logic. But topos theory is related, so information about that is not off-topic.

[Michael Shulman]

Firstly, I want to point out that the use of Grothendieck fibrations
in categorical logic and type theory is at the meta-level, when we
construct interpretations of a formal deductive system (such as HoTT)
into a categorical structure. So the question of how to define or
replace Grothendieck fibrations in HoTT is irrelevant to the
*inclusion* of HoTT as a subfield of categorical logic and type theory
and the interpretation of HoTT into categories; what matters for that
is, at most, the use of Grothendieck fibrations in the *meta-theory*
where we prove such things *about* HoTT. At present, such meta-theory
has generally been taken to be set-theoretic, so that this is not an
issue; but eventually it would indeed be nice to be able to use HoTT
as the meta-theory for its own interpretation too ("eating itself").

Secondly, I would say that the short answers to your two questions are
(1) yes, it's called a pseudofunctor to Cat (a.k.a. an "indexed
category"), and (2) yes, there is an equivalence of 2-categories
between pseudofunctors to Cat and Grothendieck fibrations. In fact
this is a "categorification" of the basic HoTT "object-classifier"
equivalence between maps into a (small) type Sigma(A:U) (A -> B) and
type families B -> U. Is that enough, or do you want more
explanation? You may also be interested in displayed categories
(https://ncatlab.org/nlab/show/displayed+category), which are the
indexed-category analogue of a functor that's not yet known to be a
Grothendieck fibration.

> --
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Matt Oliveri]

Right, these questions are about doing metatheory in HoTT. And not necessarily the metatheory of HoTT itself. It looks like you've answered them. Thanks!

[Hendrik Boom]

On Sat, Dec 15, 2018 at 04:20:06AM -0800, Michael Shulman wrote:
> eventually it would indeed be nice to be able to use HoTT
> as the meta-theory for its own interpretation too ("eating itself").

Can't the metatheory of type theory up to U_n be expressed in U_n+1?
or is here something about HoTT getting in the way of this?

-- hendrik

[Michael Shulman]

If by U_n you mean the universe of n-types (rather than just the n-th
universe in a hierarchy that contains types of no finite h-level from
the beginning), then yes I would expect so, but to my knowledge no one
has actually done it.