Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
quick note semi-Segal space (just recording a reference of a speaker we had today)
I have briefly added three basic definitions and a relations to semi-Segal space.
It’s probably not a surprise, but I never quite thought of it that way before: for a semi-Segal space – which is a semicategory object internal to $\infty Grpd$ – completeness/univalence is effectively the remaining unitality axiom…
That’s neat. It seems also related to the fact that a Kan-fibrant semi-simplicial set admits a choice of degeneracies making it simplicial.
One interesting upshot should be this: in principle then it seems we know how to say “$(n,1)$-category” internal to HoTT, for every finite $n$ (or maybe at least for “low $n$”):
it’s a semi-simplicial type $X_{0 \leq \bullet \leq n+3}$ formalized (which is tedious but possible for “low $n$”) as $(n+3)$ dependent types $X_0, X_1, X_2, \cdots, X_{n+3}$ by hand, like $x_0,x_1 \colon X_0 \vdash X_1(x_0,x_1) \colon Type$, etc.
satisfying the Segal-conditions;
such that the two maps $Eq(X_1) \to X_1 \stackrel{\partial_0, \partial_1}{\to} X_0$ are equivalences.
such that $X_0$ is $n$-truncated.
I suppose. (And maybe up to correcting my counting…)
To explore the above suggestion, let’s start with the lowest-degree case: with $(0,1)$-category types. How about the following definition?:
A $(0,1)$-category type is
a type $\vdash\; X_0 \colon Type$
a dependent type $x_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type$;
we write
$X^{\partial \Delta^2} \coloneqq \underset{x_0,x_1,x_2 \colon X_0}{\sum} X_1(x_1,x_2) \times X_1(x_0,x_2) \times X_1(x_0,x_1) \,;$a dependent type
$((x_0,x_1,x_2), (f_0, f_1, f_2)) \colon X^{\partial \Delta^2} \;\vdash \; X_2(f_0,f_1,f_2) \colon Type \,;$such that
0-truncation – $X_0$ is 0-truncated/is an h-set
1-coskeletalness – the function
$p_1 \colon \underset{(x_0,x_1) \colon X_0 \times X_0 }{\sum} X_1(x_0,x_1) \to X_0 \times X_0$is a 1-monomorphism;
Segal condition – the function
$( (f_{12},f_{02},f_{01}) \mapsto (f_{12},f_{01}) ) \colon \underset{((x_0,x_1,x_2),(f_{12},f_{02},f_{01})) \colon X^{\partial \Delta^2}}{\sum} X_2 \to \underset{ (x_0,x_1,x_2) \colon X_0 }{\sum} X_1(x_0,x_1) \times X_1(x_1, x_2)$is an equivalence;
unitality – the function
$p_1 \colon \underset{x \colon X_0}{\sum} X_1(x,x) \to X_0$is an equivalence.
And then the next step in exploring #4:
A $(1,1)$-category type is
a type $\vdash\; X_0 \colon Type$
a dependent type $x_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type$;
we write
$X^{\partial \Delta^2} \coloneqq \underset{x_0,x_1,x_2 \colon X_0}{\sum} X_1(x_1,x_2) \times X_1(x_0,x_2) \times X_1(x_0,x_1) \,;$a dependent type
$((x_0,x_1,x_2), (f_{12}, f_{02}, f_{01})) \colon X^{\partial \Delta^2} \;\vdash \; X_2(f_{12}, f_{02}, f_{01}) \colon Type \,;$we write
$X^{\partial \Delta^3} \coloneqq \underset{(x_0,x_1,x_2,x_3,x_4 \colon X_1) }{\sum} \underset{ f_{i j} \colon X_1(x_i, x_j)}{\sum} X_2(f_{12},f_{02},f_{01}) \times X_2(f_{23}, f_{13}, f_{12}) \times \cdots \,,$such that
1-truncation – $X_1$ is 1-truncated/is an h-groupoid
2-coskeletalness – the function
$p_1 \colon \underset{(f_{12},f_{02}, f_{01}) \colon X^{\partial \Delta^2}}{\sum} X_2(f_{12},f_{02}, f_{01}) \to X^{\partial \Delta^2}$is a 1-monomorphism;
Segal condition – the functions
$( (f_{12},f_{02},f_{01}) \mapsto (f_{12},f_{01}) ) \colon \underset{((x_0,x_1,x_2),(f_0,f_1,f_2)) \colon X^{\partial \Delta^2}}{\sum} X_2 \to \underset{ (x_0,x_1,x_2) \colon X_0 }{\sum} X_1(x_0,x_1) \times X_1(x_1, x_2)$and
$( (f_{i j}, \sigma_{i j k}) \mapsto (f_{01}, f_{12}, f_{23}) ) \colon \underset{f_{i j} \colon X_1(x_i,x_j)}{\sum} \underset{\sigma_{i_0 i_1 i_2} \colon X_2(f_{i_1 i_2}, f_{i_0 i_2}, f_{i_0 i_1})}{\sum} X_3( \sigma_{\cdots}, \cdots ) \to \underset{(x_0,x_1,x_2,x_3) \colon X_0}{\sum} X_1(x_0,x_1) \times X_1(x_1,x_2) \times X_1(x_2,x_3)$are equivalences;
unitality – the function
$(((x_0,x_1),f) \mapsto x_0) \colon \underset{x_0,x_1 \colon X_0}{\sum} X_1(x_0,x_1)_{\simeq} \to X_0$is an equivalence.
What does it mean to say that a morphism is an “equivalence” before you have a notion of identity morphism?
Once there is a notion of composition, a morphism is an equivalence if it induces equivalences of hom-spaces under composition. Yonatan discusses this in his section 4.1.
Do you then automatically get all the higher degeneracies?
Yonatan Harpaz shows that the $\infty$-category of complete Semi-Segal spaces is equivalent to that of complete Segal spaces. So in this sense, yes, the degeneracies can be recovered, up to equivalence.
Interesting.
So, I stared for a minute or two at Voevodsky’s recent code for semi-simplicial types. But I’ll need to stare at it for a few more minutes to parse it. Meanwhile, maybe you can give me a quick hint:
is his code the generalization to arbitrary degree of the low-degree expressions in #6?
If it is, then with Harpaz’ observation it would seem to be just a small remaining step to HoTT-internal $\infty$-categories.
First of all, that code doesn’t work. The fact that it doesn’t work is apparently the reason that he’s currently trying to develop a new type theory with a stronger, but undecidable, judgmental equality. Many type theorists seem to be dubious.
Second, I haven’t managed to make much sense of that code myself yet either, so I don’t think I can help you.
Thanks, Mike, that’s very useful to know.
1 to 14 of 14