Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 19th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexquick note _[[semi-Segal space]]_ (just recording a reference of a speaker we had today)

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

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeNov 20th 2012
   • (edited Nov 20th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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...

   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 – completeness/univalence is effectively the remaining unitality axiom…

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeNov 20th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat's neat. It seems also related to the fact that a Kan-fibrant semi-simplicial set admits a choice of degeneracies making it simplicial.

   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.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeNov 23rd 2012
   • (edited Nov 23rd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOne 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. 1. satisfying the Segal-conditions; 1. such that the two maps $Eq(X_1) \to X_1 \stackrel{\partial_0, \partial_1}{\to} X_0$ are equivalences. 1. such that $X_0$ is $n$-truncated. I suppose. (And maybe up to correcting my counting...)

   One interesting upshot should be this: in principle then it seems we know how to say “-category” internal to HoTT, for every finite (or maybe at least for “low ”):

   1. it’s a semi-simplicial type formalized (which is tedious but possible for “low ”) as dependent types by hand, like , etc.

   2. satisfying the Segal-conditions;

   3. such that the two maps are equivalences.

   4. such that is -truncated.

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

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeNov 23rd 2012
   • (edited Nov 23rd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexTo 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$ 1. 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) \,; $$ 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 1. **[[n-truncated|0-truncation]]** -- $X_0$ is [[0-truncated]]/is an [[h-set]] 1. **[[coskeleton|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]]; 1. **[[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 in homotopy type theory|equivalence]]; 1. **[[univalence|unitality]]** -- the function $$ p_1 \colon \underset{x \colon X_0}{\sum} X_1(x,x) \to X_0 $$ is an [[equivalence in homotopy type theory|equivalence]].

   To explore the above suggestion, let’s start with the lowest-degree case: with -category types. How about the following definition?:

   A -category type is

   1. a type

   2. a dependent type ;

      we write

   3. a dependent type

   such that

   1. 0-truncation – is 0-truncated/is an h-set

   2. 1-coskeletalness – the function

      is a 1-monomorphism;

   3. Segal condition – the function

      is an equivalence;

   4. unitality – the function

      is an equivalence.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeNov 23rd 2012
   • (edited Nov 23rd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexAnd then the next step in exploring [#4](http://nforum.mathforge.org/discussion/4537/semisegal-space/?Focus=37128#Comment_37128): A **$(1,1)$-category type** is 1. a [[type]] $\vdash\; X_0 \colon Type$ 1. 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) \,; $$ 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 \,, $$ * a [[dependent type]] $$ (\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. **[[n-truncated|1-truncation]]** -- $X_1$ is [[1-truncated]]/is an [[h-groupoid]] 1. **[[coskeleton|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]]; 1. **[[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 [[equivalence in homotopy type theory|equivalences]]; 1. **[[univalence|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 in homotopy type theory|equivalence]].

   And then the next step in exploring #4:

   A -category type is

   1. a type

   2. a dependent type ;

      we write

   3. a dependent type

      we write

   • a dependent type

   such that

   1. 1-truncation – is 1-truncated/is an h-groupoid

   2. 2-coskeletalness – the function

      is a 1-monomorphism;

   3. Segal condition – the functions

      and

      are equivalences;

   4. unitality – the function

      is an equivalence.

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeDec 3rd 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexWhat does it mean to say that a morphism is an "equivalence" before you have a notion of identity morphism?

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

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeDec 3rd 2012
   • (edited Dec 3rd 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexOnce 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](http://arxiv.org/pdf/1210.0212v1.pdf#page=37).

   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.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeDec 3rd 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexDo you then automatically get all the higher degeneracies?

   Do you then automatically get all the higher degeneracies?

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 3rd 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexYonatan 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.

    Yonatan Harpaz shows that the -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.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 4th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexInteresting.

    Interesting.

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 4th 2012
    • (edited Dec 4th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexSo, I stared for a minute or two at Voevodsky's recent [code](http://uf-ias-2012.wikispaces.com/file/detail/semisimplicial.v) 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.

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

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeDec 5th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexFirst 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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeDec 5th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexThanks, Mike, that's very useful to know.

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