Polynomial functor (type theory)

In type theory, a polynomial functor (or container functor) is a kind of endofunctor of a category of types that is intimately related to the concept of inductive and coinductive types. Specifically, all W-types (resp. M-types) are (isomorphic to) initial algebras (resp. final coalgebras) of such functors.

Polynomial functors have been studied in the more general setting of a pretopos with Σ-types;^[1] this article deals only with the applications of this concept inside the category of types of a Martin-Löf style type theory.

Definition

Let U be a universe of types, let A : U, and let B : A → U be a family of types indexed by A. The pair (A, B) is sometimes called a signature^[2] or a container.^[3] The polynomial functor associated to the container (A, B) is defined as follows:^[4]^[5]^[6]

{\begin{aligned}P:U&\longrightarrow U\\X&\longmapsto \sum _{a:A}(B(a)\to X)\end{aligned}}

Any functor naturally isomorphic to P is called a container functor.^[7] The action of P on functions is defined by

{\begin{aligned}P:(X\to Y)&\longrightarrow (PX\to PY)\\f\qquad &\longmapsto \left((a,g)\mapsto (a,g\circ f)\right)\end{aligned}}

Note that this assignment is only truly functorial in extensional type theories (see #Properties).

Properties

In intensional type theories, such functions are not truly functors, because the universe type is not strictly a category (the field of homotopy type theory is dedicated to exploring how the universe type behaves more like a higher category). However, it is functorial up to propositional equalities, that is, the following identity types are inhabited:

{\begin{aligned}P(f\circ g)&=Pf\circ Pg\\P({\mathsf {id}}_{X})&={\mathsf {id}}_{PX}\end{aligned}}

for any functions f and g and any type X, where ${\mathsf {id}}_{X}$ is the identity function on the type X.^[8]

Inline citations

^ Moerdijk, Ieke; Palmgren, Erik (2000). "Wellfounded trees in categories". Annals of Pure and Applied Logic. 104 (1–3): 189–218. doi:10.1016/s0168-0072(00)00012-9. hdl:2066/129036.
^ Ahrens, Capriotti & Spadotti 2015, Definition 1.
^ Abbott, Altenkirch & Ghani 2005, p. 4.
^ Univalent Foundations Program 2013, Equation 5.4.6.
^ Ahrens, Capriotti & Spadotti 2015, Definition 2.
^ Awodey, Gambino & Sojakova 2012, p. 8.
^ Abbott, Altenkirch & Ghani 2005, p. 10.
^ Awodey, Gambino & Sojakova 2015.

References

Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 4. CiteSeerX 10.1.1.166.34. doi:10.1016/j.tcs.2005.06.002.
Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (2015-04-12). Non-wellfounded trees in Homotopy Type Theory. Leibniz International Proceedings in Informatics (LIPIcs). Vol. 38. pp. 17–30. arXiv:1504.02949. doi:10.4230/LIPIcs.TLCA.2015.17. ISBN 9783939897873. S2CID 15020752.
Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. p. 159.
Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2012-01-18). "Inductive types in homotopy type theory". arXiv:1201.3898 [math.LO].
Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2015-04-21). "Homotopy-initial algebras in type theory". arXiv:1504.05531 [math.LO].

External links

An extensive collection of Notes on Polynomial Functors

Read other articles:

List of Malaysian films of the 2000s

Cinema of Malaysia List of Malaysian filmsList of Malaysian cinemasList of Malaysian animated films pre-1960 1960s 1970s 1980s 1990s 2000s 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010s 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020s 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 vte This is a list of films produced in Malaysia ordered by year of release in the 2000s. For an alphabetical listing of Malaysian films see Category:Malaysian films. 2000 List of Malaysian films...

العلاقات السنغالية الفيتنامية

العلاقات السنغالية الفيتنامية السنغال فيتنام السنغال فيتنام تعديل مصدري - تعديل العلاقات السنغالية الفيتنامية هي العلاقات الثنائية التي تجمع بين السنغال وفيتنام.[1][2][3][4][5] مقارنة بين البلدين هذه مقارنة عامة ومرجعية للدولتين: وجه الم...

ماسايوكي أوشياي (لاعب كرة قدم)

