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.
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:\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?
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.
Mimicking the definition of homotopy-coherent nerve, could we not define e.g. $Id_A (x, y, z)$ to consist of tuples $(p, q, r, s)$, where $p : Id_A (x, y)$, $q : Id_A (y, z)$, $r : Id_A (x, z)$, and $s : Id_{Id_A} (q \circ p, r)$? This seems like the obvious thing to do with any globular category.
@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 $(\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…
I think the problem with that is going to be satisfying the iterated degeneracy laws.
Thanks for the comments, Mike! It will take some us time to think about them.
Another way of departing from the globular, rather than the simplicial, is the opetopic.
I have added that link to opetope.
1 to 8 of 8