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

Atrium > Mathematics, Physics & Philosophy: simplicial identity types?

Bottom of Page

1 to 8 of 8

  1.  
    • CommentRowNumber1.
    • CommentAuthorTobias Fritz
    • CommentTimeMay 25th 2013
    • (edited May 25th 2013)

    Hi,

    in homotopy type theory, higher identity types have a globular structure. Is there also a kind of intensional type theory in which higher identity types have the structure of a simplicial set?

    I suppose that reflexivity terms should correspond to degenerate simplices. But then, an identity term p:Id A(x,y)p:\mathrm{Id}_A(x,y) should have two reflexivity terms associated to it! Would this make any sense at all? If so, how could an inductive definition of such higher identity types look like?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeMay 28th 2013

    This is an excellent question, which some people have thought about, but no definite answer is known yet.

    One thing to note is that ordinary identity types suffice to give a weak factorization system, and the usual framing/resolution theory in model categories makes any object into a simplicial one from only a weak factorization system… plus finite limits and colimits! In type theory, HITs give us only homotopy limits and colimits, but we could perhaps try to mimic the usual construction to get a ’homotopy’ simplicial structure. On the other hand, it’s not clear whether this would be interesting or useful.

    Another approach would be to use only degeneracies of 0-simplices to generate the whole structure inductively. This seems to yield something in between a simplicial object and a semisimplicial one.

    Finally one could try to build the notion of simplicial object into the type theory directly. I don’t know if anyone has tried this seriously.

    • CommentRowNumber3.
    • CommentAuthorZhen Lin
    • CommentTimeMay 28th 2013

    Mimicking the definition of homotopy-coherent nerve, could we not define e.g. Id A(x,y,z)Id_A (x, y, z) to consist of tuples (p,q,r,s)(p, q, r, s), where p:Id A(x,y)p : Id_A (x, y), q:Id A(y,z)q : Id_A (y, z), r:Id A(x,z)r : Id_A (x, z), and s:Id Id A(q∘p,r)s : Id_{Id_A} (q \circ p, r)? This seems like the obvious thing to do with any globular category.

    • CommentRowNumber4.
    • CommentAuthorTobias Fritz
    • CommentTimeMay 28th 2013

    @Mike: that’s good to know!

    @Zhen: that’s also what I thought. If this makes sense, then it should be possible to do this for all dimensions using the combinatorics of orientals to translate from the globular world to the simplicial word.
    What seems unnatural about this is that it needs infinitely many identity types (one for each arity). Or could there be a way to define all of those at once as in (ℕ→A)→Type(\mathbb{N}\to A)\to\mathbf{Type}?

    My understanding of HoTT hasn’t extended beyond the basic conceptual ideas yet, so I’m very shaky on the technical details…

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeMay 28th 2013

    I think the problem with that is going to be satisfying the iterated degeneracy laws.

    • CommentRowNumber6.
    • CommentAuthorTobias Fritz
    • CommentTimeMay 28th 2013

    Thanks for the comments, Mike! It will take some us time to think about them.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 10th 2013

    Another way of departing from the globular, rather than the simplicial, is the opetopic.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJun 10th 2013

    I have added that link to opetope.

1 to 8 of 8

  1.