Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-13T06:49:21.353Z Has data issue: false hasContentIssue false
  • English
  • Français

Polynomial functors and polynomial monads

Published online by Cambridge University Press:  06 September 2012

NICOLA GAMBINO  and
JOACHIM KOCK
NICOLA GAMBINO
Affiliation:
Dipartimento di Matematica e Informatica, Università degli Studi di Palermo, via Archirafi 34, 90123 Palermo, Italy. e-mail: [email protected]
JOACHIM KOCK
Affiliation:
Departament de Matemàtiques, Universitat Autònoma de Barcelona, 08193 Bellaterra (Barcelona), Spain. e-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.

Type
Research Article
Information
Mathematical Proceedings of the Cambridge Philosophical Society , Volume 154 , Issue 1 , January 2013 , pp. 153 - 192
Copyright
Copyright © Cambridge Philosophical Society 2012

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Abbott, M. Categories of containers. Ph.D. thesis. University of Leicester (2003).CrossRefGoogle Scholar
[2]Abbott, M., Altenkirch, T. and Ghani, N.Categories of containers. Foundations of Software Science and Computation Structures (Gordon, A. D., ed.). Lecture Notes in Computer Science, vol. 2620 (Springer, 2003), pp. 23–38.Google Scholar
[3]Abbott, M., Altenkirch, T. and Ghani, N.Representing nested inductive types using W-types. Automata, languages and programming (Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D., eds.) Lecture Notes in Computer Science, vol. 3142. (Springer, Berlin, 2004), pp. 59–71.Google Scholar
[4]Abbott, M., Altenkirch, T. and Ghani, N.Containers: constructing strictly positive types. Theoret. Comput. Sci. 342 (2005), pp. 3–27.CrossRefGoogle Scholar
[5]Altenkirch, T. and Morris, P.Indexed containers. Proceedings of the 24th IEEE Symposium in Logic in Computer Science (LICS 2009), IEEE Computer Society, 2009.CrossRefGoogle Scholar
[6]Baez, J. C. and Dolan, J.Higher-dimensional algebra III. n-categories and the algebra of opetopes. Adv. Math. 135 (1998), pp. 145–206.CrossRefGoogle Scholar
[7]Barr, M. and Wells, C.Toposes Triples and Theories (Springer-Verlag, 1983). Reprinted in Repr. Theory Appl. Categ. 12 (2005), x+288 pp. (electronic).Google Scholar
[8]Bénabou, J.Introduction to bicategories. Reports of the Midwest Category Theory Seminar (Bénabou, J.et al., eds.) Lecture Notes in Math., vol. 47 (Springer-Verlag, 1967), pp. 1–77.Google Scholar
[9]Bergeron, F., Labelle, G. and Leroux, P.Combinatorial Species and Tree-Like Structures (Cambridge University Press, 1998).Google Scholar
[10]Bisson, T. and Joyal, A.The Dyer-Lashof algebra in bordism. C. R. Math. Rep. Acad. Sci. Canada 17 (1995), pp. 135–140.Google Scholar
[11]Brun, M.Witt vectors and Tambara functors. Adv. Math. 193 (2005), pp. 233–256.CrossRefGoogle Scholar
[12]Burroni, A.T-catégories (catégories dans une triple). Cah. Topol. Géom. Différ. Catég. 12 (1971), pp. 215–315.Google Scholar
[13]Carboni, A. and Johnstone, P.Connected limits, familial representability and Artin glueing. Math. Structures Comput. Sci. 5 (1995), 441–459, with Corrigenda in Math. Structures Comput. Sci. 14 (2004), pp. 185–187.CrossRefGoogle Scholar
[14]Diers, Y. Catégories localisables. Ph.D. thesis. Université de Paris VI (1977).Google Scholar
[15]Clairambault, P. and Dybjer, P.The biequivalence of locally Cartesian closed categories and Martin-Löf type theories. Typed lambda calculi and applications. Lecture Notes in Computer Science, vol. 6690. (Springer, 2011), pp. 91–106.Google Scholar
[16]Freyd, P.Aspects of topoi. Bull. Austral. Math. Soc. 7 (1972), pp. 1–76 and pp. 467–480.CrossRefGoogle Scholar
[17]Gambino, N. and Hyland, M.Wellfounded trees and dependent polynomial functors. Types for proofs and programs (Berardi, S., Coppo, M., and Damiani, F., eds.), Lecture Notes in Computer Science, vol. 3085, (Springer, 2004), pp. 210–225.Google Scholar
[18]Girard, J.-Y.Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic 37 (1988), pp. 129–177.CrossRefGoogle Scholar
[19]Grandis, M. and Paré, R.Adjoints for double categories. Addenda to “Limits in double categories”. Cah. Topol. Géom. Différ. Catég. 45 (2004), pp. 193–240.Google Scholar
[20]Grothendieck, A.Revétements étales et groupe fondamental (SGA1). Lecture Notes in Mathematics, vol. 224 (Springer, 1971).CrossRefGoogle Scholar
[21]Hancock, P. and Setzer, A.Interactive programs and weakly final coalgebras in dependent type theory. From sets and types to topology and analysis, Oxford Logic Guides, vol. 48. (Oxford University Press, 2005), pp. 115–136.Google Scholar
[22]Hermida, C.Representable multicategories. Adv. Math. 151 (2000), pp. 164–225.CrossRefGoogle Scholar
[23]Hofmann, M.On the interpretation of type theory in locally Cartesian closed categories. Computer Science Logic (Kasimierz 1994). Lecture Notes in Computer Science, vol. 933 (Springer, 1995), pp. 427–441.Google Scholar
[24]Hyvernat, P. A logical investigation of interaction systems. Ph.D. thesis. Chalmers University (2005).Google Scholar
[25]Jay, C. B.A semantics for shape. Sci. Comput. Programming 25 (1995), pp. 251–283.CrossRefGoogle Scholar
[26]Jay, C. B. and Cockett, J. R. B.Shapely types and shape polymorphism, Programming languages and systems - ESOP '94 (Sannella, D., ed.) Lecture Notes in Computer Science, vol. 788 (Springer, 1994), pp. 302–316.Google Scholar
[27]Johnstone, P.Cartesian monads on toposes. J. Pure Appl. Alg. 116 (1997), pp. 199–220.CrossRefGoogle Scholar
[28]Joyal, A.Une théorie combinatoire des séries formelles. Adv. Math. 42 (1981), pp. 1–82.CrossRefGoogle Scholar
[29]Joyal, A.Foncteurs analytiques et espèces de structures. Combinatoire Énumerative (Montréal/Québec, 1985), Lecture Notes in Math. vol. 1234 (Springer, 1986), pp. 126–159.Google Scholar
[30]Kelly, G. M.A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves and so on. Bull. Austral. Math. Soc. 22 (1980), pp. 1–83.CrossRefGoogle Scholar
[31]Kelly, G. M.Basic concepts of enriched category theory. London Mathematical Society Lecture Note Series, vol. 64 (Cambridge University Press, 1982), Reprinted in Repr. Theory Appl. Categ. 10 (2005), vi+137 pp. (electronic).Google Scholar
[32]Kelly, G. M. and Street, R. H.Review of the elements of 2-categories, Category Seminar (Sydney 1972/1973) (Kelly, G. M., ed.). Lecture Notes in Mathematics, vol. 420 (Springer-Verlag, Berlin, 1974), pp. 75–103.Google Scholar
[33]Kock, A.Strong functors and monoidal monads. Arch. Math. (Basel) 23 (1972), pp. 113–120.CrossRefGoogle Scholar
[34]Kock, A. and Kock, J. Local fibered right adjoints are polynomial. arXiv:1005.4236, 2010, to appear in Math. Struct. Comp. Sci.Google Scholar
[35]Kock, J.Polynomial functors and trees. Internat. Math. Res. Not. 2011 (2011) pp. 609–673.Google Scholar
[36]Kock, J., Joyal, A., Batanin, M. and Mascari, J.-F.Polynomial functors and opetopes. Adv. Math. 224 (2010), pp. 2690–2737.CrossRefGoogle Scholar
[37]Kontsevich, M. and Soibelman, Y.Deformations of algebras over operads and the Deligne conjecture. Conférence Moshé Flato 1999, Vol. I (Dijon) Math. Phys. Stud. vol. 21, (Kluwer Academic Publishers, 2000), pp. 255–307.Google Scholar
[38]Lack, S. and Street, R.The formal theory of monads. II. J. Pure Appl. Alg. 175 (2002), pp. 243–265.CrossRefGoogle Scholar
[39]Lamarche, F. Modelling polymorphism with categories. Ph.D. thesis. McGill University (1988).Google Scholar
[40]Lambek, J.Deductive systems and categories. II. Standard constructions and closed categories. Category Theory, Homology Theory and their Applications, I (Battelle Institute Conference, Seattle, Wash. 1968, Vol. One) (Springer, Berlin, 1969), pp. 76–122.Google Scholar
[41]Mac Lane, S. and Moerdijk, I.Sheaves in Geometry and Logic: a First Introduction to Topos Theory (Springer, New York, 1992).Google Scholar
[42]Leinster, T.A survey of definitions of n-category. Theory Appl. Categ. 10 (2002), pp. 1–70 (electronic).Google Scholar
[43]Leinster, T.Higher operads, higher categories. London Mathematical Society Lecture Note Series, vol. 298 (Cambridge University Press, 2004).CrossRefGoogle Scholar
[44]Macdonald, I. G.Symmetric functions and Hall polynomials. Oxford Mathematical Monographs (The Clarendon Press Oxford University Press, New York, 1979).Google Scholar
[45]Makkai, M. and Reyes, G.First-order categorical logic. Lecture Notes in Mathematics, vol. 611 (Springer-Verlag, Berlin, 1977).CrossRefGoogle Scholar
[46]Manes, E. G. and Arbib, M. A.Algebraic Approaches to Program Semantics (Springer-Verlag, New York, 1986).CrossRefGoogle Scholar
[47]Martins–Ferreira, N.Pseudo-categories. J. Homotopy Relat. Struct. 1 (2006), pp. 47–78.Google Scholar
[48]Moerdijk, I. and Palmgren, E.Wellfounded trees in categories. Ann. Pure Appl. Logic 104 (2000), pp. 189–218.CrossRefGoogle Scholar
[49]Moggi, E., Bellè, G. and Jay, C. B.Monads, shapely functors and transversals. Electron. Notes Theor. Comput. Sci. 29 (1999), pp. 187–208.CrossRefGoogle Scholar
[50]Nordström, B., Petersson, K. and Smith, J. M.Programming in Martin-Löf Type Theory: an Introduction (Oxford University Press, 1990).Google Scholar
[51]Nordström, B., Petersson, K. and Smith, J. M.Martin-Löf Type Theory. Handbook of Logic in Computer Science. Volume V (Abramsky, S., D. Gabbay, M., and Maibaum, T. S. E., eds.) (Oxford University Press, 2001, pp. 1–37).Google Scholar
[52]Petersson, K. and Synek, D.A set constructor for inductive sets in Martin-Löf type theory. Category Theory and Computer Science (Manchester 1989) (Rydeheard, D. E., Dybjer, P., Pitts, A. M., and Poigné, A., eds.). Lecture Notes in Computer Science, vol. 389 (Springer, 1989, pp. 128–140).Google Scholar
[53]Pirashvili, T.Polynomial functors over finite fields (after Franjou, Friedlander, Henn, Lannes, Schwartz, Suslin). Séminaire Bourbaki, Vol. 1999/2000. Astérisque, vol. 276 (Société Mathématique de France, 2002), pp. 369–388.Google Scholar
[54]Seely, R. A. G.Locally cartesian closed categories and type theory. Math. Proc. Camb. Phil. Soc. 95 (1984), pp. 33–48.CrossRefGoogle Scholar
[55]Shulman, M.Framed bicategories and monoidal fibrations. Theory Appl. Categ. 20 (2008), pp. 650–738 (electronic).Google Scholar
[56]Street, R.The formal theory of monads. J. Pure Appl. Alg. 2 (1972), pp. 149–169.CrossRefGoogle Scholar
[57]Street, R.The petit topos of globular sets. J. Pure Appl. Alg. 154 (2000), pp. 299–315.CrossRefGoogle Scholar
[58]Strickland, N. Tambara functors. arXiv:1205.2516, 2012.Google Scholar
[59]Tambara, D.On multiplicative transfer. Comm. Alg. 21 (1993), pp. 1393–1420.CrossRefGoogle Scholar
[60]Taylor, P.Quantitative domains, groupoids and linear logic. Category theory and computer science (Pitt, D. H., Rydeheard, D. E., Dybjer, P., Pitts, A. M., and Poigné, A., eds.) Lecture Notes in Computer Science, vol. 389 (Springer, Berlin, 1989), pp. 155–181.Google Scholar
[61]Weber, M.Generic morphisms, parametric representations and weakly Cartesian monads. Theory Appl. Categ. 13 (2004), pp. 191–234 (electronic).Google Scholar
[62]Weber, M.Familial 2-functors and parametric right adjoints. Theory Appl. Categ. 18 (2007), pp. 665–732 (electronic).Google Scholar
[63]Weber, M. Polynomials in categories with pullbacks. arXiv:1106.1983, 2011.Google Scholar
[64]Zawadowski, M.Lax monoidal fibrations. Models, logics and higher-dimensional categories. (American Mathematical Society, 2011), pp. 341–426.Google Scholar