{"entities":{"Q2786141":{"pageid":2796879,"ns":120,"title":"Item:Q2786141","lastrevid":58007745,"modified":"2026-04-03T10:37:43Z","type":"item","id":"Q2786141","labels":{"en":{"language":"en","value":"Weak omega-categories from intensional type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5789411"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2786141$0154F0C9-A72E-48D4-AC85-E24DB36F4498","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a74638f4d79dcce8a8db404fcb71ca203d7616c7","datavalue":{"value":{"text":"Weak omega-categories from intensional type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2786141$F986DEFD-5C08-457C-90B2-41AED0E47B66","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aaa1298a480bba2285d5529c8d3977c032962c30","datavalue":{"value":"1250.03127","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2786141$5B25FD0F-C8BE-44F0-97F4-003E624182C3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b44415f8105c365a1bf3319ef10141075e9e9c5d","datavalue":{"value":"10.2168/LMCS-6(3:24)2010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2786141$753E97D6-A910-418C-BBFA-2AF63203B42F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"49e0837564dfa9a6596ab14ab5ec88f3e83b3911","datavalue":{"value":{"entity-type":"item","numeric-id":1785778,"id":"Q1785778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2786141$94FDCD4B-63A3-4A80-9B60-70A0D6CB8FE8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2786141$A07C3DFA-AE71-4397-900E-A5983BC41B92","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"24079ba03437de62c4e6fda5262431b289580da2","datavalue":{"value":{"time":"+2010-09-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2786141$67BE0823-2589-4810-8529-D0CD45E0A2B9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bba1f8d8d98b63ac576df5d6cb0330ba478a7926","datavalue":{"value":"https://arxiv.org/abs/0812.0409","type":"string"},"datatype":"url"},"type":"statement","id":"Q2786141$FA417719-6D9B-4A4E-8424-7FF57ACBC974","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2786141$8853423E-AF02-4431-9763-F21B0320B997","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2786141$27F0D545-C125-47B4-9EB5-FB8D3EEE93E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e9ca7ce31d5d58dbe274220a6e1fb57992f4db59","datavalue":{"value":"18D50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2786141$114C1D91-FC48-426E-9E30-8290357324E2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8183a34660244a42cf71ef7cb072b4665a0bdceb","datavalue":{"value":"5789411","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2786141$344AC1B2-017E-49A9-AF45-5ABFCA206DD2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9e6d307399d40747a7ccf9eafea50adb4f4e5846","datavalue":{"value":"intensional type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$4EEBA515-5F6D-4223-BE9B-6638312BA36E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$36FB38AA-A528-4004-BDD2-D1284CEED153","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb7b45a4a1edbeb4c9f7bae8234defdd2e485bdf","datavalue":{"value":"identity types","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$7764B636-8F51-48CE-BFF7-8C8D6C66D36D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dd004aedfc1f573e3015716a96b77d9d88373031","datavalue":{"value":"higher categories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$4BA3CA6E-9E5C-4A04-B6E5-4FA408F2006D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c034534e5c7579d1f95321dcd2fb1c2d6669b26b","datavalue":{"value":"\\(n\\)-categories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$BFAD08CB-D6ED-43B8-8C00-ABF58DFEDC55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"445bbabfb0ea5116466f74024e770e40ef7773bb","datavalue":{"value":"omega-categories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$95880383-A752-4743-9A3C-FF3141A54740","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1716750e079664e241cb89c90f295b87ba8af9f9","datavalue":{"value":"infinity-categories","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$DAB466E5-7781-41CA-A413-AEA746E0D2A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e6a699a57727d04c80da2ec427cea3f5facb6125","datavalue":{"value":"operads","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$22A88104-0707-4C04-AE3D-6F4B36FB6ACA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cbc29d347a2fb5ab12fe5de5ba7a30a9fdf2916f","datavalue":{"value":"univalent foundations","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$7CE3C70A-956C-40C5-AF0E-6CE43FB72F0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"486173fdea484958e371bcc478b16d274811d71a","datavalue":{"value":"intuitionistic type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$F744BF78-9713-4E60-B1D1-98C99FCFF124","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2786141$B3C1746A-7FED-421C-91BB-9AAF7355FD9B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d4cc9aec43fcb5ff63ecc585a377aa304efbcbfe","datavalue":{"value":"W2951884685","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2786141$F48EB4A4-BE7D-4717-9980-B17240BAD264","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7a2ffd964b52e043cfd16f4cc9576c949491b8fd","datavalue":{"value":"The aim of the paper is to show that for any type in Martin-L\u00f6f intuitionistic type theory, the terms of this type and its higher identity types form a weak \\(\\omega\\)-category in the sense of \\textit{T. Leinster} [Theory Appl. Categ. 10, 1--70 (2002; Zbl 0987.18007)]. In the globular approach to higher categories, the objects of a higher category are \\(0\\)-cells, the arrows between objects are \\(1\\)-cells, there are \\(2\\)-cells considered as arrows between arrows \\(\\mathrm{etc}\\)., all these data subject to appropriate composition operations and laws that depend on the kind of category under consideration (strict or weak, \\(n\\)- or \\(\\omega\\)-). As the author outlines, the paradigm for semantics of type theory is roughly that types (or contexts) are thought of as objects \\([|A|]\\), terms \\(x:A\\vdash \\tau(x):B\\) as arrows \\([|\\tau|]: [|A|]\\rightarrow [|B|]\\), terms of identity type \\(\\rho: \\mathrm{Id}_B(\\tau, \\tau')\\) as \\(2\\)-cells etc.NEWLINENEWLINEDeveloping this idea, the author uses a syntactical approach, { i.e.}, investigation of the structures formed by the syntax of type theory, based on the methods of structural proof theory.NEWLINENEWLINEIt has been suggested earlier (the idea can be traced back to [\\textit{M. Hofmann} and \\textit{T. Streicher}, Oxf. Logic Guides 36, 83--111 (1998; Zbl 0930.03089)]) that the terms of any type considered together with its higher identity types should carry the structure of a weak \\(\\omega\\)-category or an \\(\\omega\\)-groupoid. The paper provides a proof of this hypothesis. It uses the definition of weak \\(\\omega\\)-category by Leinster [loc. cit.] that follows the approach of \\textit{M. A. Batanin} [Adv. Math. 136, No. 1, 39--103 (1998; Zbl 0912.18006)]. A proof of similar results was proposed independently by \\textit{B. van den Berg} and \\textit{R. Garner} [Proc. Lond. Math. Soc. (3) 102, No. 2, 370--394 (2011; Zbl 1229.18007)]. Their proof is based rather on the use of category-theoretical methods. A detailed comparison of the two proofs is given at the end of the present paper.NEWLINENEWLINEBesides the proof of a hypothesis concerning weak \\(\\omega\\)-structure that is of interest in itself, the paper is interesting in the context of recent developments concerning the so-called univalent foundations program (cf. [\\textit{V. Voevodsky}, Lect. Notes Comput. Sci. 7086, 70 (2011; Zbl 1250.03121)]).","type":"string"},"datatype":"string"},"type":"statement","id":"Q2786141$1193D6DE-603F-4CE9-B8D8-2DDA302A600D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"b6c848266fa72da40ff1802d3555a7d072216992","datavalue":{"value":{"entity-type":"item","numeric-id":590478,"id":"Q590478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2786141$266CAFB6-E426-4E5B-BC93-759DFC2A1D3B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e79b722ea90aab36f61f2aa04e9519d48b769557","datavalue":{"value":{"entity-type":"item","numeric-id":3637194,"id":"Q3637194"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22f8462563757c14a683d96fb74ce875cb1fae46","datavalue":{"value":{"amount":"+0.9605472087860109","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2786141$2D8CB9D6-1AA1-438C-89B0-BF9D506CDA5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd907cede99fcb05d765169f91944a60b7a643a7","datavalue":{"value":{"entity-type":"item","numeric-id":3079518,"id":"Q3079518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7075e4c9752d868e9a060170fa6d74805948398a","datavalue":{"value":{"amount":"+0.8824576735496521","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2786141$8A9B31F2-AF8F-4B91-93F5-5083D2894FEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"94186da4403ee8117b593c39f36cde425884c59b","datavalue":{"value":{"entity-type":"item","numeric-id":4649535,"id":"Q4649535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecc3b13691e543fc834e50026f2957d39f97b08d","datavalue":{"value":{"amount":"+0.8778215646743774","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2786141$03564B57-EF36-4883-BD3D-0C1635CC65E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3785f6641bf5329b7361766998a822858a7156a","datavalue":{"value":{"entity-type":"item","numeric-id":5144671,"id":"Q5144671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a0c18d2f86e3060bae1c778d4e356bc8068b4a0d","datavalue":{"value":{"amount":"+0.8379532694816589","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2786141$CB85B640-7661-416B-A7E7-B9DBAB206048","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d3a803e58eb49928f05e4592bc5d0b5a7a777c3","datavalue":{"value":{"entity-type":"item","numeric-id":5094693,"id":"Q5094693"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6499f01301af45003575f95a1df77d92c3d118a0","datavalue":{"value":{"amount":"+0.7796708941459656","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2786141$0E2BB131-4C4B-413A-A23E-4A250322F47A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2786141","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2786141"}}}}}