2
$\begingroup$

Here's another question about the formalities of Riehl and Shulman's A type theory for synthetic $\infty$-categories, and in particular about the role that "shapes" play in this type theory. In Prop 5.9, where the authors prove associativity of concatenation in Segal types, they give a few "maps" between shapes. For instance, along the lines of earlier comments in the paper, they write "$\Delta^1\times\Delta^1\simeq\Delta^2\cup_{\Delta^1_1}\Delta^2$", and later they assert "$\lambda(t_1, t_2, t_3).((t_1, t_3), t_2):\Delta^3\rightarrow\Delta^2\times\mathbb{2}$", etc. Now, as I understand the formal deduction rules of the type theory, shapes are not types, and there is no way to make a judgement that a particular term is "of the type" of a particular shape; in particular, I believe the only types that involve a shape are built up from extension types with the shape as a domain. So for instance there are no function types with a shape as a codomain, and hence I assumed that the statements above were just shorthand for the comparable statements about maps out of the shapes in question.

IE, I read the first as shorthand for "for all types $A$, $(\Delta^1\times\Delta^1\rightarrow A)\simeq(\Delta^2\cup_{\Delta^1_1}\Delta^2\rightarrow A)$", and the second as "for all types $A$, $\lambda f.\lambda(t_1, t_2, t_3).f((t_1, t_3), t_2):(\Delta^2\times\mathbb{2}\rightarrow A)\rightarrow(\Delta^3\rightarrow A)$". Indeed these statements are easy to verify and are all that one needs for the proof.

However, some statements later in the paper make me question my interpretation. In particular, in proposition 5.21, where the authors prove that the shape inclusion of $\Lambda^3_2$ into $\Delta^3$ is inner anodyne, they mention that – if minimum and maximum operators were included as part of the data of the cube $\mathbb{2}$ – one could prove that "$\Lambda^3_2\rightarrow\Delta^3$ is literally a retract of $X\rightarrow\Delta^3\times\Delta^2$" (emphasis mine).

The issue is that, in light of the comments in my first paragraph, I don't really understand how to parse this statement if it's meant to be taken literally or formally; the intuitive meaning (that function types out of $\Delta^3$ with a given restriction to $\Lambda^3_2$ are retracts of function types out of $\Delta^2$ with a corresponding restriction to $X$) makes sense in the type theory, and is what the authors go on to prove. But how can we make any formal assertions about a shape (or in this case a shape inclusion) being a retract of another when the type theory does not give a way of defining maps into shapes?

What am I missing here? It seems to me also that if that latter assertion can be understood formally in the type theory then the assertions that I quoted in my first paragraph also can be; is this the case as well or is there some difference between the two statements?

$\endgroup$

1 Answer 1

2
$\begingroup$

It's meant at the level of the tope theory. A morphism between shapes is a morphism of cubes together with an implication of topes. We could formalize this with a notion of "term in a shape" analogous to eq. (2.1), but in general there's no need.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.