January 14th, 2007

beartato phd

(no subject)

Talking to neelk earlier today, I was informed that the things you get if you generalize multicategories to arrows with multiple codomains as well as multiple domains are called polycategories. This blog post makes an introduction to them which, being very much about logic and cut elimination, is quite near and dear to my heart. According to these slides polycategories have something to do with quantum entanglement, which is kinda weird. Here's a more detailed paper about them.

---

Also a couple citations about *-autonomous categories:

Linear Topology, Hopf Algebras, and *-Autonomous Categories, Richard F. Blute
*-Autonomous Categories: Once More Around the Track, Michael Barr
beartato phd

(no subject)

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.