So I’ve been thinking about higher-dimensional type theories off and on for awhile, and one thing I’ve been wondering about is what the design space is apart from the currently-being-explored point of homotopy type theory. I guess I tend to think of all this in terms of semantics, so let’s start from that perspective: if HoTT is a “theory of”, in that this is what types mean, weak -groupoids, and weak -groupoids are really just categories where arrows can exist at all levels but are all invertible, then what are the theories for other such categories?
For example, the first paper I read on higher-dimensional type theory in general is was Dan Licata’s dissertation that introduced Directed Type Theory (DTT) which was, essentially, a theory of categories in the same sense that HoTT is a theory of -groupoids. Now, if this is a theory of -groupoids then why couldn’t we, say, have a theory where types are -categories for any and or choice of weak/strict? I ask this not just from the perspective of logic and foundational mathematics, but from the perspective of someone who wants a serious theorem prover that implements such a logic. I wouldn’t be surprised if there was a difference in utility for programmers or implementors between some of these choices.
My own personal interest has drifted towards the strict theories because, well if I’m being perfectly honest, they haven’t been explored much and drifting off a little from the pack makes me feel more comfortable. I have my own 3TT theory, based on the Licata & Harper 2TT, that I wrote up and am trying to flesh out with examples and maybe a toy implementation in the near future. There’ll be a pdf on arXiv at some point even if it kills me, despite the fact that actually sharing my ideas is still rather terrifying. My concern at first was that by having types be interpreted as strict 2-groupoids would potentially ruin the ability to talk about 1-types in a meaningful way, but as far as I can tell I can still show that for the circle really is the integers. The choice I’ve made here, though, is to have induction over 1-types actually compute over paths definitionally not just propositionally, i.e. that the dependent eliminator’s “respect” of the loop of the circle is equal to the path supplied to the eliminator not just isomorphic to it. The HoTT book says in the notes of Ch 6 that they have semantic reasons for not necessarily wanting this to be a definitional equality, but given that I’ve chosen to work with the more strict theory I think it’s natural.
Of course, that’s all good to say but that do I have a fleshed out model theory for inductive types and can I show that I’ll actually buy anything from this experiment? I don’t know! That’s half the fun, I suppose. (The other half is terror, just for the record.)
But my current goals for the not too distant future involve
- understanding the sound and complete models for the theory without a notion of inductive types (based on my still unpublished work on the sound and complete models of 2TT (cough cough))
- try a simplified model of inductive 1-types (perhaps based off of what Shulmann and Lumsdaine were working on)
- actually write some preprints and throw them on arXiv for once