Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: general

Topic: Universes in (ML)-type theory

Alexander Gietelink Oldenziel (Nov 07 2020 at 12:35):

Where are universe essentially used in Martin-Lof type theory? I understand you need a Universe type to state the univalence axiom in HoTT but it seems to me one can do much of non-homotopic type theory without universes.

Shea Levy (Nov 07 2020 at 12:43):

Alexander Gietelink Oldenziel said:

Where are universe essentially used in Martin-Lof type theory? I understand you need a Universe type to state the univalence axiom in HoTT but it seems to me one can do much of non-homotopic type theory without universes.

You can't even prove $1 \ne 0$ without them :smile:

Shea Levy (Nov 07 2020 at 12:46):

e.g. a verbose version of the proof in coq:

Definition one_ne_zero : 1 ≠ 0 :=
  λ (p : 1 = 0),
  match p as _ in _ = zero return match zero return Type with
                                  | 0 => False
                                  | S _ => IDProp
                                  end with
  | eq_refl => idProp
  end.

The match in the return requires a universe (here, Type)

Shea Levy (Nov 07 2020 at 12:53):

I've thought about a scheme without a closed universe type term, but with a more direct notion of polymorphism, and you'd have a type code interpretation operator that takes a term in a context with the universe code primitives as variables of some polymorphically bound T. Not sure it actually gains anything but it's always annoyed me that type codes don't compute and yet we pretend they're values :tongue:

Ulrik Buchholtz (Nov 07 2020 at 13:05):

Alexander Gietelink Oldenziel said:

Where are universe essentially used in Martin-Lof type theory? I understand you need a Universe type to state the univalence axiom in HoTT but it seems to me one can do much of non-homotopic type theory without universes.

Besides the use in characterizing identity types mentioned above by Shea Levy, universes are used to define structures and constructions on them, and hence they're crucial for category theory.
As a simple example, the type of pointed sets (relative to a universe) can be defined as $\sum_{X:\mathrm{Set}}X$, where $\mathrm{Set}$ is a universe of sets. (In HoTT, this would itself be a sigma-type over the universe; in MLTT with UIP, it would just be the universe.)
The type of groups would be defined as $\sum_{G:\mathrm{Set}}\sum_{e:G}\sum_{\mu:G\to G\to G}\mathrm{isGroup}(G,e,\mu)$, etc.

sarahzrf (Nov 09 2020 at 01:26):

Shea Levy said:

Alexander Gietelink Oldenziel said:

Where are universe essentially used in Martin-Lof type theory? I understand you need a Universe type to state the univalence axiom in HoTT but it seems to me one can do much of non-homotopic type theory without universes.

You can't even prove $1 \ne 0$ without them :smile:

it's possible to give a large elimination rule w/o a universe!

sarahzrf (Nov 09 2020 at 01:27):

e.g., image.png

Alexander Gietelink Oldenziel (Nov 10 2020 at 11:52):

Shea Levy said:

Alexander Gietelink Oldenziel said:

Where are universe essentially used in Martin-Lof type theory? I understand you need a Universe type to state the univalence axiom in HoTT but it seems to me one can do much of non-homotopic type theory without universes.

You can't even prove $1 \ne 0$ without them :smile:

Okay... this confuses me a little.
My understanding is that dependent type theories are modelled by fibrations (with extra structure), but most of these fibrations do not have universes I believe. E.g., I don't think the codomain fibration of a topos has a universe.
How does this work?

Ulrik Buchholtz (Nov 10 2020 at 12:16):

@Alexander Gietelink Oldenziel If you don't have any universes (and no large eliminations), then you can have a model where, intuitively, non-empty types are modeled by a singleton, while empty types are modeled by the empty type. The reference is this 1988 JSL article by Jan Smith.

Kenji Maillard (Nov 10 2020 at 12:21):

And I think universes are often taken as part of the "extra stuff" you mention, as are $\Pi$-types, dependent sums, ...

Alexander Gietelink Oldenziel (Nov 10 2020 at 12:44):

Ulrik Buchholtz said:

Alexander Gietelink Oldenziel If you don't have any universes (and no large eliminations), then you can have a model where, intuitively, non-empty types are modeled by a singleton, while empty types are modeled by the empty type. The reference is this 1988 JSL article by Jan Smith.

So I think I understand this. What I don't understand: the categorical semantics of Martin-Lof type theory in a topos should be (more or less?) the codomain fibration of the topos. However, I don't think that this fibration has a universe?

sarahzrf (Nov 10 2020 at 13:16):

just because a system has a semantics and something is true in that semantics, it doesnt mean the thing is derivable in the system

sarahzrf (Nov 10 2020 at 13:16):

or, wait, are you asking how to model universes in that semantics?

Kenji Maillard (Nov 10 2020 at 13:20):

@Alexander Gietelink Oldenziel I think that in order to interpret MLTT with $n$ universes in a topos (or rather in the codomain fibration of the topos) you need to ask for $n$ (suitable) object classifiers on your topos. In the case of $\mathcal{Set}$ I think it correspond to the assumption that you have $n$ Grothendieck universes

Alexander Gietelink Oldenziel (Nov 10 2020 at 13:31):

