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: learning: questions

Topic: universal properties for positive types

Josselin Poiret (Jul 08 2025 at 16:54):

Mike Shulman said:

That isn't the case for any other type constructors that I know of, because they all have a universal property

that isn't the case for positive types though! I don't have anything formal here, but you could probably add some exception in the model that bubbles up to positive types

Mike Shulman (Jul 08 2025 at 16:54):

Um, yes it is? $A+B$ is a coproduct?

Josselin Poiret (Jul 08 2025 at 16:55):

the syntactic rules don't force uniqueness: it's a weak colimit

Mike Shulman (Jul 08 2025 at 16:55):

In dependent type theory you can prove that it's a strong colimit, propositionally.

Josselin Poiret (Jul 08 2025 at 16:56):

yes, but the propositional here is the key: definitionally, the type doesn't have to behave as a strong colimit

Mike Shulman (Jul 08 2025 at 16:57):

But that's irrelevant to my point. The propositional universal property characterizes the type up to equivalence, so you don't have any freedom in choosing what it should be semantically.

Josselin Poiret (Jul 08 2025 at 17:04):

I still disagree about positive types being forced to be colimits in the model: in MLTT with a universe, negative dependent pairs, dependent function types and ⊥, you can surely add an extra inhabitant in the model to the interpretation of ⊥, and propagate it to other type formers by just bubbling it up

Mike Shulman (Jul 08 2025 at 17:07):

Do you mean that for an interpretation of MLTT in Set, for instance, you can choose $\bot$ to be interpreted by a 1-element set rather than a 0-element set? In that case it won't satisfy the elimination rule, since there won't be a map out of it into an empty set.

Josselin Poiret (Jul 08 2025 at 17:07):

but what if you can't access any empty set in the model using the syntax? all my types are inhabited, so you won't be able to test for that

Josselin Poiret (Jul 08 2025 at 17:08):

the eliminator in the syntax won't let you talk about the empty set of the semantics

Mike Shulman (Jul 08 2025 at 17:08):

A "model" has to satisfy all the rules of the theory. In a model of the theory of groups, you have to be able to multiply any two elements, not just any two elements that are "describable using syntax".

Josselin Poiret (Jul 08 2025 at 17:09):

that depends on your interpretation of the universe!

Mike Shulman (Jul 08 2025 at 17:09):

You can try to define a model in some category other than Set that contains only nonempty sets. Maybe that's what you mean by "the intepretation of the universe". But if your definition satisfies the rules of the theory, then your interpretation of $\bot$ will be initial in that category.

Josselin Poiret (Jul 08 2025 at 17:10):

you're saying that the eliminator has to be able to talk about "all types", but no, it only talks about things that are in the interpretation of the universe. This in turn is something that you have control over

Josselin Poiret (Jul 08 2025 at 17:14):

what's your notion of model for a type theory? CwF?

Mike Shulman (Jul 08 2025 at 17:14):

I don't know if you wrote that before my last comment or afterwards, but my reply to it is what I just said: defining the interpretation of the universe means specifying what category you're working in, and whatever that category is, the interpretation of $\bot$ must be initial in it, even if from an "outside" point of view it has an element.

Josselin Poiret (Jul 08 2025 at 17:15):

I think we're talking past each other: when you say it must be initial, you mean that it's initial when "viewed from the inside". But when defining a model, you're defining the interpretation of everyone externally

Mike Shulman (Jul 08 2025 at 17:16):

Being initial is a statement from the outside about some category.

Mike Shulman (Jul 08 2025 at 17:17):

In case this is the confusion, it's true that even semantically there can be a distinction between strict equality (which interprets definitional equality) and homotopy equality (which interprets propositional equality). That usually only starts to matter when you're doing homotopy type theory, but some unusual models could have different equalities even if you don't have homotopy theory in mind. However, in that case the universal property I'm talking about is relative to the homotopy equality, that is relative to the (perhaps $\infty$-)category that the model describes.

Josselin Poiret (Jul 08 2025 at 17:17):

sure, but it's only initial in a category that has "syntactical" flavor: its objects are closed types, morphisms are functions quotiented by propositional proofs of equality

Mike Shulman (Jul 08 2025 at 17:18):

No!

Mike Shulman said:

A "model" has to satisfy all the rules of the theory. In a model of the theory of groups, you have to be able to multiply any two elements, not just any two elements that are "describable using syntax".

Josselin Poiret (Jul 08 2025 at 17:18):

So what's your notion of model? CwFs?

Mike Shulman (Jul 08 2025 at 17:19):

Sure, say a CwF.

Mike Shulman (Jul 08 2025 at 17:20):

Of course, the underlying category of contexts involves "strict equality", so the relevant notion of "initial" is in the category "presented" by this category and the identity types.

Josselin Poiret (Jul 08 2025 at 17:22):

then the trivial CwF if i'm not mistaken gives you a model where the interpretation of the empty type in the empty context is semantically inhabited

Josselin Poiret (Jul 08 2025 at 17:23):

you just interpret the base category as 1, the Ty family as 1 and the Tm family as ... also 1. You should be able to interpret the eliminator of ⊥ in there without any issues

Mike Shulman (Jul 08 2025 at 17:24):

The unique object of the trivial category is initial.

Mike Shulman (Jul 08 2025 at 17:24):

(as well as terminal)

Josselin Poiret (Jul 08 2025 at 17:25):

right, but that doesn't constrain its semantic inhabitants, right?

