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: Categorical semantics of this dependent type

Bruno Gavranović (Jan 18 2024 at 22:07):

It's known that a dependent function type can be modeled as a morphism in the slice from the identity map. That is, the set of dependent functions $\Pi (a :A).X(a)$ in $\mathbf{Set}$ is isomorphic to the set of morphisms $\mathbf{Set}/A(\text{id}_A, \pi_A)$, (where $\pi_A : \Sigma (a :A).X(a) \to A$ is the projection). This allows us to move away from $\mathbf{Set}$ and state this in an arbitrary category $\mathcal{C}$.

It's also known that a dependent pair type is modeled simply as an object in the slice category. That is, $\Sigma (a :A).X(a)$, together with the above projection, is simply an object of $\mathbf{Set}/A$.

But how do I state the following set --- a combination of these --- in an arbitrary category?

$$\Pi (a :A) . \Sigma (b :B) . R(a, b)$$

I imagine this should be a morphism in the slice over $A$, but I'm getting confused since at the end I'm producing something over $B$. But it also can't be a map in slice over $A \times B$ since that would imply we're universally quantifying over $(b:B)$.

Mike Shulman (Jan 18 2024 at 23:11):

Your description of $\Pi$- and $\Sigma$-types is a bit confused, which I think is what's producing your confusion about combining them. E.g. while "the set of morphisms from the identity in a slice category" can be stated in any category, it itself is only ever a set, whereas a $\Pi$-type in a category $C$ should also be a thing in $C$.

Mike Shulman (Jan 18 2024 at 23:12):

