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: theory: type theory

Topic: Displayed Type Theory

Astra Kolomatskaia (Dec 01 2023 at 02:51):

A new paper of mine, joint with @Mike Shulman, just went live on the arxiv!

It may be accessed here: https://arxiv.org/abs/2311.18781

We construct a new type theory in which it is possible to coinductively construct semi-simplicial types in full semantic generality. In particular, the discrete mode of our theory has semantics in any CwF with pi-types, universes, and ω-limits; any ∞-topos model will satisfy these properties. We accomplish this through a syntactic primitive called display, which is, in semantics, the fibrant counterpart of décalage on augmented semi-simplicial diagrams.

I am opening this thread to start a discussion on our results! :smile:

Chris Grossack (they/them) (Dec 01 2023 at 04:48):

Congrats! ^_^

Christian Williams (Dec 08 2023 at 00:29):

Wow, this is amazing! I need to read the whole paper soon; the intro is extremely clear and insightful.

Julius Hamilton (Jun 09 2024 at 17:41):

I want to read this but probably don’t know enough about type theory yet.

Mike Shulman (Jun 09 2024 at 19:05):

You could try the blog posts instead: part 1, part 2.

Julius Hamilton (Jun 09 2024 at 22:46):

DB9CAC0B-C177-4908-82DD-7E0925709489.png

To explain the problem of defining semi-simplicial types, we start with a classical perspective grounded first in set theory and later in homotopy theory.

A semi-simplicial set is defined to consist of sets $X_n$ for $n \geq 0$, along with face maps $\delta_k : X_n \to X_{n-1}$, for $k \in \{0,…,n\}$…

So for a specific value $n \geq 0$, a “semi-simplicial set” $S$ is a set of $n + 1$ sets, $\{X_i | 0 \leq i \leq n\}$, with $n + 1$ maps $\delta_k : X_n \to X_{n - 1}$ for $0 \leq k \leq n$. You only need the face maps between the final set in $S$, $X_n$, and the penultimate set, $X_{n-1}$ - not between every pair of consecutive sets?

satisfying the relations:

$\delta_k \circ \delta_l = \delta_{l-1} \circ \delta_k$

How can they compose with each other if all the face maps have the same domain and codomain as each other?

Or is it supposed to say $X_k \to X_{k-1}$?

Astra Kolomatskaia (Jun 10 2024 at 01:45):

There is a hidden implicit index on the face maps

Astra Kolomatskaia (Jun 10 2024 at 01:46):

The maps are really $\delta_{n,k} : X_n \to X_{n-1}$, but we thought that it was acceptable abuse of notation to infer that from context

Julius Hamilton (Jun 10 2024 at 03:54):

Alright. I’ll try to understand the definition from Wikipedia.

0023537D-7ED1-458B-9C63-1AAAC55392BE.png

A semi-simplicial set or $\Delta$-set is a sequence of sets $\{S_n\}_{n=0}^{\infty}$, and for each $n$, there are maps $\delta_i^n$ for $0 \leq i \leq n + 1$. So, if $n = 5$, there exists $\delta_0^5, \delta_1^5, …, \delta_6^5$, which are all maps $S_6 \to S_5$. In other words, it’s just a sequence of a decreasing number of maps:

4B890583-1DF5-482B-9757-BC33083B2848.jpg

The maps must conform to this condition:

$d_i^n \circ d_j^{n+1}$ (…)

This is any of the maps between $S_{n+2}$ and $S_{n+1}$, followed by any of the maps between $S_{n+1}$ and $S_n$:

$$\begin{CD} S_{n+2} @>j>> S_{n+1} @>i>> S_n \end{CD}$$

…$= d_{j-1}^n \circ d_i^{n+1}$

Which is the map between $S_{n+1}$ and $S_n$ whose index is one less than $j$, after the map between $S_{n+2}$ and $S_{n+1}$.

$$\begin{CD} S_{n+2} @>i>> S_{n+1} @>j-1>> S_n \end{CD}$$

That is, while both these pairs of composed maps are between the same two sets, there is a correspondence between the indices: $j$, then $i$, must be the same as $i$, then $j-1$. I have yet to understand the significance of this condition.

Julius Hamilton (Jun 10 2024 at 04:06):

AB6CF282-9DAE-4ED2-A2FA-2E9164C00627.jpg

Here we see the maps with indices. According to the condition, map 4 from $S_4$ to $S_3$, followed by map 2 from $S_3$ to $S_2$, must be equal to map 2 from the former, followed by map 3 from the latter.

We can write other such corresponding map pairs:

3 then 0 must equal 0 then 2

4 then 3 must equal 3 then 3 (?)

I still don’t grasp what this condition is implying.

Julius Hamilton (Jun 10 2024 at 10:56):

I’ll read this, anyway. https://math.jhu.edu/~eriehl/ssets.pdf

David Michael Roberts (Jun 10 2024 at 11:20):

Draw a tetrahedron with vertices labelled 0,1,2,3, (directed) edges labelled 01, 12, 23, 13, 02, 03, faces labelled by triples of increasing numbers (eg 013), and the volume by 0123. the map $$d_i$: S_3 \to S_2$ acts on one of these to throw away the number $i$ from 0123 and give a face.

Now each face, labelled $ijk$ with $j<k<\ell$ is order-isomorphic to 012. Then the maps $d_i\colon S_2 \to S_1$ throw away the index $j,k$ or $\ell$ corresponding to the element $i\in \{0,1,2\}$ under this isomorphism. So, for instance, in 013 the function $d_2$ throws out the 3 (as under $013 \simeq 012$ 3 corresponds to 2) to give 01. And $d_1$ throws out the 1 to give 03.

It's best if you actually draw a big picture of the tetrahedron and label things. And you can see that from the volume, you can get to each edge by two different compositions of face maps. For instance, you can do 0123 -> 023 -> 02, or 0123 -> 012 -> 02, and this corresponds to one of the simplicial identities.

You can do the same going down a dimension, starting with a triangle instead, namely 012, and looking at how to get to vertices. You can do eg 012 -> 01 -> 1 or 012 -> 12 -> 1.

Astra Kolomatskaia (Jun 10 2024 at 14:36):

David gave a good illustration. The only reason that I talk about the fibred formulation of SSTs in the blog post is because that is the way that the problem has traditionally phrased, and as it allows me to discuss coherence issues. My preferred definition of SSTs in the indexed one.

In the fibred definition, for example, all of the lines are put together in a single set [or space]. In the indexed definition, in contrast, there is a family of lines indexed by their two endpoints. So for points $x$ and $y$, there is a space of lines $A_1~x~y$. Triangles are then indexed by three points and three lines.

Here are the first few simplex types:

Astra Kolomatskaia (Jun 10 2024 at 14:36):

Screenshot-2024-06-10-at-10.35.27-AM.png

Astra Kolomatskaia (Jun 10 2024 at 14:37):

In the indexed formulation, the face maps don't really exist as data, but rather just correspond to index lookup.

Astra Kolomatskaia (Jun 10 2024 at 14:37):

I think that the indexed formulation makes it clear that a SST is just a notion of points, a notion of lines, a notion of triangles, etc.

Astra Kolomatskaia (Jun 10 2024 at 14:39):

In the first blog post, I sketch an equivalence between the fibred and indexed formulations, up to level two. In order to continue this equivalence, one would have to use higher coherences in the fibred formulation.

Astra Kolomatskaia (Jun 10 2024 at 15:09):

Oh, also here is a talk recording of mine on dTT:
https://www.youtube.com/watch?v=vLCvrXJDPys