Workshop on Polynomial Functors

Participants will learn background material and hear the latest progress on polynomial functors, monads, and comonads, their algebras and coalgebras, as well as on operads, parametric right adjoints, and cofunctors, with applications to combinatorics, database theory, dynamical systems, higher category theory, logic, and type theory.

Each day's talks will be live-streaming on YouTube at the links below:
March 15
March 16
March 17
March 18
March 19
You can also find each speakers' talk linked individually; see the schedule at page bottom.

Speakers

● Thorsten Altenkirch:

► Containers and inductive types

● Steve Awodey:

► Polynomial functors and natural models of type theory

● Michael Batanin:

► Grothendieck homotopy theory and polynomial monads

▼ Grothendieck homotopy theory and polynomial monads
Batanin's slides

Abstract: Grothendieck in 'Pursuing Stacks' has developed a beautiful axiomatic approach to homotopy theory. This theory was further deepened by Cisinski. One of the main points of Grothendieck's approach is that a 'good' homotopy theory must come with a rich toolbox of instruments for computing the main homotopy theoretical constructions. And he, indeed, provided such a toolbox using the category of small categories as a basis for his theory.

The category of polynomial monads contains the category of small categories as a full subcategory of 'linear' monads. In my talk I am going to show that the most important constructions of Grothendieck's theory can be extended from small categories and their categories of presheaves to the category of polynomial monads and their algebras. This includes: Quillen Theorem A, Grothendieck construction, Thomason theorem, homotopy left Kan extension construction, theory of homotopy final functors between small categories, Cisinski localisations etc... It is interesting that some of these constructions may have more than one analogue in the polynomial monads world.

As illustration of how practical this extended homotopy theory can be I will briefly sketch two applications:

1. A theory of delooping of mapping spaces between algebras of polynomial monads which leads to a new categorical proof of a seminal theorem of Dwyer-Hess and Turchin on double delooping of space of long knots.

2. A theory of locally constant algebras of polynomial monads which generalises Cisinski theory of locally constant functors. The Baez-Dolan stabilisation hypothesis for higher categories and the classical Freudenthal stabilisation theorem are some of the direct consequences of this theory.

Acknowledgement. I express my best gratitude to my coauthors C. Berger, F. de Leger and D. White. This talk is based on the results of our collaboration over several years.

● Bryce Clarke:

► Cofunctors, lenses, and split opfibrations

● Marcelo Fiore:

► Stable species of structures

● Richard Garner:

► Polynomials in categories with pullbacks

● David Gepner:

► Analytic monads and ∞-operads

● Helle Hvid Hansen:

► Coalgebras and their modal logics: polynomial functors and beyond

● Rune Haugseng:

► Polynomial functors and Segal conditions

● Bart Jacobs:

► Lifting of polynomial functors for logical reasoning

● André Joyal:

► Three kinds of polynomial functors

● Fredrik Nordvall Forsberg:

► Quantitative polynomial functors

● Kristina Sojakova:

► Initial algebras in homotopy type theory

● David Spivak:

► The polynomial abacus

● Ross Street:

► Polynomials as spans

● Tarmo Uustalu:

► Polynomial comonads

Organizers

Participation

Anyone interested in participating is welcome; simply fill out the online form. A zoom link will be sent out to registered participants a few hours before the workshop.

Program

(Sydney (+1) 07:00–11:00; Berkeley 13:00–17:00; Boston 16:00–20:00; Barcelona 21:00–01:00+; etc.)

Time (UTC)	Monday	Tuesday	Wednesday	Thursday	Friday
20:00–21:00	Joyal	Uustalu	Hansen 2	Altenkirch	Fiore
21:00–22:00	Spivak 1	Hansen 1	Jacobs	Sojakova	Haugseng
22:00–23:00	Garner 1	Street	Spivak 2	Batanin	Nordvall F.
23:00–24:00	Gepner	Clarke	Garner 2	Garner 3	Awodey

