bhudson was extremely helpful, and so was everyone else that came. Thank you all very much! I have some ideas now for how to redo it, but only about one day in which to implement them. My excuse for putting this off so long is spending all of last week chasing down the LFMTP deadline, but eh.Also had a meeting with Steve Awodey this morning during which we talked about how the categorical semantics for dependent types + world-labelled type operators might look.