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)