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: semisimplicial types

Tim Campion (May 09 2021 at 17:43):

Every so often I find myself revisiting the question of how to define semisimplicial types in HoTT. Every time, I come to the conclusion that I don't understand type theory well enough to judge whether I'm getting anywhere, or whether I'm missing the point. Here's my latest attempt. This attempt does not attempt to define semisimplicial types in such a way as to have a bunch of nice judgmental equalities to work with -- it would probably be very cumbersome to actually use. But my hope is that it would at any rate be a definition which (1) is syntactically well-formed and (2) upon interpretation in the standard model in simplicial sets actually gives the correct notion (and in particular gets all the higher coherences right). It's still a sketch, and probably the main issue is that some step or other will just have all the same problems as any other approach, but here goes:

The idea is to define, by mutual induction on $n: \mathbb N$, the following concepts:
1.) The notion of an $n$-truncated semisimplicial type
2.) The notion of a presheaf on an $n$-truncated semisimplicial type
3.) The space of natural transformations $Nat_n(-,-)$ between presheaves on an $n$-truncated semisimplicial type

Here, a presheaf on an n-truncated semisimplicial type S is to be thought of as the "the same" as a presheaf on the "Segalic replacement" of S (which we avoid defining directly). For example, the terminal category $\Delta^{inj}_{\leq [0]}$ is a $0$-truncated semisimplicial type (as is any discrete category). The site for graphs $\Delta^{inj}_{\leq [1]}$ is a $1$-truncated semisimplicial type (as is any free category, up to Segalic replacement). More generally, $\Delta^{inj}_{\leq [n]}$, the site for $n$-truncated semisimplicial types, is itself an $n$-truncated semisimplicial type. This, along with the "Reedy construction" which Mike Shulman has written about, which allows one to construct $\Delta^{inj}_{\leq [n]}$ from $\Delta^{inj}_{\leq [n-1]}$ in an inductive manner, is what is supposed to make the construction tick.

So the idea would be as follows. The base case $n=0$ is clear (maybe one could even start at $n=-1$, whatever). Given notions 1,2,3 for $n-1$, we define them for $n$ as follows. We define the $n-1$-truncated semisimplicial set $\partial \Delta[n]$ by $[i] \mapsto Inj(i+1,n+1)$ "in the usual way" (using definition (2) for $n-1$). We define, for an $n-1$-truncated semisimplicial type, the $n$-matching object by $M_n X = Nat_{n-1}(\partial \Delta[n], X)$ using (3) for $n-1$. We define an $n$-truncated semisimplicial type $sk^n X$ to comprise an $n-1$-truncated semisimplicial type $sk^{n-1} X$, a type $X_n$,and a map $X_n \to M_{n} sk^{n-1} X$. I'm a little hazy on how to now complete the induction for (2) and (3), but perhaps this issue is not insurmountable?

Or would such an approach, even if it works, "miss the point" in some sense? I'm thinking that a definition of the above form would allow one to take a limit over $n$ and arrive at a notion of "semisimplicial type". But perhaps I'm mistaken, and it would be no easier to do this than with any other definition of "$n$-truncated semisimplicial type".

Ulrik Buchholtz (May 09 2021 at 18:58):

I hope that something like this works, but so far no-one has been able to get all the pieces to line up to complete the definition.
In particular, when you define the transformations in the inductive step, you'll need the 2-cells of transformations in the previous step, so you'll actually need to define the k-cells for all k, interleaved with the inductive procedure, I think.

Mike Shulman (May 09 2021 at 21:06):

If you can make it work, that would be great, but people have tried a lot of different variations on ideas like this, and so far they always end up in some sort of infinite regress.

Tim Campion (May 09 2021 at 22:13):

Thanks, both of you! I've had ideas about this before which turned out to be totally wrong-headed when I explained them to somebody knowing more type theory than me, so it's gratifying to hear that at least this approach is not crazy, and in fact something which people have tried!

Tim Campion (May 10 2021 at 08:18):

Here goes. Define the following by induction on $a: \mathbb N$:

• An "$a$-truncated semisimplicial type" $X : ST(a)$ comprises $X_a: Type$, $X_{<a}: ST(a-1)$, and $\mu_X : Nat_{a-1}(sk^{a-1} \Delta[a] \times X_a, X_{<a})$ (base case: $ST(-1) = 1$);
• Given $X,Y: ST(a)$, a "map" $f: Nat_a(X,Y)$ comprises $f_a: X_a \to Y_a$, $f_{<a}: Nat_{a-1}(X_{<a}, Y_{<a})$, and an equality $f_{<a} \circ \mu_X = \mu_Y \circ (id \times f_a): Nat_{a-1}(sk^{a-1} \Delta[a] \times X_a, Y_{<a})$ (base case is trivial);
• Composition $\circ: Nat_a(X,Y) \times Nat_a(Y,Z) \to Nat_a(X,Z)$ is defined in the obvious way. So is the product operation $\times : ST(a) \times Type \to ST(a)$ and its extension to morphisms.

Tim Campion (May 10 2021 at 08:18):

To complete the induction, it remains only to define $sk^a\Delta[a+1]: ST(a)$. This is a bit more involved. First we define, for $a \leq b: \mathbb N$ the following:

• $\Delta[b]_a : Type$ is defined to be $IO(a+1,b+1)$, and $\psi_{a,b,c}: \Delta[b]_a \times \Delta[c]_b \to \Delta[c]_a$ is defined to be composition;
  Here "$IO$" stands for "injective order-preserving maps", and $a+1,b+1$ are the appropriate finite ordinals.

Now we define, by induction on $a \leq b \leq c \leq d : \mathbb N$, the following data:

• $sk^a \Delta[b]: ST(a)$;
• $\phi_{a,b,c}: Nat_a(sk^a \Delta[b] \times \Delta[c]_b,sk^a \Delta[c])$;
• We require that $\phi_{a,c,d} \circ (\phi_{a,b,c} \times id) = \phi_{a,b,d} \circ (id \times \psi_{b,c,d}): Nat_a(sk^a \Delta[b] \times \Delta[c]_b \times \Delta[d]_c, sk^a \Delta[d])$;

Tim Campion (May 10 2021 at 08:18):

This data is defined inductively as follows:

