Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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 Grpd\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)(n,1)-category” internal to HoTT, for every finite nn (or maybe at least for “low nn”):

    1. it’s a semi-simplicial type X 0n+3X_{0 \leq \bullet \leq n+3} formalized (which is tedious but possible for “low nn”) as (n+3)(n+3) dependent types X 0,X 1,X 2,,X n+3X_0, X_1, X_2, \cdots, X_{n+3} by hand, like x 0,x 1:X 0X 1(x 0,x 1):Typex_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)X 1 0, 1X 0Eq(X_1) \to X_1 \stackrel{\partial_0, \partial_1}{\to} X_0 are equivalences.

    4. such that X 0X_0 is nn-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)(0,1)-category types. How about the following definition?:

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

    1. a type X 0:Type\vdash\; X_0 \colon Type

    2. a dependent type x 0,x 1:X 0X 1(x 0,x 1):Typex_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type;

      we write

      X Δ 2x 0,x 1,x 2:X 0X 1(x 1,x 2)×X 1(x 0,x 2)×X 1(x 0,x 1); 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)):X Δ 2X 2(f 0,f 1,f 2):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-truncationX 0X_0 is 0-truncated/is an h-set

    2. 1-coskeletalness – the function

      p 1:(x 0,x 1):X 0×X 0X 1(x 0,x 1)X 0×X 0 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)(f 12,f 01)):((x 0,x 1,x 2),(f 12,f 02,f 01)):X Δ 2X 2(x 0,x 1,x 2):X 0X 1(x 0,x 1)×X 1(x 1,x 2) ( (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:x:X 0X 1(x,x)X 0 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)(1,1)-category type is

    1. a type X 0:Type\vdash\; X_0 \colon Type

    2. a dependent type x 0,x 1:X 0X 1(x 0,x 1):Typex_0,x_1 \colon X_0 \; \vdash \; X_1(x_0,x_1) \colon Type;

      we write

      X Δ 2x 0,x 1,x 2:X 0X 1(x 1,x 2)×X 1(x 0,x 2)×X 1(x 0,x 1); 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)):X Δ 2X 2(f 12,f 02,f 01):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 Δ 3(x 0,x 1,x 2,x 3,x 4:X 1)f ij:X 1(x i,x j)X 2(f 12,f 02,f 01)×X 2(f 23,f 13,f 12)×, 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

      (σ 123,σ 023,σ 013,σ 012):X Δ 3X 3(σ 123,σ 023,σ 013,σ 012):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. 1-truncationX 1X_1 is 1-truncated/is an h-groupoid

    2. 2-coskeletalness – the function

      p 1:(f 12,f 02,f 01):X Δ 2X 2(f 12,f 02,f 01)X Δ 2 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)(f 12,f 01)):((x 0,x 1,x 2),(f 0,f 1,f 2)):X Δ 2X 2(x 0,x 1,x 2):X 0X 1(x 0,x 1)×X 1(x 1,x 2) ( (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 ij,σ ijk)(f 01,f 12,f 23)):f ij:X 1(x i,x j)σ i 0i 1i 2:X 2(f i 1i 2,f i 0i 2,f i 0i 1)X 3(σ ,)(x 0,x 1,x 2,x 3):X 0X 1(x 0,x 1)×X 1(x 1,x 2)×X 1(x 2,x 3) ( (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)x 0):x 0,x 1:X 0X 1(x 0,x 1) X 0 (((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.