Got an email indicating my external committee member seems okay with my thesis proposal (modulo a set of complaints hopefully of measure zero), which is exciting. I worked a little bit today on sketching out the talk. I ought to schedule a practice talk soon. Additionally got some work done on poking the ol' proof irrelevance stuff again. There's still a nagging question I haven't answered to my satisfaction about whether the irrelevant Pi tosses an irrelevant or relevant hypothesis into the context for the type kinding judgment.
Talked with neelk some more about multicategories, and some wooly stuff about What Is Extensional Equality All About, Man, which I enjoy.