Kenji Maillard said:

Alexander Gietelink Oldenziel I think that in order to interpret MLTT with $n$ universes in a topos (or rather in the codomain fibration of the topos) you need to ask for $n$ (suitable) object classifiers on your topos. In the case of $\mathcal{Set}$ I think it correspond to the assumption that you have $n$ Grothendieck universes

Wait, you are saying we need inaccesible cardinal (which I believe is equivalent to Grothendieck universes?) to have a categorical semantics in topoi for ML-type theory? That sounds quite worrisome. =D

Alexander Gietelink Oldenziel (Nov 10 2020 at 13:33):

sarahzrf said:

or, wait, are you asking how to model universes in that semantics?

Yes. My understanding is that the 'correct/natural/canonical' semantics of ML-type theory is some variant of a topos.
(and an $\infty$-topos for HoTT). So how do we interpret the apparently essential Universe of ML-type theory in a given topos $E$ (or more precisely, some variant of its codomain fibration)?

sarahzrf (Nov 10 2020 at 13:34):

well, it's not essential, just quite useful

sarahzrf (Nov 10 2020 at 13:35):

but yes, i believe you generally aren't going to be able to interpret MLTT with a universe in an arbitrary elementary topos

sarahzrf (Nov 10 2020 at 13:35):

(actually, MLTT should morally be interpretable in any locally cartesian closed category; elementary topoi just give an abundant supply of those)

sarahzrf (Nov 10 2020 at 13:36):

iirc, the semantics of a universe is indeed going to be some kind of, well, semantical universe—something that behaves akin to an inaccessible cardinal

Kenji Maillard (Nov 10 2020 at 13:37):

Why would that be worrisome ? MLTT already has good enough syntactic properties (strong-normalization, decidability of conversion and type checking) to stand on its own independently of a not-so-well suited set-theoretic model

sarahzrf (Nov 10 2020 at 13:37):

but note that you should certainly be able to give semantics in topoi other than Set, where such universes may be easier to come by

sarahzrf (Nov 10 2020 at 13:39):

i'm not terribly knowledgable on this topic, but im pretty sure that there are methods based on realizability that let you construct nice categories, particularly topoi, that model useful and unusual universe-y stuff

sarahzrf (Nov 10 2020 at 13:39):

i seem to recall that the effective topos believes itself to contain a non-posetal complete small category

sarahzrf (Nov 10 2020 at 13:42):

(note that the theorem which states that such a thing can't exist hinges on LEM—it doesn't go through in the effective topos!)

Tom de Jong (Nov 10 2020 at 13:47):

sarahzrf said:

i seem to recall that the effective topos believes itself to contain a non-posetal complete small category

Indeed, there are two papers discussing this: "A Small Complete Category" by Hyland and "The Discrete Objects in the Effective Topos" by Hyland, Robinson and Rosolini.

sarahzrf (Nov 10 2020 at 13:49):

ah, i had this one open :-) image.png

sarahzrf (Nov 10 2020 at 13:49):

i shd probably read it at some point...

Alexander Gietelink Oldenziel (Nov 10 2020 at 13:50):

Kenji Maillard said:

Why would that be worrisome ? MLTT already has good enough syntactic properties (strong-normalization, decidability of conversion and type checking) to stand on its own independently of a not-so-well suited set-theoretic model

I wasn't sure whether ' worrisome' is the right choice of words. Certainly for MLTT as a syntactic formal system there is no problem whatsoever.

But for the claim that the internal language of a topos is MLTT, I do find this peculiar...

sarahzrf (Nov 10 2020 at 13:50):

more like MLTT w/ a universe of propositions

sarahzrf (Nov 10 2020 at 13:50):

but not a universe of types

sarahzrf (Nov 10 2020 at 13:51):

i guess there's some "stack semantics" which might be relevant to that though... but i never got very far into that one before getting distracted >_<

sarahzrf (Nov 10 2020 at 13:52):

er, i suppose stack semantics is relevant to quantification over types, less so to internalizing that as an instance of ordinary quantification

sarahzrf (Nov 10 2020 at 13:52):

(...or maybe it is; i wouldnt know since i havent, yknow, read about it :sweat_smile:)

Kenji Maillard (Nov 10 2020 at 13:56):

Alexander Gietelink Oldenziel said:

But for the claim that the internal language of a topos is MLTT, I do find this peculiar...

Yes that claim is inadequate: on the one hand you need to add the structure of a universe to your topos to interpret the "usual" MLTT with a universe, on the other hand a topos is proof-irrelevant and satisfy function extensionality that you should then add to your type theory (it agrees with the original extensional variant of MLTT with equality reflection though)

Dan Doel (Nov 10 2020 at 16:03):

@Alexander Gietelink Oldenziel MLTT doesn't have a subobject classifier, so universes get used for some things that could be done with one of those instead, because they are the smallest classifier of $0$ and $1$, basically.

Dan Doel (Nov 10 2020 at 16:15):

A subobject classifier actually is a sort of universe, arguably. So topoi do have universes in that sense. Just a different universe than MLTT.

Also, a subobject classifier seems to be a much stronger assumption than the universe in MLTT.