One of those days

My update for the day is fairly skimpy. I skimmed "A View From The Left", started a paper on the omega-groupoid interpretation of ITT, and subsequently tripped over my lack of intuition about operads and landed flat on my fibration. I think I sprained a syntactic category, or something equivalent to it.

In all seriousness, I clearly need to read some relevant chapters both from Jacobs's Giant Yellow Book and from Leinster's elaboration of operads and higher-order categories. I was skimming along fine with my current level of mathematical knowledge, but need to buff up a bit now. I've read a bit of the machinery for the syntactic category of a dependent theory but it was long enough ago I can barely hum the tune. I probably could have faked it slightly better today had I slept well, but it was one of those days when I woke up <6 for no apparent reason.

I did, though, see a talk about relativistic programming and chatted briefly with one of the grad students working on it. It turns out that their last submission outlines a kind of induction principle for reasoning about concurrent programs that use their primitives for blocking. I was told that they hoped someone could pick up the note and mechanize the reasoning in some fashion, but I was good and didn't offer up my services. :-) Maybe it'd be a cute thing to do at some point during my PhD, but at the moment I'm too excited about digging into OTT/HTT/etc.

Papers of the Day: Moar Types

This is the second day of my binging on type theory. For today's reading I read the first couple of chapters of Dan Licata's thesis, Hoffman & Streicher's paper on groupoid models of type theory, and Altenkirch's original paper on OTT. 

As far as the thesis went, I only read the introduction and the background chapters so I haven't gotten into the heart of it yet. Funnily enough, the background chapter did have some food for thought in the distinction between derivability and admissibility. I don't know if this is a common way of looking at things that I would have seen if I had ever really taken courses in logic, but in any case I think it makes a lot of sense. I'll probably try to read a chapter three tomorrow.

Alright, so now we come to the things I'm still chewing on. First, there's the Hoffman & Streicher paper. The basic point of the paper was really about proving that uniqueness of identity proofs doesn't follow from intensional type theory by constructing a model where it didn't hold, but I can see that there was some deeper insight in terms of using groupoids to model types - setting the stage for the later omega-groupoid models which I intend to read about tomorrow - as well as it being a good illustration of the general technique of constructing models to help determine if a property of the logical system is necessarily true. I'll probably review some of the constructions again tomorrow, though, before I read some of the papers on omega-groupoid models.

Speaking of models, that's the main thing I've gotten so far out of the other Altenkirch paper: the idea that one can construct a model of your proposed theory within another type theory to determine if it is even possible to make. I think there's more I should be getting out of it, but honestly it was the last thing I read today and I was a bit burned out. I think I'll put it back on the pile for tomorrow for another attack.