• If $a = -1$, there is nothing to define for $sk^a \Delta[b]$. Otherwise, define $(sk^a \Delta[b])_a = \Delta[b]_a$, $(sk^a \Delta[b])_{<a} = sk^{a-1} \Delta[b]$, and $\mu_{sk^a \Delta[b]} = \phi_{a-1,a,b}: Nat_{a-1}(sk^{a-1} \Delta[a] \times \Delta[b]_a, sk^{a-1} \Delta[b]$);
• If $a = -1$, there is nothing to define for $\phi_{a,b,c}$. Otherwise, define $(\phi_{a,b,c})_a = \psi_{a,b,c}: \Delta[b]_a \times \Delta[c]_b \to \Delta[c]_a$; Define $(\phi_{a,b,c})_{<a} = \phi_{a-1,b,c}: Nat_{a-1}(sk^{a-1} \Delta[b] \times \Delta[c]_b, sk^{a-1} \Delta[c])$. This yields $\phi_{a,b,c}: Nat_a (sk^a \Delta[b] \times \Delta[c]_b, sk^a \Delta[c])$ because $\phi_{a-1,b,c} \circ (\phi_{a-1,a,b} \times id) = \phi_{a-1,a,c} \circ (id \times \psi_{a,b,c})$ by induction on $a$;
• If $a = -1$, there is nothing to verify for the posited equation. Otherwise, it suffices (EDIT: in view of the "discreteness" property added to the induction below, thanks to @Reid Barton ) to verify that $(\phi_{a,c,d} \circ (\phi_{a,b,c} \times id))_a = (\phi_{a,b,d} \circ (id \times \psi_{b,c,d}))_a$ and $(\phi_{a,c,d} \circ (\phi_{a,b,c} \times id))_{<a} = (\phi_{a,b,d} \circ (id \times \psi_{b,c,d}))_{<a}$; the former equation reduces to $\psi_{a,c,d} \circ (\psi_{a,b,c} \times id) = \psi_{a,b,d} \circ (id \times \psi_{b,c,d})$, which is just associativity of composition in the category $IO$ of finite ordinals and injective order-preserving maps; the latter equation just says that $\phi_{a-1,c,d} \circ (\phi_{a-1,b,c} \times id) = \phi_{a-1,b,d} \circ (id \times \psi_{b,c,d})$, which holds by induction on $a$.

This completes the induction. We now have a type $ST(a)$ of $a$-truncated semisimplicial types for each $a: \mathbb N$, and we transparently have forgetful maps $ST(a) \to ST(a-1)$ for each $a$ as well. We may pass to the limit to obtain a type $ST$ of semisimplicial types.

Reid Barton (May 10 2021 at 11:09):

In the very last bullet point, you also need to check that the equality components of the two "map"s are equal (after identifying the data components). But maybe you can simultaneously prove that "map"s into a skeleton form a 0-type?

Reid Barton (May 10 2021 at 11:23):

(By "skeleton" I meant one of these objects $sk^a \Delta[b]$.)

Tim Campion (May 10 2021 at 12:09):

Reid Barton said:

In the very last bullet point, you also need to check that the equality components of the two "map"s are equal (after identifying the data components). But maybe you can simultaneously prove that "map"s into a skeleton form a 0-type?

Good point. I was wondering if this expected discreteness might actually need to be explicitly checked and used... I think probably the other option -- trying to add this higher equality data to the induction hypothesis -- sounds like something that would lead to an infinite regress, so it does seem best to try instead to inductively show some kind of discreteness and invoke it in the induction.

Actually, I think this is not bad. Add to the induction the following:

• Say that $X: ST(a)$ is discrete if $Nat_a(Y,X)$ is a 0-type for every $Y: ST(a)$;
• Inductively show that if $X_a : Type$ is a 0-type and $X_{<a}: ST(a-1)$ is discrete, then $X: ST(a)$ is discrete;

• Do this as follows: $Nat_a(Y,X)$ is a pullback of $Map(Y_a, X_a)$ and $Nat_{a-1}(Y_{<a},X_{<a})$ over $Nat_{a-1}(something, X_{<a})$ -- so because 0-types are stable under pullback, $Nat_a(Y,X)$ is discrete if these other three types are 0-types; if $X$ is discrete, then $Map(Y_a,X_a)$ is a 0-type because $X_a$ is a 0-type and $Nat_{a-1}(anything, X_{<a})$ is discrete because $X_{<a}$ is discrete, using induction on $a$;

• Conclude that $sk^a \Delta[b]$ is discrete;

• Conclude, as you suggest, Reid, that those two equalities must be equal equalities.

Tim Campion (May 10 2021 at 13:44):

Here's a non-type-theoretic issue: I'm not sure that the tensoring of semisimplicial types with plain types works in the way I'm assuming. The map $\mu_X: Nat_{a-1}(sk^{a-1} \Delta[a] \times X_a \to X_{<a})$ is really an adjointed-over stand-in for a map $X_a \to Nat_{a-1}(sk^{a-1} \Delta[a], X_{<a})$, but maybe it's not so clear what "$\times$" has to be to be this adjoint. What I had in mind was that for $X : ST(a)$ and $Y: Type$, one would have $(X \times Y)_a = X_a \times Y$ and $(X\times Y)_{<a} = X_{<a} \times Y$. This definition would be correct for simplicial types, but I think it's incorrect for semisimplicial types? There are several possible fixes: one might work with everything adjointed back over in the form $X_a \to Nat_{a-1}(sk^{a-1} \Delta[a], X_{<a})$, or one might actually work with simplicial types instead of semisimplicial -- this would require defining latching objects as well as matching objects, but might not actually be that crazy.

Tim Campion (May 10 2021 at 13:56):