● Thorsten Altenkirch:	► Containers and inductive types ▼ Containers and inductive types Altenkirch's notes Abstract: Inductive types are playing a central role in Type Theory. They can be modelled using initial algebra of functors. However, not all functors have an initial algebra and the syntactic condition of strict positivity is reflected by the requirement that the functor is a container aka a polynomial functor. The term container derives from the intuition that an element of such a type contains the data it is parametrised by. Recent generalisations of inductive types include inductive-inductive types (IITs), quotient inductive-inductive types (QIITs, related to generalised algebraic types) and higher inductive-inductive types (HIITs). In this setting we cannot identify one functor since the types of one constructor can refer to a previous one. An example where this shows up is the intrinsic syntax of dependently typed languages, where intrinsic means that we avoid untyped preterms. In our talk we describe recent and ongoing work how to capture these situations semantically and syntactically. We exploit the view that a generalised container is a presheaf that is a sum of representables where the base category is the category of algebras of the previous constructors. We present a new syntax for QIITs which is itself a QIIT and we conjecture to be complete for the semantics.
● Steve Awodey:	► Polynomial functors and natural models of type theory ▼ Polynomial functors and natural models of type theory Awodey's slides Abstract: Dependent type theory is sometimes described categorically as a Category with Families (CwF). In [1], it was shown that the notion of a CwF can conveniently be reformulated as a so-called "natural model", which is simply a representable natural transformation p : U. → U over an arbitrary index category C of "contexts". Such a model of type theory admits dependent sums and a terminal type just if it is a (pseudo-)monad, when regarded as a polynomial endofunctor P : Ĉ → Ĉ on the category of presheaves on C. Moreover, dependent products correspond to a P-algebra structure. The logical Propositions-as-Types conception is then modelled by a retraction of polynomial monads relating the type theoretic and the topos-theoretic interpretations of predicate logic. [1] Awodey, S., Natural models of homotopy type theory, Math. Stru. Comp. Sci., 2018.
● Michael Batanin:	► Grothendieck homotopy theory and polynomial monads ▼ Grothendieck homotopy theory and polynomial monads Batanin's slides Abstract: Grothendieck in 'Pursuing Stacks' has developed a beautiful axiomatic approach to homotopy theory. This theory was further deepened by Cisinski. One of the main points of Grothendieck's approach is that a 'good' homotopy theory must come with a rich toolbox of instruments for computing the main homotopy theoretical constructions. And he, indeed, provided such a toolbox using the category of small categories as a basis for his theory. The category of polynomial monads contains the category of small categories as a full subcategory of 'linear' monads. In my talk I am going to show that the most important constructions of Grothendieck's theory can be extended from small categories and their categories of presheaves to the category of polynomial monads and their algebras. This includes: Quillen Theorem A, Grothendieck construction, Thomason theorem, homotopy left Kan extension construction, theory of homotopy final functors between small categories, Cisinski localisations etc... It is interesting that some of these constructions may have more than one analogue in the polynomial monads world. As illustration of how practical this extended homotopy theory can be I will briefly sketch two applications: 1. A theory of delooping of mapping spaces between algebras of polynomial monads which leads to a new categorical proof of a seminal theorem of Dwyer-Hess and Turchin on double delooping of space of long knots. 2. A theory of locally constant algebras of polynomial monads which generalises Cisinski theory of locally constant functors. The Baez-Dolan stabilisation hypothesis for higher categories and the classical Freudenthal stabilisation theorem are some of the direct consequences of this theory. Acknowledgement. I express my best gratitude to my coauthors C. Berger, F. de Leger and D. White. This talk is based on the results of our collaboration over several years.
● Bryce Clarke:	► Cofunctors, lenses, and split opfibrations ▼ Cofunctors, lenses, and split opfibrations Clarke's slides Abstract: Perhaps the most natural place to notice the duality between functors and cofunctors is within the double category Poly(E) of polynomials in a category E with pullbacks. Monads in Poly(E) whose underlying polynomial is a left adjoint are precisely internal categories, with the monad morphisms equivalent to internal functors. Dually, comonads in Poly(E) whose underlying polynomial is a right adjoint are also internal categories, while the comonad morphisms correspond to internal cofunctors. However, when E has finite limits, Ahman and Uustalu characterise categories and cofunctors in a different way, as comonads and comonad morphisms in the full double subcategory of Poly(E) on the terminal object. In this talk, I will first discuss how the above view of categories and cofunctors relates to the characterisation given by Ahman and Uustalu. Next I will consider a kind of morphism between categories, called a (delta) lens, which is both a functor and a cofunctor in a compatible way. Finally, I will characterise split opfibrations as lenses which behave nicely with respect to the decalage construction.
● Marcelo Fiore:	► Stable species of structures ▼ Stable species of structures Fiore's slides Abstract: We introduce a bicategorical model of differential classical linear logic that I will present both in intensional and extensional forms. The intensional model is based on a variation of the bicategory of groupoids and profunctors that results from endowing groupoids with structure of both logical and combinatorial character that stabilises the profunctors. Therein, we construct a star-autonomous bicategory and a linear exponential pseudocomonad on it that will be shown to simultaneously extend and refine the model of generalised species of structures restricted to groupoids. Extensionally, the structure carried by groupoids determines generalised domains as full subcategories of stabilised presheaves. From this viewpoint, we will see that the model consists of linear functors (namely, local left and right adjoints) and that the resulting cartesian closed coKleisli bicategory is that of stable functors (namely, epi-preserving finitary local right adjoints). This is joint work with Zeinab Galal and Hugo Paquet.
● Richard Garner:	► Polynomials in categories with pullbacks ▼ Polynomials in categories with pullbacks Garner's slides Abstract: This series of talks will describe the theory of polynomials in a category with pullbacks, as developed by inter alia Abbott, Altenkirch and Ghani; Gambino and Hyland; Gambino and Kock; and Weber. In particular, we describe how polynomials form themselves into a bicategory, and explain the universal properties of this bicategory, as described by Tamara von Glehn and by Charles Walker. If time permits, we sketch the link to Hyland's "theories of algebraic theories".
● David Gepner:	► Analytic monads and ∞-operads ▼ Analytic monads and ∞-operads Gepner's slides Abstract: We will discuss aspects of the theory of polynomials functors and infinity operads. Time permitting we will sketch some steps in an argument (joint with Rune Haugseng and Joachim Kock) that the infinity categories of infinity operads and analytic monads are equivalent.
● Helle Hvid Hansen:	► Coalgebras and their modal logics: polynomial functors and beyond ▼ Coalgebras and their modal logics: polynomial functors and beyond Hansen's slides: talk 1, talk 2. Abstract: This two-part talk is a tutorial on the use of coalgebraic techniques to model and reason about state-based dynamical systems. The first part will introduce the basic concept of an F-coalgebra for an endofunctor F, and the derived notions of morphism, bisimulation, behavioural equivalence and coinduction. We will see examples where F is a polynomial functor as well as examples where F is a composition of a polynomial functor and a monad in order to model systems with, e.g., nondeterministic or probabilistic transitions. The second part will be an introduction to coalgebraic modal logic, which is a framework for developing adequate and expressive modal logics for specifying properties of system behaviours. We will see that many results can be proved and studied parametric in the functor F. Time permitting, I will discuss some recent work on generalisations of the notion of coalgebraic bisimulation.
● Rune Haugseng:	► Polynomial functors and Segal conditions ▼ Polynomial functors and Segal conditions Haugseng's slides Abstract: Polynomial monads on slices of the infinity-category of spaces can be described as cartesian monads whose underlying endofunctor is accessible and preserves weakly contractible limits. Such "polynomial" monads can be considered in more general settings, and I will explain how polynomial monads on presheaf infinity-categories are closely related (through an infinity-categorical version of Weber's Nerve Theorem) to monads describing homotopy-coherent algebraic structures defined in terms of "Segal conditions". This is joint work with Hongyi Chu.
● Bart Jacobs:	► Lifting of polynomial functors for logical reasoning ▼ Lifting of polynomial functors for logical reasoning Jacob's slides Abstract: This will be a tutorial talk about explaining how logical reasoning principles associated with (co)algebras of a polynomial functor, as data types, can be obtained, via lifting of the functor to a logical level. This lifting happens in the context of fibrations, as categorical logical models. The lifting exploits the polynomial structure. Original source: C. Hermida and B. Jacobs, Structural induction and coinduction in a fibrational setting, Information and Computation 145 (1998), p.107-152.
● André Joyal:	► Three kinds of polynomial functors ▼ Three kinds of polynomial functors Joyal's slides Abstract: (Joint work with Marcelo Fiore and Nicola Gambino) We consider three kinds of polynomial functor: the first is associated to symmetric monoidal categories, the second to categories with finite cartesian products and the third to categories with finite limits. The category of polynomial functors is cartesian closed in every case.
● Fredrik Nordvall Forsberg:	► Quantitative polynomial functors ▼ Quantitative polynomial functors Abstract: Quantitative Type Theory combines linear types (where we keep track of how many times a variable is used) and dependent types (where we can keep track of properties of terms using types). This gives a logical system which is both expressive and precise with respect to the resource usage of programs and proofs, with a rich model theory. I will talk about data types in this setting, in the form of "resource-aware" polynomial functors and their initial algebras, and how "quantitative" induction can be derived from initiality. This is joint work with Georgi Nakov.
● Kristina Sojakova:	► Initial algebras in homotopy type theory ▼ Initial algebras in homotopy type theory Sojakova's slides Abstract: Initial algebras of polynomial endofunctors are important in computer science because they precisely characterize inductive datatypes — in the presence of extensional equality. If the equality is intensional, as is most often the case with modern formal tools, this correspondence is known to break down since we can no longer prove the uniqueness of recursively-defined functions. Homotopy type theory fixes this drawback — and then some. Inductive types in homotopy type theory enjoy a correspondence with algebras that are homotopy-initial: by definition, the space of morphisms from a homotopy-initial algebra to any other algebra is contractible. Going further, we can show that the space of homotopy-initial algebras for polynomial endofunctors is itself contractible, and hence that any two homotopy-initial algebras automatically satisfy the same type-theoretic properties (equality a la Leibniz).
● David Spivak:	► The polynomial abacus ▼ The polynomial abacus Spivak's slides Abstract: A set-theoretic polynomial functor is naturally a combinatorial object, which might be imagined as an abacus: a collection of columns, each equipped with a set of beads. Moving quickly but with little outside knowledge beyond the Yoneda lemma, I will use these abacuses to very concretely tell the story of P, the framed bicategory of polynomial comonads and bicomodules. In particular, I'll discuss both theory and applications of P. For theory I'll begin with an overview of some pleasing properties enjoyed by the category of polynomials. Then I'll explain Ahman-Uustalu's result that—up to isomorphism—polynomial comonads are categories and Garner's result that the bicomodules between them are parametric right adjoints between the associated copresheaf categories. In particular every copresheaf topos is found as a hom-category in P. I'll also discuss the cofree comonad construction. For applications, I'll recall the notion of Moore machines and show that they are objects in a copresheaf topos C-Set for a particular category C; I'll explain how the story generalizes to arbitrary C. I'll also explain how databases and data migration functors live naturally in this setting. Time permitting I may also discuss how deep learning and cellular automata show up in P.
● Ross Street:	► Polynomials as spans ▼ Polynomials as spans Street's slides Abstract: Often it is useful to place fragments of category theory into the formal context of a bicategory, possibly with extra structure. Apart from isolating the essential concepts, the mechanisms can be applied to other bicategories. My progress on such a program for categorical polynomials will be explained.
● Tarmo Uustalu:	► Polynomial comonads ▼ Polynomial comonads Abstract: I will discuss the category of comonoid objects in the category of polynomials, equivalently, the category of small categories and cofunctors in the sense of Aguiar. I am interested in them as a representation for polynomial comonads and update monads. I am motivated by applications of those in programming semantics. I will discuss a number of constructions with polynomial comonads and what they amount to in terms of small categories and cofunctors.