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.
Eric Bond (Aug 23 2021 at 19:36):Hello!
I've been following the Polynomial Functors course from Topos Institute and attempting to formalize the definitions in Agda.
This is an example showing that Turing machines can be expressed as natural transformations of polynomial functors.
https://gist.github.com/bond15/1d56e4a605e302498fceb1dae0f03f45
(for anyone interested, https://github.com/bond15/Polynomials-Categorically contains more work)
I come from a type theory/CS background and i'm still trying to grok applied category theory.
Just wanted to say thanks to all the folks who made that class possible :)
David Michael Roberts (Aug 24 2021 at 10:56):I was asked on Twitter if there is a non-code writeup of this. Is there?
Nathanael Arkor (Aug 24 2021 at 11:00):There's some reference to Turing machines in the book David Spivak and Nelson Niu are writing.
Henry Story (Aug 24 2021 at 12:52):The first chapter of @David Jaz's book on Poly also has an example of a Turing machine. There is also Agda directory on its github repo, but I have not looked at it.
Matteo Capucci (he/him) (Aug 27 2021 at 09:36):Also see this video by @David Spivak himself