{"entities":{"Q1689738":{"pageid":1700479,"ns":120,"title":"Item:Q1689738","lastrevid":68242314,"modified":"2026-04-12T22:23:18Z","type":"item","id":"Q1689738","labels":{"en":{"language":"en","value":"Univalence for inverse EI diagrams"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6826931"}},"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":"Q1689738$7944E3A5-15CB-46D3-B6A2-F4D93F9ABBA5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"29a0a542e3e2fbf898126b76b9c160efb1a5ad10","datavalue":{"value":{"text":"Univalence for inverse EI diagrams","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1689738$6F335DDD-C75A-48E8-B8B3-2C976E9B14E6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dd3edf937d045b2af58f41d71213576556323157","datavalue":{"value":"1425.18005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$D5E4A0C6-A228-4B27-B394-BEE990314452","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0aec988e4b31ab0b3fd008867fb1fbedfd6f4bff","datavalue":{"value":{"entity-type":"item","numeric-id":246332,"id":"Q246332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1689738$5F3B7F0A-154A-4976-A0DC-CF18171D6553","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1e22c5b89240190fc74b760088a55141cf0fb60b","datavalue":{"value":{"entity-type":"item","numeric-id":180135,"id":"Q180135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1689738$72D1BAAB-3FD4-4E72-91B9-920048D5BFD9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cbb07437eb9aefda4cafb7f0f71b164b900249e4","datavalue":{"value":{"time":"+2018-01-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1689738$21F9DEA3-1094-4DA4-AA39-1CDB3AA58A2A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c34a6d6cc1ce1ffc1bd6fdb446ea7e21e045b17b","datavalue":{"value":"https://arxiv.org/abs/1508.02410","type":"string"},"datatype":"url"},"type":"statement","id":"Q1689738$8C51093C-42C8-40E3-8A6C-569031023E39","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"54703fa4ecc4a7307e9735aa65395e38116cc0af","datavalue":{"value":"\\textit{Homotopy type theory} [\\textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)] synthesizes intensional constructive type theory [\\textit{P. Martin-L\u00f6f}, Intuitionistic type theory. Napoli: Bibliopolis (1984; Zbl 0571.03030)] with homotopy theory, offering the possibility of making use of type theory as a \\textit{formal syntax} to prove homotopy-theoretic theorems, which would apply automatically to any homotopy theory or \\(\\infty\\)-topos [\\textit{J. Lurie}, Higher topos theory. Princeton, NJ: Princeton University Press (2009; Zbl 1175.18001); \\url{https://faculty.math.illinois.edu/~rezk/homotopy-topos-sketch.pdf}]. It talks concretely about points and paths, which are then compiled by an interpretation theorem to diagrammatic arguments. This paper studies univalence providing a classifying space for all small spaces whose points are literally spaces, making available such technical tools as \\textit{higher inductive types} (a formal language for cell complexes that avoids small object arguments) and Voevodsky's \\textit{univalence axiom}.  Higher inductive types and univalence enable \\textit{synthetic homotopy theory} [\\textit{D. R. Licata} and \\textit{M. Shulman}, in: Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25--28, 2013. Los Alamitos, CA: IEEE Computer Society. 223--232 (2013; Zbl 1369.03097); \\textit{D. R. Licata} and \\textit{G. Brunerie}, Lect. Notes Comput. Sci. 8307, 1--16 (2013; Zbl 1427.03033); \\textit{D. R. Licata} and \\textit{E. Finster}, in: Proceedings of the joint meeting of the twenty-third EACSL annual conference on computer science logic, CSL, and the 2014 29th annual ACM/IEEE symposium on logic in computer science, LICS 2014, Vienna, Austria, July 14--18, 2014. Los Alamitos, CA: IEEE Computer Society. Paper No. 66, 9 p. (2014; Zbl 1395.68249); \\textit{G. Brunerie}, ``On the homotopy groups of spheres in homotopy type theory'', Preprint, \\url{arXiv:1606.05916}; \\textit{K.-B. Hou (Favonia)} et al., in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 565--574 (2016; Zbl 1395.55011)], the last of which was the first genuinely homotopy-theoretic proof of the Blakers-Massey connectivity theorem that applies to any \\(\\infty\\)-topos and that was finally traslated into \\(\\infty\\)-categorical language [\\url{https://faculty.math.illinois.edu/~rezk/freudenthal-and-blakers-massey.pdf}]. However, not all \\(\\infty\\)-toposes are known to model univalence in its usual form, notably for equivariant homotopy theory. The principal objective in this paper is to generalize univalent models of [\\textit{M. Shulman}, Math. Struct. Comput. Sci. 25, No. 5, 1203--1277 (2015; Zbl 1362.03008)] to include classical equivariant homotopy theory over a compact Lie group.  It was shown in [\\textit{A. D. Elmendorf}, Trans. Am. Math. Soc. 277, 275--284 (1983; Zbl 0521.57027)] that \\(G\\)-equivariant homotopy theory is equivalent to the \\(\\infty\\)-topos of diagrams on the orbit category \\(\\mathcal{O}_{G}^{\\mathrm{op}}\\), which is an \\textit{inverse EI \\((\\infty,1)\\)-category} providing that \\(G\\) is a compact Lie group. Therefore, this paper aims to construct a new model category presenting the homotopy theory of presheaves on \\textit{inverse EI \\((\\infty,1)\\)-categories}, which contain universe objects abiding by Voevodsky's univalence axiom. The construction is a generalization of [\\textit{M. Shulman}, Math. Struct. Comput. Sci. 25, No. 5, 1203--1277 (2015; Zbl 1362.03008)] that internalizes in an \\(\\left( \\infty,1\\right) \\)-category, being an iteration of the gluing construction (i.e., comma categories) \\ from [loc. cit.], where this paper generalizes by gluing along hom-functors of internal categories rather than by gluing along matching object functors.  A synopsis of the paper goes as follows.  \\begin{itemize} \\item[\\S 2] recalls basic facts about indexed categories and well-founded recursion.  \\item[\\S 3] studies \\textit{internal inverse categories} in a general context to be specialized both to type theory and homotopy theory.  \\item[\\S \\S 4--6] specialize to homotopy theory, identifying diagrams on such internal categories with previously known models for \\(\\infty\\)-toposes of diagrams.  \\item[\\S 7] specializes to type theory, establishing that internal diagram categories admit models of homotopy type theory with univalence.  \\item[\\S 8] addresses some examples, including equivariant homotopy theory. \\end{itemize}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1689738$676DE814-D2CD-457B-934D-F88BA8175F8E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"50a4d88aaef452ee91d36bc895e7495d5ed6f713","datavalue":{"value":{"entity-type":"item","numeric-id":195143,"id":"Q195143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1689738$A3D25B6B-7A96-4335-AE3E-0910814C8789","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"c71f3ae49cb2a1eeef9914b0fdcd1f33e90aac9c","datavalue":{"value":"18G55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$76339C27-C88B-4A42-93C3-5EA4FA72BD89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$83D7E723-AB9D-4668-9491-51DD2E83BEBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$3FF94326-0423-4CEB-94B6-210F5A134691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"aa2d311bfebadfc58292672011b7418c359f6a26","datavalue":{"value":"18A15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$61D30DE3-A7E1-4868-8F97-C3AE77E393E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"72047dd175f2df177aa1ddf4f7ca150e0c1e70c2","datavalue":{"value":"55U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$2B49D3E5-2391-4159-80D2-954394D544D6","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"da21ea6d9c459037a88dc66df92bd7ed20ac0934","datavalue":{"value":"6826931","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$659522F0-2D61-4C0F-9726-6B7871E57D8B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1689738$D68F71D9-CDD5-49D1-99CE-16EF633CDD65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d3fe3f5ce79cef43b16740889fd3395c13c03fc1","datavalue":{"value":"univalence axiom","type":"string"},"datatype":"string"},"type":"statement","id":"Q1689738$03D74644-338A-4AA7-A0EB-411E2D2DC1F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d2452059af4eefce788199afc211b58ad2a3d0d5","datavalue":{"value":"inverse category","type":"string"},"datatype":"string"},"type":"statement","id":"Q1689738$78CBB1FA-1163-4E49-A812-5BCF072DE0B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6a3cebaf1201c828c4acba7c1f89a7921a418ba","datavalue":{"value":"EI-category","type":"string"},"datatype":"string"},"type":"statement","id":"Q1689738$EEE9AA27-0BB7-4EE3-87CD-1E9D7B0EA7D9","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":"Q1689738$641AA7D0-DC56-4862-AD06-C9D5C02E79A1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"188a436d3e295a385f3ed4be3d1fb2f4a6f9e996","datavalue":{"value":"10.4310/HHA.2017.V19.N2.A12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1689738$BFDD4DAB-8ED3-4997-937F-964F36BA05FE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"936c250e6df014634a63438944ed866ecc7a9168","datavalue":{"value":{"entity-type":"item","numeric-id":5963045,"id":"Q5963045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93f47a95bedef7aefeca0b2f3b50f866157d56db","datavalue":{"value":{"amount":"+0.7745621","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$AE3C15CC-BAAB-4F22-8509-5928A152FA29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20c33c176c1af02c7c955a44f3b4740fff785fa1","datavalue":{"value":{"entity-type":"item","numeric-id":5740656,"id":"Q5740656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ecf2ae45c3ad5d98950413ad1295740318b1e6be","datavalue":{"value":{"amount":"+0.7590331","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$1FC38587-F72F-4AB4-BD4A-08017B5D2CE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67ec9b030401ca7dc1a392d776507f50e8efaae8","datavalue":{"value":{"entity-type":"item","numeric-id":6075425,"id":"Q6075425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"beadc206a0b79ef84199d6bc09b3bf4121ffcb9e","datavalue":{"value":{"amount":"+0.7429607","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$C660ECB9-7448-4D40-9808-AC080FEAE1D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"88dc032ac74caaa33274dc83171569da6ce3a3e0","datavalue":{"value":{"entity-type":"item","numeric-id":2230805,"id":"Q2230805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eadd385179b3ca37deb5185458de220ad3b44c08","datavalue":{"value":{"amount":"+0.72998047","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$AAFF7D34-3D17-4F74-BA58-7050851113F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0f36025c468d9abe1b5322a967f8472527f15a9","datavalue":{"value":{"entity-type":"item","numeric-id":2675950,"id":"Q2675950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"857bd85e12027d6f02a8d75d4fd697b269fc7870","datavalue":{"value":{"amount":"+0.7268431","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$2E2ADB8D-7E32-4ABA-8707-0B79E6D56E39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69bccc653ecc7e1f58ad093de68d34233fde7a1f","datavalue":{"value":{"entity-type":"item","numeric-id":2414596,"id":"Q2414596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82542c26aa0ec5a9f08b2d86954828a2fd01e794","datavalue":{"value":{"amount":"+0.7204151","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$92A3499C-13FA-4979-B276-CB76A3176AE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81df944e21213f59b891323477300d4d84470d54","datavalue":{"value":{"entity-type":"item","numeric-id":3121017,"id":"Q3121017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f445d518bcce65aa249886ccccec8bb3fbeaf9d9","datavalue":{"value":{"amount":"+0.7182092","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$456374A8-8000-4B31-B12E-4B93EA0EFCF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"11e0f7bb7fceb3fadcbe8d2ac5700e675b8c5206","datavalue":{"value":{"entity-type":"item","numeric-id":4611379,"id":"Q4611379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12f144609fb2602289b422b660fdb365fb41517a","datavalue":{"value":{"amount":"+0.7021558","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$F623764B-27E7-451A-B390-7ABB51DC8FD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"310b7eabfcc8a29fa3b19e60ac47d50917382d98","datavalue":{"value":{"entity-type":"item","numeric-id":2125994,"id":"Q2125994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"47545aa9d1967ce0b806ca8623e2abb5b58c35f7","datavalue":{"value":{"amount":"+0.69854593","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$62908533-9364-4EC9-B461-53ADBB1124A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b3442ad616d32779e52660c63c4a8e5689e2d1a","datavalue":{"value":{"entity-type":"item","numeric-id":5277842,"id":"Q5277842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"57ad7783fb05b1c14947f5f88538da44b976a31a","datavalue":{"value":{"amount":"+0.69838977","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1689738$B865C6EB-1A01-416C-877D-8762DEE53FD9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Univalence for inverse EI diagrams","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Univalence_for_inverse_EI_diagrams"}}}}}