A better way to think about it is that $\Sigma(a:A)$ and $\Pi(a:A)$ are, respectively, left and right adjoints to pullback from $C$ to the slice $C/A$. Or, more generally, from one slice $C/\Gamma$ to another $C/A$, where $A$ is given as an object of $C/\Gamma$ (and type-theoretically we would tend to write something like $\Gamma.A$ instead of $A$, to indicate that it's a "context extension").

Mike Shulman (Jan 18 2024 at 23:14):

The reason $\Sigma$ "is" an object of a slice category is that the left adjoint $\Sigma : C/A \to C$ just forgets the map to $A$, remembering only its domain.

Mike Shulman (Jan 18 2024 at 23:14):

So if $A$ and $B$ are both objects of $C$ (i.e. neither depends on the other), then $R(a,b)$ would denote an object of the double slice $C/(A\times B)$, and $\Pi(a:A).\Sigma(b:B).R(a,b)$ would mean to first apply the left adjoint on $B$, that is forgetting the map to $B$, or equivalently composing the map $R\to A\times B$ with the projection $A\times B \to A$, and then apply the right adjoint $\Pi : C/A \to C$.

Dylan Braithwaite (Jan 18 2024 at 23:18):

I think the 'proper' way to think about this is using contexts. That is, where a type $\Gamma \vdash T$ corresponds with an object of the slice category $\mathcal C / \Gamma$.

The sigma and pi type formers then correspond to functors between the slice categories: if $\Gamma, x : T \vdash U(x)$ corresponds with an object $(U, p) \in \mathcal C/(\Gamma \times T)$ then the sigma-type $\Gamma \vdash \Sigma(x : T) U(x)$ corresponds with the object $\Sigma_T U \in \mathcal C/\Gamma$ defined by $U \xrightarrow{p} \Gamma \times T \xrightarrow{\pi_\Gamma} \Gamma$.

Similarly, if $\mathcal C$ is locally cartesian closed then you get a functor $\Pi_T : \mathcal C / (\Gamma \times T) \to \mathcal C / \Gamma$.

So for the expression you've written you start with something $a : A, b : B \vdash R(a, b)$ which is interpreted as an object of $\mathcal C/(A \times B)$, then $a : A \vdash \Sigma (b : B) . R(a, b)$ is an object of $\mathcal C/A$ and $\vdash \Pi(a : A) . \Sigma (b : B) . R(a, b)$ is an object of $\mathcal C/1$.

(Mikes message came in just as I finished typing this, but I'll send it anyway, in case it helps to have the same thing written two ways)

Dylan Braithwaite (Jan 18 2024 at 23:42):

Also, you can see where the expression you have (for the set of dependent functions) comes from, using the adjunction between $\Pi_A$ and the pullback functor $!_A^* : \mathcal C \to \mathcal C/A$. (I'm writing $!_A$ to mean the terminal map $A \to 1$).

$!_A^* \dashv \Pi_A$ means that $\mathcal C(1, \Pi_A X) \cong \mathcal C/A(!_A^*(1), X)$, and $!_A^*(1) = \mathrm{id}_A$, so points of $\Pi_A X$ are equivalently elements of $\mathcal C/A(\mathrm{id}_A, X)$.

Bruno Gavranović (Jan 19 2024 at 16:05):

Thanks for the answers. Let me check if I understand what you mean.

It sounds like you're suggesting I should make a distinction between

• $(a :A) \vdash A'(a)$, which is an object $(\Sigma (a : A) . A'(A), \pi)$ of $\mathbf{Set}/A$, and
• $\vdash \Sigma (a :A) . A'(A)$, which is the image of that object under $\Sigma_{!} : \mathbf{Set}/A \to \mathbf{Set}/1$

You seem to be suggesting that I should call only the latter a sigma type (is that what you're suggesting?).
Now, I understand the idea of interpreting the latter as a term in a trivial context where the original $(a:A)$ is now existentially quantified. But I'm confused by the fact that: a) now this term is not 'over' anything. The whole thing about categorical semantics of dependent types is that we think of things being over one another, no?, and b) in the former, $(a:A)$ also appears existentially quantified (in $(\Sigma (a : A) . A'(A), \pi)$). If this is not to be thought of as a sigma type, then what is this?

Dylan Braithwaite (Jan 19 2024 at 16:34):

Bruno Gavranović said:

The whole thing about categorical semantics of dependent types is that we think of things being over one another, no?

Yes, but the thing that we think of types being over is contexts. $\Gamma \vdash T$ is a type defined over $\Gamma$ and that's reflected in the way it's interpreted as an object of the fibre over $\Gamma$. The sigma type moves this 'overness' into the object, so that we can talk about closed types which are still dependent. It would be a bit weird if we couldn't give semantics to an arbitrary type $\cdot \vdash T$ without first looking inside $T$ to decide which category it belongs in.

It's a similar situation to the use of exponentials in the semantics of simple type theory. You could say the whole thing about categorical semantics of simple types is that we can think of types as morphisms with a domain and codomain, but we still interpret function types as an object of a CCC rather than a morphism, because without that we can't talk about higher order functions. You run into the same thing with the semantics of dependent types because you can't talk about "higher order" dependent types without internalising some of information about the dependence into the object.

Dylan Braithwaite (Jan 19 2024 at 16:45):

Bruno Gavranović said:

in the former, $(a:A)$ also appears existentially quantified (in $(\Sigma (a : A) . A'(A), \pi)$). If this is not to be thought of as a sigma type, then what is this?

In the first bullet point you're using the sigma to describe an object of $\mathbf{Set}$ whereas in the second you're using the sigma to describe a type in the type theory so these are different situations. But all the same, even in writing that, you have run into a reason why sigma-types should be interpreted in that way, maybe without realising it.

To describe an object of $\mathcal C/A$ you must give an object $X$ of $\mathcal C$ and a morphism $X \to A$. You did this by giving an object $\Sigma(a : A) . A'(A)$, but if sigma-types were to be interpreted as an object of $\mathcal C/A$ then this wouldn't type-check, because you gave an object of the wrong category!

Mike Shulman (Jan 19 2024 at 17:33):

In case saying the same thing in different words helps:

Bruno Gavranović said:

You seem to be suggesting that I should call only the latter a sigma type (is that what you're suggesting?).

Yes.

Now, I understand the idea of interpreting the latter as a term in a trivial context where the original $(a:A)$ is now existentially quantified. But I'm confused by the fact that: a) now this term is not 'over' anything.

What it's "over" syntactically is the empty context, which category-theoretically corresponds to the terminal object. It just so happens that the slice category over the terminal object is equivalent to the category itself, $C/1\simeq C$.

b) in the former, $(a:A)$ also appears existentially quantified (in $(\Sigma (a : A) . A'(A), \pi)$). If this is not to be thought of as a sigma type, then what is this?

The Sigma-type is the object $\Sigma (a : A) . A'(a)$ (or, more precisely, that object paired with its unique map to the terminal object). The pair $(\Sigma (a : A) . A'(a), \pi)$ is not a Sigma-type. It "contains within it" the data of the Sigma-type, but the operation of "taking the Sigma-type" is the operation of forgetting the morphism $\pi$ (or, more precisely, composing it with the unique morphism $A\to 1$).

Mike Shulman (Jan 19 2024 at 17:34):

You might also find it helpful to read about some [[categorical models of dependent types]], which distinguish more carefully between "types in a context" and "objects of a slice category". Many category-theorists find it more intuitive to blur that line, but it sounds like maybe this blurring is part of what's causing your confusion and looking at a more precise treatment would help.

Kevin Arlin (Jan 19 2024 at 17:53):

Second that motion. I found it all much too floppy to understand till I read about categories with families, which actually distinguish between contexts, types and terms in the semantics.