Data Types with Symmetries and Polynomial Functors over Groupoids
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Data Types with Symmetries and Polynomial Functors over Groupoids. / Kock, Joachim.
In: Electronic Notes in Theoretical Computer Science, Vol. 286, 24.09.2012, p. 351-365.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Data Types with Symmetries and Polynomial Functors over Groupoids
AU - Kock, Joachim
PY - 2012/9/24
Y1 - 2012/9/24
N2 - Polynomial functors (over Set or other locally cartesian closed categories) are useful in the theory of data types, where they are often called containers. They are also useful in algebra, combinatorics, topology, and higher category theory, and in this broader perspective the polynomial aspect is often prominent and justifies the terminology. For example, Tambara's theorem states that the category of finite polynomial functors is the Lawvere theory for commutative semirings [45], [18].In this talk I will explain how an upgrade of the theory from sets to groupoids (or other locally cartesian closed 2-categories) is useful to deal with data types with symmetries, and provides a common generalisation of and a clean unifying framework for quotient containers (in the sense of Abbott et al.), species and analytic functors (Joyal 1985), as well as the stuff types of Baez and Dolan. The multi-variate setting also includes relations and spans, multispans, and stuff operators. An attractive feature of this theory is that with the correct homotopical approach - homotopy slices, homotopy pullbacks, homotopy colimits, etc. - the groupoid case looks exactly like the set case.After some standard examples, I will illustrate the notion of data-types-with-symmetries with examples from perturbative quantum field theory, where the symmetries of complicated tree structures of graphs play a crucial role, and can be handled elegantly using polynomial functors over groupoids. (These examples, although beyond species, are purely combinatorial and can be appreciated without background in quantum field theory.)Locally cartesian closed 2-categories provide semantics for a 2-truncated version of Martin-Lof intensional type theory. For a fullfledged type theory, locally cartesian closed 8-categories seem to be needed. The theory of these is being developed by David Gepner and the author as a setting for homotopical species, and several of the results exposed in this talk are just truncations of 8-results obtained in joint work with Gepner. Details will appear elsewhere.
AB - Polynomial functors (over Set or other locally cartesian closed categories) are useful in the theory of data types, where they are often called containers. They are also useful in algebra, combinatorics, topology, and higher category theory, and in this broader perspective the polynomial aspect is often prominent and justifies the terminology. For example, Tambara's theorem states that the category of finite polynomial functors is the Lawvere theory for commutative semirings [45], [18].In this talk I will explain how an upgrade of the theory from sets to groupoids (or other locally cartesian closed 2-categories) is useful to deal with data types with symmetries, and provides a common generalisation of and a clean unifying framework for quotient containers (in the sense of Abbott et al.), species and analytic functors (Joyal 1985), as well as the stuff types of Baez and Dolan. The multi-variate setting also includes relations and spans, multispans, and stuff operators. An attractive feature of this theory is that with the correct homotopical approach - homotopy slices, homotopy pullbacks, homotopy colimits, etc. - the groupoid case looks exactly like the set case.After some standard examples, I will illustrate the notion of data-types-with-symmetries with examples from perturbative quantum field theory, where the symmetries of complicated tree structures of graphs play a crucial role, and can be handled elegantly using polynomial functors over groupoids. (These examples, although beyond species, are purely combinatorial and can be appreciated without background in quantum field theory.)Locally cartesian closed 2-categories provide semantics for a 2-truncated version of Martin-Lof intensional type theory. For a fullfledged type theory, locally cartesian closed 8-categories seem to be needed. The theory of these is being developed by David Gepner and the author as a setting for homotopical species, and several of the results exposed in this talk are just truncations of 8-results obtained in joint work with Gepner. Details will appear elsewhere.
KW - Polynomial functors
KW - groupoids
KW - data types
KW - symmetries
KW - species
KW - trees
KW - WELLFOUNDED TREES
KW - CATEGORIES
KW - MODELS
U2 - 10.1016/j.entcs.2013.01.001
DO - 10.1016/j.entcs.2013.01.001
M3 - Journal article
VL - 286
SP - 351
EP - 365
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
SN - 1571-0661
ER -
ID: 331501933