You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Max New (Apr 13 2022 at 21:15):Hi everybody, I hope this isn't off-topic. I've been teaching a category theory class this semester in the computer science department at the University of Michigan (http://maxsnew.com/teaching/eecs-598-w22/) and for the last lecture I want to provide the students with some advertisements for different areas that they should now be empowered to explore on their own.
In the course, I've focused on mostly "programming language" examples, such as simply typed lambda calculus, Lawvere's fixed point theorem, Hoare Logic, logical relations, and monads. For my final lecture I plan to put brief pointers to dependent/homotopy type theory, polymorphism using reflexive graph categories, linear/substructural logic as monoidal categories/multicategories and its influence on languages like Rust, probabilistic programming using sheaves, as well as my own research on gradual typing and call-by-push-value.
So are there any suggestions for other topics to briefly cover? Shameless self-promotion is completely encouraged!
Evan Patterson (Apr 13 2022 at 23:04):I think that categorical models of relational databases are a nice complement to PLT applications for a CT in CS course. One can put bells and whistles on it, but the basic model of Spivak's functorial data migration is pleasingly simple: database schemas are finitely presented categories and database instances are set-valued functors (copresheaves) on the schema. With this setup, there is a dictionary between many standard CT and database concepts.
Tom Hirschowitz (Apr 14 2022 at 09:02):Ok, shameless self-promotion then: Peio Borthelle, @Ambroise Lafont, and I used category theory to prove a general congruence theorem for applicative bisimilarity, recasting and generalising Howe's standard format in terms of cellularity.
There is also the literature on high-level constructions for syntax with variable binding. E.g., a recent, impressive achievement is @Daniel Gratzer and @Jon Sterling's method for presenting type theories. Or the preprint I recently advertised here.
Finally, let's ping @Stelios Tsampas, who might have something to add.
Stelios Tsampas (Apr 14 2022 at 09:29):Thanks for the assist @Tom Hirschowitz.
Hey Max :). Since you're going to mention DTT and HTT, how about pointing them towards Agda, it's CT library and it's cubical version? And then coalgebras, they're a natural fit with computer science, right?
Max New (Apr 15 2022 at 00:46):Stelios Tsampas said:
Thanks for the assist Tom Hirschowitz.
Hey Max :). Since you're going to mention DTT and HTT, how about pointing them towards Agda, it's CT library and it's cubical version? And then coalgebras, they're a natural fit with computer science, right?
Could you be more specific on "coalgebra" ? Kind of a broad area
Stelios Tsampas (Apr 15 2022 at 10:53):You could start broadly by explaining coalgebras as a generic framework to model systems exhibiting observable behavior. Two nice, elementary instantiations of this framework (to mention to students) is that directed graphs are -coalgebras (coalgebras of the powerset functor) and that labelled transitions systems are -coalgebras for some set of labels .
Also, if you're feeling adventurous and your students are comfortable with SOS-style rules, you would point them towards Turi and Plotkin's bialgebraic framework (https://homepages.inf.ed.ac.uk/gdp/publications/Math_Op_Sem.pdf), presenting GSOS systems as natural transformations of a certain shape.