Mike Shulman (Jul 08 2025 at 17:25):

Mike Shulman said:

whatever that category is, the interpretation of $\bot$ must be initial in it, even if from an "outside" point of view it has an element.

Josselin Poiret (Jul 08 2025 at 17:26):

Mike Shulman said:

It's interesting that there are multiple ways to construct a universe semantically. That isn't the case for any other type constructors that I know of, because they all have a universal property and hence are uniquely determined up to isomorphism.

Here, you say that to construct semantics for a type theory, all other type formers are completely constrained by their universal properties. I'm arguing that there is freedom when choosing semantic inhabitants of positive types, as opposed to negative types

Mike Shulman (Jul 08 2025 at 17:27):

There are lots of "trivial categories". There's a trivial category where the unique object is the empty set. There's a trivial category where the unique object is a 923-element set. There's a trivial category where the unique object is the real numbers. But what matters categorically is the structure of the category, and saying that an object is initial is a statement only about the structure of the category. It has nothing to do with what the "elements" of that object are in some set-theoretic sense, only about how it is related to other objects of the category by morphisms.

Josselin Poiret (Jul 08 2025 at 17:28):

type theories aren't completely reducible to their category of contexts, there is extra structure on top

Mike Shulman (Jul 08 2025 at 17:28):

What do you mean by "semantic inhabitants"?

Mike Shulman (Jul 08 2025 at 17:28):

In CwF-language, do you mean elements of $\mathrm{Tm}(\Gamma.A)$?

Josselin Poiret (Jul 08 2025 at 17:28):

it's getting late here but I'll be happy to continue this conversation tomorrow

Josselin Poiret (Jul 08 2025 at 17:28):

Mike Shulman said:

In CwF-language, do you mean elements of $\mathrm{Tm}(\Gamma.A)$?

yes

Mike Shulman (Jul 08 2025 at 17:29):

Okay. I was not making any claim about that.

Mike Shulman (Jul 08 2025 at 17:29):

What I was claiming is that the interpretation of $\bot$ is an initial object of the category of types, which determines it up to isomorphism in that category.

Mike Shulman (Jul 08 2025 at 17:29):

Josselin Poiret said:

it's getting late here but I'll be happy to continue this conversation tomorrow

Okay, good night!

Josselin Poiret (Jul 08 2025 at 17:30):

this is the only meaning I can assign to "semantics" in our case, up to any other equivalent notion of model like natural models

Mike Shulman (Jul 08 2025 at 17:37):

It might be the case in some model that $\mathrm{Tm}(\Gamma.A)$ is nonempty even if $A$ is initial. But in that case, $\mathrm{Tm}(\Gamma.B)$ would also be nonempty for any other initial object $B$ since we would have $A\cong B$. I was not making any claim about $\mathrm{Tm}(\Gamma.A)$ being determined in any "absolute" sense, only that once you fix a model, the interpretation of any given type, including a positive type, is fixed up to isomorphism by its universal property, including the value of $\mathrm{Tm}(\Gamma.A)$ in that model (which might, of course, be different from its value in some other model).

Notification Bot (Jul 08 2025 at 17:41):

36 messages were moved here from #learning: questions > Continuations, parametricity, and polymorphism by Mike Shulman.

Josselin Poiret (Jul 09 2025 at 08:44):

but the notion of isomorphism here is internal as well, i.e. you care about having an inhabitant of $\mathrm{Tm}(ε.f\,\text{is an isomorphism})$, for $f : \mathrm{Tm}(ε.A→B)$, no?

Josselin Poiret (Jul 09 2025 at 08:46):

we agree with each other i think, just not with how to intuitively interpret

Mike Shulman said:

It's interesting that there are multiple ways to construct a universe semantically. That isn't the case for any other type constructors that I know of, because they all have a universal property and hence are uniquely determined up to isomorphism.

Josselin Poiret (Jul 09 2025 at 08:50):

my intuition was more from an "implementer" side, where when making normalization models, you have some choice in how you implement positives (even though from the internal pov all the choices are equivalent (but that fact hinges on precisely what kind of semantic equality you choose))

Mike Shulman (Jul 09 2025 at 14:58):

Josselin Poiret said:

but the notion of isomorphism here is internal as well, i.e. you care about having an inhabitant of $\mathrm{Tm}(ε.f\,\text{is an isomorphism})$, for $f : \mathrm{Tm}(ε.A→B)$, no?

You could say that, sure, but by $\beta\eta$ that's equivalent to having a context iso $(x:A) \cong (y:B)$.

Mike Shulman (Jul 09 2025 at 14:59):

Josselin Poiret said:

you have some choice in how you implement positives (even though from the internal pov all the choices are equivalent (but that fact hinges on precisely what kind of semantic equality you choose))

So is this the point then?

Mike Shulman said:

In case this is the confusion, it's true that even semantically there can be a distinction between strict equality (which interprets definitional equality) and homotopy equality (which interprets propositional equality). That usually only starts to matter when you're doing homotopy type theory, but some unusual models could have different equalities even if you don't have homotopy theory in mind. However, in that case the universal property I'm talking about is relative to the homotopy equality, that is relative to the (perhaps $\infty$-)category that the model describes.

Mike Shulman (Jul 09 2025 at 16:33):

Anyway, whether or not you agree with that phrasing of it, I think your statement that "from the internal pov all the choices are equivalent" is sufficient for my point. All I was saying is that universes are different from other type formers, because for universes there are multiple choices that are not equivalent even from the internal pov.