Elementary reasoning for structuralists, Shulman's practical type theory of symmetric monoidal categories, and sketches of a type theory for symmetric monoidal bicategories
Paul Lessard – 12 August 2020, 19 August 2020, 26 August 2020
In this series of talks (borrowing from a talk jointly written with Nuiok Dicaire) we'll:
*) Explore how type theories for certain cartesian monoidal (hihger)-categories, HoTT for example, through their term calculus can:'give structuralists their elements back'in the sense that we are granted a form of reasoning:
**) which looks and feels like reasoning about sets with elements; but
**) which comes with syntactic limits on that which can be defined:
-) functions,
-) propositions,
-) etc.
such that this elementary reasoning coincides precisely with reasoning about the structural, i.e. (higher)-categorical properties of objects.*) Develop Mike Shulman's:"... Practical Type Theory for Symmetric Monoidal Categories"as a type theory with a term calculus which extends this program to symmetric monoidal categories*) Treat the example of the free dual pair in this type theory in some detail, explaining:
**) how a natural presentation of the free dual pair as a co-equalizer of free (coloured)-Props defines a PTT
**) how the term calulus of the type theory recovers the familiar elementary relationship between functions and functional from the structural one of a duality
**) see how the cyclicity of trace is easily proved elementarily in this type theory*) Describe how the computads of Street, Batanin, et al. and the strictification results of Schommer-Pries pave the way towards higher dimensional variants of Shulman's PTT and a synthetic treatment of symmetric monoidal bicategories, etc.(this last topic will cover joint work with Nuiok Dicaiure, Zeinab Galal, Paige North, Mike Shulman, and Sam Speight)
Back