Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeNov 19th 2012

quick note semi-Segal space (just recording a reference of a speaker we had today)

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeNov 20th 2012
• (edited Nov 20th 2012)

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…

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeNov 20th 2012

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.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeNov 23rd 2012
• (edited Nov 23rd 2012)

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$”):

1. 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.

2. satisfying the Segal-conditions;

3. such that the two maps $Eq(X_1) \to X_1 \stackrel{\partial_0, \partial_1}{\to} X_0$ are equivalences.

4. such that $X_0$ is $n$-truncated.

I suppose. (And maybe up to correcting my counting…)

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeNov 23rd 2012
• (edited Nov 23rd 2012)

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

1. a type $\vdash\; X_0 \colon Type$

2. 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) \,;$
3. 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

1. 0-truncation$X_0$ is 0-truncated/is an h-set

2. 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;

3. 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;

4. unitality – the function

$p_1 \colon \underset{x \colon X_0}{\sum} X_1(x,x) \to X_0$

is an equivalence.

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeNov 23rd 2012
• (edited Nov 23rd 2012)

And then the next step in exploring #4:

A $(1,1)$-category type is

1. a type $\vdash\; X_0 \colon Type$

2. 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) \,;$
3. 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 \,,$
• $(\sigma_{123}, \sigma_{023}, \sigma_{013}, \sigma_{012}) \colon X^{\partial \Delta^3} \;\vdash\; X_3(\sigma_{123}, \sigma_{023}, \sigma_{013}, \sigma_{012}) \colon Type$

such that

1. 1-truncation$X_1$ is 1-truncated/is an h-groupoid

2. 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;

3. 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;

4. 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.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeDec 3rd 2012

What does it mean to say that a morphism is an “equivalence” before you have a notion of identity morphism?

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeDec 3rd 2012
• (edited Dec 3rd 2012)

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.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeDec 3rd 2012

Do you then automatically get all the higher degeneracies?

• CommentRowNumber10.
• CommentAuthorUrs
• CommentTimeDec 3rd 2012

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.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTimeDec 4th 2012

Interesting.

• CommentRowNumber12.
• CommentAuthorUrs
• CommentTimeDec 4th 2012
• (edited Dec 4th 2012)

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.

• CommentRowNumber13.
• CommentAuthorMike Shulman
• CommentTimeDec 5th 2012

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.

• CommentRowNumber14.
• CommentAuthorUrs
• CommentTimeDec 5th 2012

Thanks, Mike, that’s very useful to know.