A cartesian bicategory of polynomial functors in homotopy type theory

Eric Finster, Samuel Mimram, Maxime Lucas, Thomas Seiller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.
Original languageEnglish
Title of host publicationProceedings 37th Conference on Mathematical Foundations of Programming Semantics
EditorsAna Sokolova
PublisherOpen Publishing Association
Pages67-83
Number of pages17
DOIs
Publication statusPublished - 28 Dec 2021
Event37th Conference on Mathematical Foundations of Programming Semantics - Salzburg, Austria
Duration: 30 Aug 20212 Sep 2021
https://easychair.org/cfp/MFPS37

Publication series

NameEPTCS
Volume351
ISSN (Electronic)2075-2180

Conference

Conference37th Conference on Mathematical Foundations of Programming Semantics
Abbreviated titleMFPS37
Country/TerritoryAustria
CitySalzburg
Period30/08/212/09/21
Internet address

Fingerprint

Dive into the research topics of 'A cartesian bicategory of polynomial functors in homotopy type theory'. Together they form a unique fingerprint.

Cite this