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)