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.
No comments:
Post a Comment