Er -- maybe this is okay, actually. $n$-truncated semisimplicial spaces are a presheaf category; they are cartesian closed. The cartesian product really is levelwise (it's just not the "geometric" product). The tensoring with spaces can be constructed from the cartesian product and the tensoring of a space with the terminal object. The terminal object, by definition, has one simplex in each dimension -- again, it's not the "geometric" terminal object, being rather a model of $S^n$ or $\mathbb R\mathbb P^n$ or something, but thats okay. Tensoring with the terminal object is "levelwise", so $1 \times Y$ really has $Y$ for its space of $k$-simplices for each $k \leq n$. Since the cartesian product is levelwise, the "levelwise" formula I gave above for $X \times Y$ is actually correct (It's just not "geometrically correct", but we knew we were getting into such issues by moving to the semisimplicial world).

Tim Campion (May 10 2021 at 13:57):

So I'm back to thinking that this construction works, which still seems too good to be true...

Tim Campion (May 10 2021 at 14:00):

I suppose there's still the question of whether it defines the correct thing -- there are equalities going into the definition which are not submitted to explicit higher coherence conditions, so one might suspect that $ST(n)$ doesn't really give you "sufficiently coherent" "$n$-truncated semisimplicial types"... but I'm very tempted to think that the universality of the Reedy construction at the heart of the construction might just mean that this really is what one wants...

Tim Campion (May 10 2021 at 16:07):

I suppose in the equation which is inductively satisfied by the $\phi$'s and $\psi$'s, I am implicitly coercing across an "associativity" isomorphism for $\times$, which says that if $X: ST(a)$ and $Y,Z: Type$, then $(X \times Y ) \times Z = X \times (Y \times Z)$. This looks very routine to prove by induction as soon as one makes explicit the definition of $X \times Y$.

Mike Shulman (May 10 2021 at 16:52):

My recommendation is to try to formalize it in a proof assistant. That way you'll find out for sure whether it works, and if it does you'll have a much easier time convincing other people of it.

Tim Campion (May 10 2021 at 19:42):

The number of times I have tried and failed to install Coq and get the HoTT library running on Windows is a sad joke, so unfortunately I don't think I'll be able to even attempt this without buying a new computer. Then I would still need to address my incompetence at Coq. So if anybody else happens to have the energy / wherewithal to try out formalizing the above defintion, I'd be interested to hear how it goes.

Tim Campion (May 10 2021 at 19:44):

I'd also be interested to hear about other attempts along these lines and where they got stuck, to get a better idea of what the pitfalls here are, so that I could at least try to see whether the above definition actually avoids them.

Tim Campion (May 10 2021 at 19:45):

For such a longstanding and prominent open problem, I imagine somebody out there can say something more precise about what the obstacles are than just "eventually you always seem to encounter an infinite regress".

Tim Campion (May 10 2021 at 19:52):

At the very least, I think the pitfall that Ulrik mentioned seems to be circumvented -- it appears that the only place an equality between equalities is needed is the spot that Reid caught. Since this appearance is isolated in the part of the construction which is specific to the particular types $sk^a \Delta[b]$, which are discrete, it is easily handled. The reason for this lies in the reliance on the "Reedy decomposition" - type description of things. From the sound of things, people have tried such approaches before though, so perhaps there's some commonly-encountered pitfall going on here that I'm missing.

Jake Gillberg (May 10 2021 at 21:58):

Here is Voevodsky's attempt, with some comments on what goes wrong: https://github.com/vladimirias/Foundations/blob/master/Current_work/semisimplicial.v

assert ( e : paths (restrn (pr1 X) n (isreflnatleh n) (S n) k s1 fn) (restr n IHn (pr1 X) n (isreflnatleh n) (S n) j s0 (restrn (pr1 X) n (isreflnatleh n) j k s fn )) ).

(* At this point the goal is to prove a certain equality which asserts "transitivity" or "naturality" of restriction maps. This equlity will be provable as a strict equality in HTS. The proof is by induction and if attempt it for "paths" we get into problems with the need to take into acount transports of increasing complexity with each new induction step. Here we use "admit" . *) admit .

Tim Campion (May 11 2021 at 23:55):

Mike Shulman said:

My recommendation is to try to formalize it in a proof assistant. That way you'll find out for sure whether it works, and if it does you'll have a much easier time convincing other people of it.

I wonder if you (or anyone) could recommend a proof assistant for this? I do seem to finally have Coq running on my computer, but I'm struggling to fit the mutual recursion of the definition into it. I've read that Agda has better support for mutual recursion than Coq does, but I'm worried by the fact that the main HoTT Agda repository I can find https://github.com/HoTT/HoTT-Agda appears to have fallen into a state of neglect, with no updates in 2 years. My understanding is that Lean doesn't support univalence, so even though I don't think the main challenges with implementing this definition will actually be homotopy-theoretic, I suppose a Lean implementation might not be of much interest. The only other proof assistant which I've heard of and which I believe is type-theoretic in nature is Idris, but I don't know much about it.

Mike Shulman (May 12 2021 at 00:32):

While I generally prefer Coq for homotopy-theoretic formalization, for something like this I would reach for Agda without hesitation. As you said, Agda has very powerful mutual "inductive-inductive-recursive" definitions, I believe sometimes even outstripping what's known to make sense semantically. I believe it also has a somewhat more forgiving termination checker than Coq does, and you can even tell it to ignore the termination checker and accept something even though it can't check that it terminates. This is what you want for something like this: you want to formalize something to find out whether it makes any sense at all, and then if it does you can worry later about precisely what it requires of the formal system.

Mike Shulman (May 12 2021 at 00:47):

Since, as you said, the main challenges will probably not be homotopy-theoretic, I wouldn't expect you to need much in the way of a HoTT library. But if you do need more than is in the old HoTT-Agda library, you could try the Cubical Agda library, which is under more active development.

Mike Shulman (May 12 2021 at 00:48):

It's a bit questionable at the moment semantically too, but again, I wouldn't expect any of that to matter to you at this stage.

Ulrik Buchholtz (May 12 2021 at 07:01):

I'd second the recommendation for Agda:

• For something very simple, you can play around in a browser with AgdaPad
• There are “getting started” guides at both readthedocs and at the PLFA book site
• The old HoTT library was ported to 2.6 by Andrew Swan here
• I also second the recommendation for the cubical library
• You might also like the formalization accompanying Egbert Rijke's introductory book.

Nick Hu (May 12 2021 at 13:01):

(As a novice) I would also recommend Agda, but I think cubical is really hard to use (even for someone who knows HoTT, because you are forced to constantly be thinking about the cubes - this is 'the point' I think)

Tim Campion (May 13 2021 at 21:59):

So I've played around with this a bit, and I'm finally convinced that this doesn't work. The above formulation is a bit of a mess, requiring associativity of $\times$ to work, which, as one can imagine, leads to requiring ever-higher coherences as part of the inductive construction in order to inductively prove. One can reconfigure things without using $\times$ (basically "currying/uncurrying" by using a map $X_a \to Nat_{a-1}(sk^{a-1} \Delta[a], X_{<a})$ instead). But then there are similar problems, because you still have to define $Nat_a$, and in order to define it correctly you need to have composition maps $Nat_a(X,Y) \to Nat_a(Y,Z) \to Nat_a(X,Z)$, and in order to inductively construct those you need to know that the composition is associative, and from here one again has a regress to higher and higher coherences which must be inductively constructed. And it doesn't seem to help to use $\prod_{\sigma: Nat_{a-1}(sk^{a-1} \Delta[a], X_{<a})} Type$ instead.

I have a vague sense that one principled way to cart around higher coherence data like this would be to construct, inductively as you go, roughly an $a$-truncated semisimplical type of $b$-truncated semisimplicial types for $b\leq a$. But I haven't gotten a grip on how to define this type, even assuming that the full definition of $ST(a)$ were in place. Moreover, I'm not sure how precisely I would use it if I did have it.

So chalk this up as another case of "this well-known open problem is indeed as hard as people say"!

Mike Shulman (May 14 2021 at 02:23):

I'm not surprised you ran into the same problems that everyone else does. But it's a maddening problem -- there are so many approaches like this that make the infinite regress feel "inessential", and yet no matter how you set it up it seems unavoidable.

Mike Shulman (May 14 2021 at 02:28):

I admit I can't help but feel a thrill of hope every time someone new comes up with a proposal like this, just in case they've spotted something that's eluded everyone else.

Tim Campion (May 14 2021 at 16:32):

Here is a totally different idea, which is not inductive, but rather directly defines the type of simplicial types.

I'm thinking that the issue so far has been that the $\infty$-category $\Delta$ (or $\Delta^{op}$) is 2-coskeletal. So definitions along the above lines, where we map out of $\Delta$, are swimming against the current -- coskeletal things want to be mapped into. So let's use a definition of $Cat_\infty$ which involves mapping into $\Delta^{op}$ rather than out of $\Delta^{op}$. In particular, let's aim for a definition of a simplicial type described as a left fibration over $\Delta^{op}$.

The issue, prima facie, is of course that such a definition would seem to require us to have already defined what an $\infty$-category is. But I think we can get around this. Let $GGraph$ be the type of 2-truncated semsimplicial types, and let $\Delta^{op} : GGraph$ denote the 2-truncated semisimplicial nerve of the 1-category opposite to the simplex category. Define a weak category to be a ggraph $\mathcal E$ satisfying the only Segal condition we can formulate (i.e. that $\mathcal E_2 \to \mathcal E_1 \times_{\mathcal E_0} \mathcal E_1$ is an equivalence) as well as a Rezk completeness condition. Note that $\Delta^{op}$ is a weak category.

If $\mathcal E,\mathcal B$ are weak categories, and $p: \mathcal E \to \mathcal B$ is a map of ggraphs (defined in the obvious way), we can define the notion of a cocartesian lift via the usual pullback square of hom-spaces, and we say that $p$ is a left fibration if cocartesian lifts exist and moreover every morphism of $\mathcal E$ is cocartesian. Then we define a simplicial type to be a left fibration $\mathcal E \to \Delta^{op}$.

There's not really any induction going on here. So I'm hopeful that the above definition can be formulated in HoTT without encountering any kind of infinite regress. So the real question ought to be semantic: if I perform the above construction in the usual model, do I get the correct type? The hard to thing to swallow is that modeling everything with 2-truncated semisimplicial spaces should be adequate. I tentatively think it is adequate, basically because there's a sort of "redundancy" in the data of a left fibration -- so what we're doing here should be thought of as just not worrying about certain redundant information. The first thing to convince oneself of is the following: a weak category $\mathcal E$ has a well-defined "composition of morphisms", which is not in general associative. However, the claim is that if $\mathcal E$ is left-fibered over the 2-nerve of an ordinary 1-category, then the composition operation on $\mathcal E$ is associative. I believe this allows us to uniquely extend such a left fibration of ggraphs to a left fibration of gggraphs, and hopefully inductively on to higher truncated semisimplicial types. Then externally we may pass to the limit and see that we have a unique extension to a left fibration of complete Segal spaces in the usual sense.

Tim Campion (May 14 2021 at 17:04):

Oh -- and it bears mentioning on the semantic side that the forgetful functor from $\infty$-categories to weak categories is fully faithful (or at least it would be if we used 2-truncated simplicial spaces instead of 2-truncated semisimplicial spaces -- I'm not sure how important the units are to the story).

Mike Shulman (May 14 2021 at 17:10):

I'd need to see some details of the semantic side.

Tim Campion (May 14 2021 at 19:27):

Mike Shulman said:

I'd need to see some details of the semantic side.

That is totally fair!

Let me argue that if $\Gamma : \mathcal E \to \mathcal B$ is a left fibration from a weak category to a 1-category, then the composition on $\mathcal E$ is "associative" in some sense. This is meant to be a proof of concept -- hopefully the sense of "associative" is a relevant one, and hopefully this can be extended to higher associativity as well. For now, I will argue the following. There are two maps $\mathcal E([1]) \times_{\mathcal E([0])} \mathcal E([1]) \times_{\mathcal E([0])} \mathcal E([1]) \rightrightarrows \mathcal E([1])$ which one can construct representing 3-fold composition -- one factors through $\mathcal E([2]) \times_{\mathcal E([0])} \mathcal E([1])$ while the other factors through $\mathcal E([1]) \times_{\mathcal E([0])} \mathcal E([2])$. I will argue that these maps are (propositionally) equal.

The notion of "left fibration" of weak categories is maybe still a little bit up in the air, but let's stipulate that $\Gamma : \mathcal E \to \mathcal B$ being a left fibration should at least entail that the canonical map $\mathcal E([1]) \to \mathcal E([0]) \times_{\mathcal B([0])} \mathcal B([1])$ should be an equivalence (note that this statement doesn't require any more than the underlying graph of $\mathcal E$). This implies that the natural maps $\mathcal E_x([1]) \to \mathcal B_{\Gamma x}([1])$ and $\mathcal E_x([1]) \times_{\mathcal E([0])} \mathcal E([1]) \times_{\mathcal E([0])} \mathcal E([1]) \to \mathcal B_{\Gamma x}([1]) \times_{\mathcal B([0])} \mathcal B([1]) \times_{\mathcal B([0])} \mathcal B([1])$ are equivalences (where the subscripts indicate that we have chosen starting points for our morphisms using some $x \in \mathcal E$). In this way the equality of the two maps $\mathcal E_x([1]) \times_{\mathcal E([0])} \mathcal E([1]) \times_{\mathcal E([0])} \mathcal E([1]) \rightrightarrows \mathcal E_x([1])$ may be transposed across these natural maps into a question of equality of two maps $\mathcal B_{\Gamma x}([1]) \times_{\mathcal B([0])} \mathcal B([1]) \times_{\mathcal B([0])} \mathcal B([1]) \rightrightarrows \mathcal B_{\Gamma x}([1])$. And these two maps are known to be equal because $\mathcal B$ is a 1-category, so that its composition is in fact associative.

Tim Campion (May 14 2021 at 19:34):

If you're keeping score at home, I maybe only seemed to use the 1-truncated simplicial structure of $\mathcal E$ above, but in fact the degree 2 part (and the Segal condition) figures into the construction of the two "composition" maps, and the naturality of $\Gamma$ at $[2]$ figures into the naturality of the map which is used to transport the equality we need from $\mathcal B$ to $\mathcal E$.

Mike Shulman (May 14 2021 at 21:25):

Probably I should have been more specific. I don't have so much trouble believing that; what seems less plausible is that you can extend to infinity.

Mike Shulman (May 14 2021 at 21:26):

Tim Campion said:

Oh -- and it bears mentioning on the semantic side that the forgetful functor from $\infty$-categories to weak categories is fully faithful

In particular, can you explain this?

Tim Campion (May 14 2021 at 22:16):

Mike Shulman said:

Probably I should have been more specific. I don't have so much trouble believing that; what seems less plausible is that you can extend to infinity.

I'm not quite sure what you you mean. I agree there's little hope of formulating within HoTT a statement of the form "for all natural numbers $n$, there is a unique extension of $\Gamma : \mathcal E \to \mathcal B$ to a left fibration of $n$-truncated 'weak categories'", because that would presuppose that we could define $n$-truncated semisimplicial types uniformly in $n$ in the first place.

But I do maintain I've made it plausible that for any $n$ for which we care to write down the explicit definition of $n$-truncated semisimplicial types, there should be a theorem in HoTT of the form "there is a unique extension of $\Gamma$ to a left fibration of $n$-truncated 'weak categories'". Perhaps I should expand on why I think this is plausible.

A 2-truncated semisimplicial space like $\mathcal E$ has no way to "record" on its own terms that its composition is in any sense associative -- such witness data is supposed to live in dimension 3. So in order to have a hope of enforcing associativity in $\mathcal E$, the associativity kind of needs to be "imported" from somewhere else. And in fact that's exactly what happens in the above argument -- the left fibration $\mathcal E \to \mathcal B$ is used to "import" associativity from $\mathcal B$. Now that we know that the composition in $\mathcal E$ is associative, it's very plausible to me that we can extend $\mathcal E$ to a 3-truncated semisimplicial space, which will again be left fibered over the 3-truncated extension of $\mathcal B$. And from there, the guess is that we will be able to import an associativity pentagon from $\mathcal B$, allowing us to extend $\mathcal E$ to a 4-truncated semisimplicial space. And so forth. I think the fact that the fibration $\mathcal E \to \mathcal B$ records even one level of associativity beyond what $\mathcal E$ itself can record makes it very likely that the whole ladder can be climbed (externally). Of course, I haven't actually shown this, but it seems unmotivated to me to suspect that the fibration will give one extra layer of associativity and no more.

Tim Campion (May 14 2021 at 22:22):

Mike Shulman said:

Tim Campion said:

Oh -- and it bears mentioning on the semantic side that the forgetful functor from $\infty$-categories to weak categories is fully faithful

In particular, can you explain this?

The thought is that if I have a map of simplicial spaces, and if those simplicial spaces are Segal, then all the data of the map is contained in the first two levels. It's possible that I'm making a mistake -- I should have said I think this is the case rather than that I was "menioning" it. I'm thinking that just as the nerve of a 1-category is a 2-coskeletal simplicial set, so too the classifying diagram of an $(\infty,1)$-category $C$ should have an appropriate 2-coskeletality property which determines any map into $C$ from $D$ just from knowing what the map does on the 0,1,2 levels of $D$. But again, I do not have a precise statement, and it is possible that I am mistaken.

Mike Shulman (May 15 2021 at 01:15):

Tim Campion said:

The thought is that if I have a map of simplicial spaces, and if those simplicial spaces are Segal, then all the data of the map is contained in the first two levels.

That seems very unlikely to me. From an algebraic perspective, a weak $\infty$-functor includes constraint data at all dimensions witnessing not only that it preserves composition up to homotopy, but that it preserves all the higher coherence of composition up to homotopy.

Tim Campion (May 15 2021 at 06:04):

Mike Shulman said:

Tim Campion said:

The thought is that if I have a map of simplicial spaces, and if those simplicial spaces are Segal, then all the data of the map is contained in the first two levels.

That seems very unlikely to me. From an algebraic perspective, a weak $\infty$-functor includes constraint data at all dimensions witnessing not only that it preserves composition up to homotopy, but that it preserves all the higher coherence of composition up to homotopy.

I think it's true. At the moment, I can only show that the space of lifts is empty or contractible, but I believe that if you can lift to the 2nd stage, then you can lift all the way.

Theorem: Let $n \geq 1$ and let $f: X_{\leq n} \to Y_{\leq n}$ be a map of $n$-truncations of Reedy-fibrant Segal spaces $X,Y$. Then the space of maps $g: X_{\leq n+1} \to Y_{\leq n+1}$ extending $f$ is empty or contractible.

Proof: By the Reedy construction the space of such maps is homotopy equivalent to the space of maps $g: X([n+1]) \to Y([n+1])$ forming a commutative square

$$\begin{CD} X([n+1]) @>>> Map(\partial \Delta[n+1], X_{\leq n}) \\ @V{g}VV @VVV \\ Y([n+1]) @>>> Map(\partial \Delta[n+1], Y_{\leq n}) \end{CD}$$

But note that we can extend this diagram by another commutative square:

$$\begin{CD} X([n+1]) @>>> Map(\partial \Delta[n+1], X_{\leq n}) @>>> Map(Sp[n+1], X_{\leq n}) \\ @V{g}VV @VVV @VVV \\ Y([n+1]) @>>> Map(\partial \Delta[n+1], Y_{\leq n}) @>>> Map (Sp[n+1], Y_{\leq n}) \end{CD}$$

Here $Sp[n+1]$ is the $n+1$-spine. The rows are equivalences by Segalicness. So after adjointing things over, it will suffice to show that the map $\partial \Delta[1] \times Idem^+ \cup_{\partial \Delta [1] \times \Delta [1]} \Delta [1] \times \Delta [1] \to \Delta [1] \times Idem^+$ is co-fully-faithful -- i.e. it induces a fully faithful functor when homming into $\mathcal D$ for any $\infty$-category $\mathcal D$ (we really only need $\mathcal D = Top$). Here $Idem^+$ is the walking split idempotent. This follows by contemplating the following diagram:

$$\begin{CD} \partial \Delta [1] \times \Delta [1] @>>> \Delta [1] \times \Delta [1] \\ @VVV @VVV \\ \partial \Delta [1] \times Idem^+ @>>> \partial \Delta [1] \times Idem^+ \cup_{\partial \Delta [1] \times \Delta [1]} \Delta [1] \times \Delta [1] \\ @V{=}VV @VVV \\ \partial \Delta [1] \times Idem^+ @>>> \Delta [1] \times Idem^+ \end{CD}$$

The top left downward map is co-fully-faithful, so the top right downward map also is because co-fully-faithful maps are closed under cobase-change. The composite downward map on the right is also co-fully-faithful. It follows that the bottom right downward map is co-fully-faithful, because co-fully-faithful maps have a cancellation property: if $g \circ f$ and $ff$ are co-fully-faithful, then so is $g$.

Tim Campion (May 15 2021 at 06:12):

So at the very least, the space of extensions of a map of truncations of Segal spaces to a map of Segal spaces is a mere proposition.

Tim Campion (May 15 2021 at 13:41):

More concretely, any extension of $F: X_{\leq 1} \to Y_{\leq 1}$ to $G : X \to Y$ must be given by the formula $G_n = F_1 \times_{F_0} \cdots \times_{F_0} F_1$ under the equivalences given by the Segal conditions, and it is a mere proposition to ask whether this formula is functorial. That is, does this formula commute with all face maps? Supposing that this is so up to level 2, it extends to all higher levels because, thanks to the Segal condition, all higher face maps decompose as fiber products of composites of face maps of dimension $\leq 2$. So assuming that we in fact have $F : X_{\leq 2} \to Y_{\leq 2}$, I believe this means we do get an extension to $G : X \to Y$.

Tim Campion (May 15 2021 at 13:43):

I think in order to make this argument completely rigorous one would need to work more carefully in a specific model. But if it's not convincing in outline, I'd be interested to hear why.

Tim Campion (May 15 2021 at 13:46):

If it still feels unlikely, then do note that the $n$ th level of a Segal space contains a lot more information than the $n$-skeleton of a quasicategory. I agree that a map of quasicategories is not typically determined by its restriction to $n$-skeleta for any $n$.

Tim Campion (May 15 2021 at 13:48):

But I suppose this argument is saying that the full subcategory of $Cat_\infty$ with object set $\{[0],[1],[2]\}$ is dense in $Cat_\infty$. Put that way, I agree that it sounds surprising.

Mike Shulman (May 15 2021 at 14:47):

I'm sorry, this is impossible for me to follow. Can you write it out with displayed equations and commutative diagrams (either here or in pdf)?

Tim Campion (May 15 2021 at 16:32):

@Mike Shulman Thanks, I appreciate your continued interest despite my borderline - incoherence! I was able to track down a post elsewhere on this zulip where somebody posted a commutative diagram and then mimic their code, so I've edited the above now to actually contain the commutative diagrams I was describing so badly. Hopefully it makes a little more sense now!

Tim Campion (May 15 2021 at 17:43):

I seen now my mistake. The map $[1] \to Idem^+$ is not co-fully-faithful (I must have been thinking of the map $Idem \to Idem^+$). So my claim "the forgetful functor from Segal spaces to '2-truncated Segal spaces' is fully faithful" is wrong -- it is too strong. I still have some optimism that my overall proposal for simplicial types might still be correct.

Nathanael Arkor (May 18 2021 at 10:34):

It looks like this recent note by Chen and Kraus is relevant to this discussion.

Tim Campion (May 18 2021 at 16:07):

I thought about this a bit more, and I now think I see the problem with this "fibration of 2-truncated semisimplicial types" approach. The issue is that the form of "associativity" which I noted above, coming from the fibrational structure, is simply not a strong enough form of associativity, even before we start trying to think about higher associativity. The reason is that this "associativity" allows the endpoints to "float". We could probably pin down one endpoint, but we're still left with a situation where we get, for each $e_0 \xrightarrow{e_{01}} e_1 \xrightarrow{e_{12}} e_2 \xrightarrow{e_{23}} e_3$, an equality $e_{23} \circ (e_{12} \circ e_{01}) = (e_{23} \circ e_{12}) \circ e_{01}$, but only relative to some equality $\epsilon_{0123}: e_3 = e_3$ -- not in the type $\mathcal E(e_0,e_3)$ itself.

One way of expressing this shortcoming is that if one tries to express the "fibration" $\Gamma : \mathcal E \to \mathcal B$ as a "pseudofunctor" $\mathcal B \to Type$, then there doesn't seem to be a way to express the highest level of coherence for the pseudofunctor (on the nlab https://ncatlab.org/nlab/show/pseudofunctor#definition this is the very last equation given in the definition of a pseudofunctor) -- the equation which involves 4 objects and 3 maps (and which basically corresponds to the 3rd oriental).

So the whole premise of my idea -- the notion that somehow an "extra level of associativity" was coming "for free" seems to be wrong. In particular, I'm not pretty sure it's not the case that from a fibration of 2-truncated semisimplicial types as indicated above, one can always write down an extension to a fibration of 3-truncated semisimplicial types.

Mike Shulman (May 18 2021 at 16:08):

Coherence rarely comes for free... (-:

Tim Campion (May 19 2021 at 17:58):

Mike Shulman said:

Coherence rarely comes for free... (-:

Except in the Eckmann-Hilton argument... maybe we can define $E_\infty$-spaces this way?

Roughly following Hirschowitz, Hirschowitz, and Tabareau https://hal.archives-ouvertes.fr/hal-01178301 (HHT), we can define the notion of a wild $\omega$-category coinductively (except I think we can leave out the associativity they impose, keeping only interchangers). That is, we can define $C : wCat_\omega$ coinductively to comprise $C_0 : Set$, $Hom_C : C_0 \to C_0 \to wCat_\omega$, and $\circ : \prod_{x,y,z : C_0} wFun_\omega(Hom_C(x,y) \times Hom_C(y,z), Hom_C(x,y))$, where $C \times D$ is coinductively defined in the obvious way, and $F: wFun(C,D)$ coinductively comprises $F_0 : C_0 \to D_0$, $F_1 : \prod_{x,y: C_0} wFun(Hom_C(x,y) , Hom_D( F_0 x , F_0 y))$, and an equality saying that $F$ commutes with $\circ$, where "equality" probably means "cell equality" in the sense of HHT.

In this setting, I believe we can lift the"flattening" operation, which turns an $n$-category into its $n-1$-category of morphisms, to an operation on wild $\omega$-categories. Say that $X : wCat_\omega$ is $k$-connected if $X_0$ is the unit type and $Hom_X(tt,tt)$ is $k-1$-connected. Say that $X : wCat_\omega$ is $k$-tuply monoidal if it is the $k$-fold flattening of a $k$-connected wild $\omega$-category, and say that a wild $\omega$-category is symmetric monoidal if it is $k$-tuply monoidal for every $k$.

The $\infty$-categorical Eckmann-Hilton argument leads me to suspect that if $X$ is symmetric monoidal, then $X_0$ is an $E_\infty$-space. Perhaps in this way, one can define the type of $E_\infty$-spaces in HoTT.

Tim Campion (May 19 2021 at 18:08):

There will need to be units too, to get the Eckmann-Hilton argument going. Those are discussed by HHT as well, and presumably can be added to the definition without fuss.

Mike Shulman (May 19 2021 at 19:47):

Hmm... could you phrase it more simply as defining an $\omega$-fold magma coinductively?

finegeometer (Jun 21 2023 at 17:47):

Do we even know how to postulate semisimplicial types?

Specifically, do we know how to define semisimplicial-types-exist : Type, such that an inhabitant of that type would be a satisfying answer to the original question?

(I gave this a brief try, but I think I hit the same infinite regress that's causing problems for the implementation of semisimplicial types.)

Another way to think about this is: "Can we write the API that a module implementing semisimplicial types should provide?". I feel that if this can't be done, or even can't be done simply, we ought to be looking for ways to extend HoTT to make it simple.

Mike Shulman (Jun 21 2023 at 17:56):

No, I don't think we know how to do that.

Nicolai Kraus (Jun 22 2023 at 16:46):

finegeometer said:

Do we even know how to postulate semisimplicial types?

Like @Mike Shulman, I also don't think we know how to do this. I made the same experience as you (@finegeometer), namely that specifying directly what one expects leads to the same sort of coherence issues as the attempts to construct such a type.

One workaround that I've discussed with @Josh Chen a few years ago might be to define a type T such that an element t : T would give rise to a definition of semisimplicial types. That means we "over-approximate" the problem of semisimplicial types. Of course, we still want it to be consistent to assume that there's an element of T.

My (only) suggestion for such a T is the type expressing that HoTT can eat itself. Here's one way how we could define T: First, define the notion of a wild CwF in HoTT. It's a tuple of the usual components, (Con, Sub, Ty, Tm), together with substitution operations and identity types for the functor equations. However, we don't include truncation conditions or other higher categorical components (aka coherences), which is why I call this thing "wild". It's a very ill-behaved definition, basically an $\infty$-category with families where almost all of the structure is removed. Usually, we avoid such ill-behaved structures like the plague, but I'd conjecture that it does the job here. The reason is that the internalised syntax, i.e., the initial set-based CwF (implemented e.g. as the Ambrus-Thorsten syntax QIIT) is such a wild CwF, and the universe ("standard model") is also a wild CwF, so you can ask whether there's a wild CwF morphism between them. While not a well-behaved notion, it's a finite thing that one can write down in HoTT. That's my suggestion for the type T.

The next question is, of course, whether an element of T (that you could postulate) gives rise to a definition of semisimplicial types. This probably depends a bit on what exactly we mean by this. I'm pretty sure that it won't give rise to a strict/judgmental (Reedy fibrant) functor $\Delta_{\textsf{mono}}^{\textsf{op}} \to \mathcal U_1$. However, it's somewhat plausible to hope that it gives rise to something that is point-wise the correct thing, in the sense the it gives a function SST : Nat -> U. One would do this by defining each SST n in the syntax-CwF and then transport it to the universe using the wild CwF morphism. But there are many things to be checked and constructed, and @Josh Chen and I discovered that it's really not easy at all - however, I think it gives a plausible strategy....

Nevertheless, assuming all of this works, a final question is whether T is actually "too strong", or whether it might be "just right". As we don't have a direct internalisation of the statement "semisimplicial types can be constructed", we can't just ask whether T is equivalent to it. But another conjecture is that semisimplicial types can be constructed iff HoTT eats itself, which could make it reasonable to say that the described type T is exactly the type semisimplicial-types-exist that you were asking for.

Another line of thought is this:

finegeometer said:

we ought to be looking for ways to extend HoTT to make it simple.

Two-level type theory (2LTT) offers one way of extending HoTT. You can think of it as HoTT plus some syntax for its meta-theory. In this setting, you can essentially define a semisimplicial type to be an infinite tuple (A0, A1, A2, ...), but it won't be an actual fibrant type in HoTT; instead, it will live at the outer (meta-theoretic) level. However, you can then simply add the axiom that this sort of construction is fibrant (i.e. lives in HoTT). In other words, it's a framework which allows you exactly to formulate postulates for HoTT such as the one you asked about.

Mike Shulman (Jun 22 2023 at 18:30):

you can then simply add the axiom that this sort of construction is fibrant

By the way, this axiom may seem ad hoc, but it follows from the more natural-seeming axiom that "exo-nat is cofibrant". (It also follows from the stronger axiom that "exo-nat is fibrant", but we don't know how to interpret that one in all $\infty$-toposes, while @Elif Uskuplu has verified that we can do that for "exo-nat is cofibrant".)

Mike Shulman (Jun 22 2023 at 18:31):

Hmm, perhaps by "this sort of construction" you actually meant to refer not just to semisimplicial types but to all the constructions you can do with cofibrant exo-nat? If so, sorry.

Mike Shulman (Jun 22 2023 at 18:40):

On the other hand, 2LTT is a pretty big hammer, and it's unclear how practical it is in practice for actually working with semisimplicial types defined in this way, since you get a lot of exo-equalities that you have to manipulate manually. @Astra Kolomatskaia and I are currently working on a different extension of HoTT that allows the type of semisimplicial types to be defined with a single generalized sort of coinductive definition.

Astra Kolomatskaia (Jun 22 2023 at 23:53):

It should be noted that our WIP has full semantic generality in the sense of having models in any infinity-topos. From what Mike summarised about the 2LTT paper, this should be true in 2LTT as well.

Astra Kolomatskaia (Jun 22 2023 at 23:58):

"Doing SSTs in HoTT" is sort of an indefinite problem because we probably don't want to be overly specific by what we mean by "HoTT". Saying "Book HoTT" seems to be a reasonably precise specification, and my intuition says that you can't do it in that setting, but one possible definition is that it is any type theory that has semantic generality in infinity-topi and has sufficiently many features that we would expect (e.g. univalence and some HITs). In which case, perhaps 2LTT solved this problem some time ago. However, the solution that Mike and I are working on has the advantage that the additional structure added to the theory is incredibly natural for SSTs and is necessary for expressing their universal property.

Astra Kolomatskaia (Jun 23 2023 at 00:00):

I would also like to make the point that it is possible to construct certain specific SSTs in present day Agda:
https://github.com/FrozenWinters/SSTs/blob/main/ZS.agda

Astra Kolomatskaia (Jun 23 2023 at 00:00):

This is code that I wrote which constructs the singular SSTs.

Astra Kolomatskaia (Jun 23 2023 at 00:02):

So, in particular, the following was generated by the above Agda code:

Astra Kolomatskaia (Jun 23 2023 at 00:02):

Screenshot-2023-06-22-at-8.01.50-PM.png

Astra Kolomatskaia (Jun 23 2023 at 00:04):

In general, see my HoTTEST talk for a preview of the WIP stuff [although a lot has changed since then]:
https://www.youtube.com/watch?v=fQv2FpeFxew

Nicolai Kraus (Jun 23 2023 at 10:54):

Mike Shulman said:

Hmm, perhaps by "this sort of construction" you actually meant to refer not just to semisimplicial types but to all the constructions you can do with cofibrant exo-nat? If so, sorry.

Well, I was very unspecific :smile:
I didn't mean any single precise construction here. I just meant: Say, one has "something" (e.g., a classifier for semisimplicial types, or a construction involving meta-theoretic natural numbers) in mind that works in a class of models that one is interested in, but one doesn't know how to talk about it in HoTT. One can then attempt to describe it as a not-necessarily-fibrant type in 2LTT and add the axiom that it is fibrant; this will give an extension of HoTT where one can study that "thing". I really see 2LTT as a convenient framework that allows one to formulate assumption or study meta-theoretic statements that aren't (known to be) internalisable in HoTT in any reasonable sense.

Nicolai Kraus (Jun 23 2023 at 11:26):

Mike Shulman said:

On the other hand, 2LTT is a pretty big hammer, and it's unclear how practical it is in practice for actually working with semisimplicial types defined in this way, since you get a lot of exo-equalities that you have to manipulate manually.

I'm not sure I agree with the hammer part, but that might be because I view 2LTT differently. While one can use a concrete instance of 2LTT as a setting to work with semisimplicial types, I don't see this as the primary point of 2LTT (even though this might have been Voevodsky's primary motivation for HTS, I don't know). I rather see 2LTT as a framework in which one can talk about some meta-theoretic statements without leaving the language of type theory.

For example, if someone presents a new extension of HoTT (let's call it HoTT-E), I can try to understand HoTT-E as (the fibrant fragment of) an instance of 2LTT, where the inner level is HoTT, the outer (exo-) level is some version of MLTT, together with a postulate that a certain construction preserves fibrancy. HoTT-E will probably be more user-friendly and nicer for developing actualy theorems in a proof assistant in practice, because HoTT-E will probably come with judgmental computation rules that the instance of 2LTT doesn't have; however, thanks to a conservativity argument, HoTT-E still corresponds to the concrete instance of 2LTT. This way, I can try to understand what HoTT-E actually does compared to HoTT, and whatever development I know to be possible in the instance of 2LTT will be possible in HoTT-E.

(It could of cause be that I can't describe HoTT-E as an instance of 2LTT in a non-trivial way that lets me related it to HoTT. But 2LTT is phrased in a very general way, so it's at least possible.)

So, from the point of view of a user who uses one concrete instance of 2LTT to develop semisimplicial types, I agree that it feels like a pretty big hammer; but conceptually, it's actually a fairly trivial and straightforward thing. Do we know a model of HoTT that is not also a model of (a standard instance of) 2LTT? I'm not aware of any such model, which makes me think that having the exo-structure lying around isn't a strong assumption at all.

Nicolai Kraus (Jun 23 2023 at 11:38):

Astra Kolomatskaia said:

I would also like to make the point that it is possible to construct certain specific SSTs in present day Agda:
https://github.com/FrozenWinters/SSTs/blob/main/ZS.agda

Thanks, this is nice! What does it mean for HoTT? I don't know a specification of Agda that is simple enough for me to understand it, and I found that Agda can do all sorts of stuff that I can't translate to HoTT. (Doesn't Agda have some sort of reflection? Plus the REWRITE pragma. I wouldn't be surprised if Agda could actually eat HoTT.)

Mike Shulman (Jun 23 2023 at 15:49):

Do we know a model of HoTT that is not also a model of (a standard instance of) 2LTT?

Well, there is the conservativity theorem that every model of HoTT can be embedded in a model of 2LTT. But probably you are also thinking of the fact that most real-world models of HoTT arise by imposing fibrancy requirements on the objects of some 1-category and thus ought to directly be the inner types in a model of 2LTT.

By calling 2LTT a big hammer I didn't mean that it significantly restricted the semantic applicability of the results. Rather I meant that it gives you a whole lot more than just SSTs. I think this may be the crucial point:

HoTT-E will probably be more user-friendly and nicer for developing actualy theorems in a proof assistant in practice, because HoTT-E will probably come with judgmental computation rules that the instance of 2LTT doesn't have

In the case of SSTs, the question is how to find a "HoTT-E" that has this property. The theory that Astra and I are developing is one candidate. In general, we can regard the definition of SSTs in 2LTT as a "specification" that a putative "type theory in which one can define SSTs" ought to satisfy, rather than thinking of 2LTT itself as "a type theory in which one can define SSTs". Does that make sense?

Nicolai Kraus (Jun 23 2023 at 16:18):

Yes, that's also what I mean. Looking forward to the theory you're developing when it's completed!