يفتقر محتوى هذه المقالة إلى الاستشهاد بمصادر. فضلاً، ساهم في تطوير هذه المقالة من خلال إضافة مصادر موثوق بها. أي معلومات غير موثقة يمكن التشكيك بها وإزالتها. (مايو 2023) هذه المقالة يتيمة إذ تصل إليها مقالات أخرى قليلة جدًا. فضلًا، ساعد بإضافة وصلة إليها في مقالات متعلقة بها. (�...

Somerset Park

Football stadium in Ayr, Scotland Somerset ParkSan Somerset SomersetView over Somerset ParkSomerset ParkLocation in South AyrshireLocationAyr, ScotlandCoordinates55°28′10″N 4°37′12″W / 55.46944°N 4.62000°W / 55.46944; -4.62000OwnerAyr United F.C. (1920–)Capacity10,185[1] (1,597 seated)Field size110 yd × 72 yd (101 m × 66 m)SurfaceGrassConstructionOpened1888ArchitectArchibald Leitch[2]TenantsAyr F.C. (1888–...

Meitantei Konan Gin-yoku no Majishan

Meitantei Konan Gin-yoku no MajishanSutradaraYasuichiro YamamotoProduserMichihiko SuwaDitulis olehKazunari Kochi[butuh rujukan]Penata musikKatsuo OnoSinematograferTakashi NomuraPenyuntingTerumitsu OkadaDistributorTohoTanggal rilis17 April 2004[1] 7 Maret 2010Durasi108 menitNegara JepangBahasaBahasa JepangPendapatankotor¥2.800.000.000PrekuelCrossroad in the Ancient CapitalSekuelStrategy Above the Depths Meitantei Konan Gin-yoku no Majishan (名探偵コナン　銀翼の...

Myuu Azama

Myuu AzamaKebangsaanJepangNama lainMewPekerjaanaktris, modelTinggi169 m (554 ft 5+1⁄2 in)Situs webhttp://ameblo.jp/mewazama/ Myuu Azama (安座間美優code: ja is deprecated , Azama Myū) lahir 26 Desember 1986 adalah seorang model dan aktris asal Jepang. Dalam Romaji (huruf Latin), namanya juga dieja Mew Azama, dan ditulis dalam tanda tangannya. Ia menjelaskannya dalam profilnya: “ 美優 dibaca 'Mew'. Saya dinamai dari judul lagu Kyoko Koizumi yang terkenal, '...

Riccardo Fedel

«Libero venne ucciso in segreto, dopo che già aveva accettato la rimozione ed era pronto ad andare a combattere altrove. La sua scomparsa ha favorito per decenni un racconto della Resistenza romagnola in cui, a partire dai fecondi rapporti con gli ufficiali britannici, si sono di fatto cancellati i primi mesi della sua attività ed esistenza.» (Marcello Flores - Mimmo Franzinelli, Storia della Resistenza, Laterza, Bari, 2019, p. 459) Riccardo Fedel Riccardo Fedel (Gorizia, 23 agosto 1906 ...

OpenEmbedded

OpenEmbeddedDeveloper(s)75+ developers[1]Repositorygit.openembedded.org/openembedded-core Operating systemLinuxPlatformCross-platformTypeBuild automationLicenseMITWebsitewww.openembedded.org OpenEmbedded is a build automation framework and cross-compile environment used to create Linux distributions for embedded devices.[2] The OpenEmbedded framework is developed by the OpenEmbedded community, which was formally established in 2003. OpenEmbedded is the recommended build system...

Evgenij Giner

Evgenij Lennorovič Giner Evgenij Lennorovič Giner (in russo Евге́ний Ленно́рович Ги́нер?; Kharkiv, 26 maggio 1960) è un imprenditore e dirigente sportivo russo. Presidente del comitato finanziario della Federazione calcistica della Russia[1] è dal febbraio 2001 presidente della squadra di calcio PFC CSKA Moscow. Sotto la sua presidenza il CSKA ha vinto 6 campionati russi (2003, 2005, 2006, 2013, 2014, 2016), 7 coppe di Russia (2002, 2005, 2006, 2008, ...

2008–09 Grimsby Town F.C. season

Grimsby Town 2008–09 football seasonGrimsby Town2008–09 seasonChairmanJohn FentyManagerAlan Buckley(until 15 September 2008)Mike Newell(from 6 October 2008)StadiumBlundell ParkLeague Two22ndFA CupFirst RoundLeague CupSecond RoundLincolnshire Senior CupRunners-upTop goalscorerLeague: Adam Proudlock (8)All: Adam Proudlock (8)Highest home attendance7,095 vs. Aldershot Town (28 March 2009)Lowest home attendance1,858 vs. Tranmere Rovers (12 August 2008) Home colours Away colours Third colours...

Dune short stories

Short stories by Frank Herbert, Brian Herbert, and Kevin J. Anderson The Road to Dune (2005) US 1st edition cover A series of Dune short stories have been written that relate to the Dune novels by Frank Herbert, Brian Herbert and Kevin J. Anderson. Some of these stories were originally available for download from the official Dune website, released in a promotional capacity in conjunction with the Brian Herbert/Kevin J. Anderson novels. Dune: A Whisper of Caladan Seas, Dune: Hunting Harkonnen...

Granite Domes of Yosemite National Park

Yosemite National Park is well known for its granite domes: Sortable table Name of Dome Summit Elevation Clean prominence County Region of Yosemite References Basket Dome 2,320 metres (7,610 ft) 64 metres (210 ft) Mariposa County Yosemite Valley [1] Daff Dome 2,790 metres (9,150 ft) 157 metres (515 ft) Tuolumne County Tuolumne Meadows [2][3] Doda Dome 2,715 metres (8,907 ft) 82 metres (269 ft) Tuolumne County Tuolumne Meadows [4]&...

Математика в Древнем Китае

Треугольник Ян Хуэй (Треугольник Паскаля) с использованием цифр стержня, как показано в публикации Чжу Шицзе в 1303 году н. э. Данная статья — часть обзора История математики. Содержание 1 История 2 Нумерация 3 Основные достижения 4 См. также 5 Примечания 6 Литература 7 Ссылк...

Elections in Burkina Faso

Politics of Burkina Faso Constitution (suspended) Human rights Government Interim President Ibrahim Traoré Interim Prime Minister Apollinaire Joachim Kyélem de Tambèla Parliament National Assembly President: Alassane Bala Sakandé Administrative divisions 13 regions 45 provinces 351 departments Elections Recent elections General: 20152020 Political parties Foreign relations Ministry of Foreign Affairs Minister: Olivia Rouamba Diplomatic missions of / in Burkina Faso Nationality law Passpo...

Conscription and sexism

Discrimination in military enlistment Soviet conscripts, Moscow, 1941 Conscription, sometimes called the draft, is the compulsory enlistment of people in a national service, most often a military service. Men have been subjected to military drafts in most cases. Currently only two countries conscript women and men on the same formal conditions: Norway and Sweden.[1] Opponents of discrimination against men,[2][3]: 102 [who?] including some femini...

Mura di Milano

Mappa di Milano del 1832. Si possono notare le mura spagnole, tracciate in rosso, e la Cerchia dei Navigli lungo la quale si sviluppavano le mura medievali, alla cui corrispondenza era presente il Castello Sforzesco, che è indicato, sulla mappa, in alto a sinistra Le mura di Milano, erette a partire dall'epoca romana a protezione della città, sono state per diversi secoli costituite da tre cinte concentriche: la cinta romana, perfezionata dall'imperatore Massimiano nel IV secolo, quella med...

Miuccia Prada

Miuccia Prada nel 2011 Maria Prada Bianchi[1][2][3][4], detta Miuccia (Milano, 10 maggio 1949), è una stilista e imprenditrice italiana. Nipote di Mario Prada, insieme al marito, Patrizio Bertelli, ha guidato e trasformato Prada in una delle più blasonate case di moda al mondo. Nel 2021, secondo una classifica della rivista Forbes, è la 10° più ricca d'Italia e la 565º al mondo, con un patrimonio di 5,3 miliardi di euro.[5] Indice 1 Biografia 1.1 ...

Unified combatant command

United States Department of Defense command United StatesArmed Forces Executive departments Department of Defense Department of Homeland Security Staff Office of the Secretary of Defense Joint Chiefs of Staff Military departments Department of the Army Department of the Navy Department of the Air Force Military services United States Army United States Marine Corps United States Navy United States Air Force United States Space Force United States Coast Guard Command structure Unified combatan...

Annales (Tacite)

Pour les articles homonymes, voir Annales (homonymie). Incipit des Annales dans l'édition princeps (Venise: Wendelin de Spire, vers 1471/72). Les Annales sont un livre écrit en latin par l'historien romain Tacite. Ces annales couvrent la période des quatre empereurs julio-claudiens qui ont succédé au fondateur de l'Empire romain, l'empereur Auguste. La plus grande partie qui nous est parvenue couvre en particulier les règnes de Tibère et de Néron. Présentation générale Les Annales...

Dick DeBartolo

American writer and podcaster Dick DeBartoloBornOctober 19, 1945 (1945-10-19) (age 78)Brooklyn, New York, U.S.[1]OccupationWriterKnown for Mad writer Match Game question writer Spouse Dennis Wunderlin (m. 2012)[2]Websitegizwiz.biz Dick DeBartolo (born October 19, 1945) is an American writer, most famous for writing for Mad. He is occasionally referred to as Mad's Maddest Writer,[3] this being a twist on Don Martin's former ...

/profillengkap.com/index.php/2012 PS4

List of political ideologies

The AWK Programming Language

1977–78 Yorkshire Football League

Belgia Kanada

New South Wales Heritage Database

Area codes 817 and 682

العلاقات الجزائرية الكينية