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.
Ben Sprott (Mar 12 2021 at 14:53):I am finding that there is a bit of a battle going on to provide a "foundation" of Type Theory, and perhaps for Mathematics, either with polynomial functors or Homotopy Type Theory. There is a nice table here that compares Homotopy Theory, based on spaces, to Type Theory. It would be great to get something similar for Polynomial Functors and Type Theory. Is this possible? The question is, how can we summarize how polynomial functors are used as a model of Type Theory?
Nathanael Arkor (Mar 12 2021 at 15:04):I think establishing the precise relationship between polynomial functors and type theory is a work-in-progress, though there are papers approaching a connection (from different perspectives) with simple type theories (by Marcelo Fiore and I) and with dependent type theories (by Steve Awodey and Clive Newstead).