होमोटॉपी प्रकार सिद्धांत: Difference between revisions

Revision as of 06:17, 27 May 2023

होमोटॉपी टाइप थ्योरी का कवर: गणित की असमान नींव।

गणितीय तर्क और कंप्यूटर विज्ञान में, होमोटॉपी टाइप थ्योरी (HoTT /hɒt/) अंतर्ज्ञानवादी प्रकार के सिद्धांत के विकास की विभिन्न पंक्तियों को संदर्भित करता है, जो वस्तुओं के रूप में व्याख्या के आधार पर होता है, जिस पर (अमूर्त) होमोटोपी सिद्धांत का अंतर्ज्ञान लागू होता है।

इसमें काम की अन्य पंक्तियों के अलावा, इस प्रकार के सिद्धांतों के लिए होमोटोपिकल और उच्च श्रेणी के सिद्धांत का निर्माण | उच्च-श्रेणीबद्ध मॉडल (गणितीय तर्क) शामिल हैं; अमूर्त समरूपता सिद्धांत और उच्च श्रेणी सिद्धांत के लिए तर्क (या आंतरिक भाषा) के रूप में प्रकार सिद्धांत का उपयोग; गणित के प्रकार-सैद्धांतिक नींव के भीतर गणित का विकास (पहले से मौजूद गणित और नए गणित दोनों को शामिल करना जो होमोटोपिकल प्रकारों को संभव बनाता है); और कंप्यूटर प्रूफ सहायकों में इनमें से प्रत्येक का औपचारिक प्रमाण।

होमोटॉपी प्रकार के सिद्धांत के रूप में संदर्भित कार्य के बीच बड़ा ओवरलैप है, और एकरूप नींव परियोजना के रूप में। हालांकि न तो सटीक रूप से चित्रित किया गया है, और शब्दों को कभी-कभी दूसरे के स्थान पर उपयोग किया जाता है, उपयोग की पसंद भी कभी-कभी दृष्टिकोण और जोर में अंतर से मेल खाती है।^[1] इस प्रकार, यह लेख समान रूप से क्षेत्र के सभी शोधकर्ताओं के विचारों का प्रतिनिधित्व नहीं कर सकता है। इस तरह की परिवर्तनशीलता अपरिहार्य है जब क्षेत्र तेजी से प्रवाह में हो।

इतिहास

प्रागितिहास: groupoid मॉडल

समय में यह विचार कि अंतर्ज्ञानवादी प्रकार के सिद्धांत #Extensional बनाम उनके पहचान प्रकारों के साथ इंटेंसिव को समूह के रूप में माना जा सकता है, गणितीय लोककथा थी। इसे पहली बार मार्टिन हॉफमैन और थॉमस स्ट्रीचर के 1994 के पेपर में सटीक रूप से शब्दार्थ बनाया गया था, जिसे द ग्रुपॉइड मॉडल कहा जाता है, जो पहचान प्रमाणों की विशिष्टता का खंडन करता है,^[2] जिसमें उन्होंने दिखाया कि गहन प्रकार के सिद्धांत का समूह समूह की श्रेणी में मॉडल था। यह टाइप थ्योरी का पहला सही मायने में होमोटोपिकल बीजगणित मॉडल था, यद्यपि केवल 1-आयामी (सेट की श्रेणी में पारंपरिक मॉडल होमोटोपिक रूप से 0-आयामी होते हैं)।

उनका फॉलो-अप पेपर^[3] होमोटॉपी प्रकार के सिद्धांत में बाद के कई विकासों का पूर्वाभास हुआ। उदाहरण के लिए, उन्होंने नोट किया कि ग्रुपॉइड मॉडल नियम को संतुष्ट करता है जिसे उन्होंने ब्रह्मांड विस्तार कहा है, जो कि 1-प्रकार के एकरूपता स्वयंसिद्ध के प्रतिबंध के अलावा और कोई नहीं है जिसे व्लादिमीर वोवोडस्की ने दस साल बाद प्रस्तावित किया था। (1-प्रकार के लिए स्वयंसिद्ध विशेष रूप से तैयार करने के लिए सरल है, हालांकि, समानता की सुसंगत स्थिति धारणा की आवश्यकता नहीं है।) उन्होंने आइसोमोर्फिज्म के साथ श्रेणियों को समानता के रूप में परिभाषित किया और अनुमान लगाया कि ऐसी श्रेणियों के लिए उच्च-आयामी समूह का उपयोग करने वाले मॉडल में किसी के पास समानता होगी समानता है; यह बाद में बेनेडिक्ट अहरेंस, क्रिज़्सटॉफ़ कपुल्किन और माइकल शुलमैन (गणितज्ञ) द्वारा सिद्ध किया गया था।^[4]

प्रारंभिक इतिहास: मॉडल श्रेणियां और उच्च समूह

मॉडल श्रेणी का उपयोग करते हुए 2005 में स्टीव अवोडे और उनके छात्र माइकल वॉरेन द्वारा आकस्मिक प्रकार के सिद्धांत के पहले उच्च-आयामी मॉडल का निर्माण किया गया था। इन परिणामों को पहली बार FMCS 2006 सम्मेलन में सार्वजनिक रूप से प्रस्तुत किया गया था^[5] जिस पर वारेन ने इंटेंसिव टाइप थ्योरी के होमोटॉपी मॉडल शीर्षक से वार्ता दी, जो उनकी थीसिस प्रॉस्पेक्टस के रूप में भी काम करती थी (शोध प्रबंध समिति में अवोडे, निकोला गैम्बिनो और एलेक्स सिम्पसन उपस्थित थे)। सारांश वॉरेन की थीसिस प्रॉस्पेक्टस सार में निहित है।^[6] 2006 में उप्साला विश्वविद्यालय में पहचान प्रकारों के बारे में बाद की कार्यशाला में^[7] गहन प्रकार के सिद्धांत और कारककरण प्रणालियों के बीच संबंध के बारे में दो बातें थीं: रिचर्ड गार्नर द्वारा, प्रकार सिद्धांत के लिए कारककरण प्रणाली,^[8] और माइकल वॉरेन द्वारा, मॉडल श्रेणियां और गहन पहचान प्रकार। संबंधित विचारों पर स्टीव अवोडी, उच्च-आयामी श्रेणियों के प्रकार सिद्धांत, और थॉमस स्ट्रीचर, पहचान प्रकार बनाम कमजोर ओमेगा-ग्रुपोइड्स: कुछ विचार, कुछ समस्याएं द्वारा वार्ता में चर्चा की गई। उसी सम्मेलन में बेन्नो वैन डेन बर्ग ने कमजोर ओमेगा-श्रेणियों के प्रकार नामक वार्ता दी जहां उन्होंने उन विचारों को रेखांकित किया जो बाद में रिचर्ड गार्नर के साथ संयुक्त पत्र का विषय बन गए।

उच्च आयामी मॉडल के सभी प्रारंभिक निर्माणों को निर्भर प्रकार के सिद्धांत के मॉडल के विशिष्ट सुसंगतता की समस्या से निपटना था, और विभिन्न समाधान विकसित किए गए थे। ऐसा ही 2009 में वोवोडस्की द्वारा दिया गया था, दूसरा 2010 में वैन डेन बर्ग और गार्नर द्वारा दिया गया था।^[9] सामान्य समाधान, वोवोडस्की के निर्माण पर निर्माण, अंततः 2014 में लम्सडाइन और वॉरेन द्वारा दिया गया था।^[10] 2007 में PSSL86 में^[11] अवोडे ने होमोटॉपी टाइप थ्योरी शीर्षक से वार्ता दी (यह उस शब्द का पहला सार्वजनिक उपयोग था, जिसे अवोडी ने गढ़ा था^[12]). Awodey और वॉरेन ने अपने परिणामों को पेपर Homotopy Theoretic Models of Identity Types में संक्षेपित किया, जिसे 2007 में ArXiv प्रीप्रिंट सर्वर पर पोस्ट किया गया था^[13] और 2009 में प्रकाशित; 2008 में वॉरेन की थीसिस होमोटॉपी थ्योरिटिक आस्पेक्ट्स ऑफ कंस्ट्रक्टिव टाइप थ्योरी में अधिक विस्तृत संस्करण दिखाई दिया।

लगभग उसी समय, व्लादिमीर वोवोडस्की गणित की व्यावहारिक औपचारिकता के लिए भाषा की खोज के संदर्भ में स्वतंत्र रूप से प्रकार के सिद्धांत की जांच कर रहे थे। सितंबर 2006 में उन्होंने टाइप्स मेलिंग लिस्ट में होमोटॉपी लैम्ब्डा कैलकुलस पर बहुत ही छोटा नोट पोस्ट किया,^[14] जिसने आश्रित उत्पादों, योगों और ब्रह्मांडों के साथ प्रकार के सिद्धांत की रूपरेखा तैयार की और कान सरल सेटों में इस प्रकार के सिद्धांत का मॉडल तैयार किया। यह कहकर शुरू हुआ होमोटॉपी λ-कैलकुलस काल्पनिक (फिलहाल) प्रकार की प्रणाली है और इस समय समाप्त हो गया है, जो मैंने ऊपर कहा है, वह अनुमानों के स्तर पर है। होमोटॉपी श्रेणी में टीएस के मॉडल की परिभाषा भी गैर-तुच्छ है, जो कि 2009 तक हल नहीं किए गए जटिल सुसंगतता के मुद्दों का जिक्र है। इस नोट में समानता प्रकारों की वाक्यात्मक परिभाषा शामिल थी, जिन्हें मॉडल में पथ द्वारा व्याख्या किए जाने का दावा किया गया था- रिक्त स्थान, लेकिन पहचान प्रकारों के लिए प्रति मार्टिन-लोफ के नियमों पर विचार नहीं किया। इसने ब्रह्मांडों को आकार के अलावा होमोटॉपी आयाम द्वारा भी स्तरीकृत किया, ऐसा विचार जिसे बाद में ज्यादातर खारिज कर दिया गया था।

सिंटैक्टिक पक्ष पर, बेन्नो वैन डेन बर्ग ने 2006 में अनुमान लगाया था कि आकस्मिक प्रकार के सिद्धांत में प्रकार के पहचान प्रकार के टावर में ω-श्रेणी की संरचना होनी चाहिए, और वास्तव में माइकल के गोलाकार, बीजगणितीय अर्थ में ω-ग्रुपॉइड होना चाहिए। बटानिन। यह बाद में पेपर में वैन डेन बर्ग और गार्नर द्वारा स्वतंत्र रूप से सिद्ध किया गया था प्रकार कमजोर ओमेगा-ग्रुपोइड्स हैं (प्रकाशित 2008),^[15] और पीटर लम्सडाइन द्वारा पेपर वीक ω-श्रेणियाँ इंटेंशनल टाइप थ्योरी (2009 में प्रकाशित) और उनके 2010 के पीएचडी के हिस्से के रूप में। थीसिस टाइप थ्योरीज़ से उच्च श्रेणियाँ।^[16]

एकरूपता स्वयंसिद्ध, सिंथेटिक होमोटॉपी सिद्धांत, और उच्च आगमनात्मक प्रकार

2006 की शुरुआत में वोएवोडस्की द्वारा असमान कंपन की अवधारणा पेश की गई थी।^[17] हालांकि, संपत्ति पर मार्टिन-लोफ प्रकार के सिद्धांत की सभी प्रस्तुतियों के आग्रह के कारण कि पहचान प्रकार, खाली संदर्भ में, केवल रिफ्लेक्सिविटी हो सकती है, वोवोडस्की ने 2009 तक यह नहीं पहचाना कि इन पहचान प्रकारों का संयोजन में उपयोग किया जा सकता है असमान ब्रह्मांड। विशेष रूप से, यह विचार कि मौजूदा मार्टिन-लोफ प्रकार के सिद्धांत में केवल स्वयंसिद्ध जोड़कर एकरूपता को पेश किया जा सकता है, केवल 2009 में दिखाई दिया।^{[lower-alpha 1]}^{[lower-alpha 2]}

इसके अलावा 2009 में, वोएवोडस्की ने कान परिसरों में टाइप थ्योरी के मॉडल के विवरण के बारे में अधिक काम किया, और देखा कि सार्वभौमिक कैन फाइब्रेशन के अस्तित्व का उपयोग टाइप थ्योरी के श्रेणीबद्ध मॉडल के लिए सुसंगतता की समस्याओं को हल करने के लिए किया जा सकता है। उन्होंने यह भी साबित किया, ए.के. बोसफील्ड के विचार का उपयोग करते हुए, कि यह सार्वभौमिक कंपन एकतरफा था: तंतुओं के बीच जोड़ीदार होमोटॉपी समकक्षों का संबद्ध कंपन आधार के पथ-अंतरिक्ष कंपन के बराबर है।

स्वयंसिद्ध के रूप में एकरूपता तैयार करने के लिए वोवोडस्की ने समतुल्यता को वाक्य-विन्यास के रूप में परिभाषित करने का तरीका खोजा, जिसमें महत्वपूर्ण गुण था कि कथन f का प्रतिनिधित्व करने वाला प्रकार तुल्यता था (फ़ंक्शन विस्तार की धारणा के तहत) (-1) - काट दिया गया (यानी अगर बसा हुआ है) . इसने उन्हें उच्च आयामों के लिए हॉफमैन और स्ट्रीचर की ब्रह्मांड की व्यापकता को सामान्य करते हुए, एकरूपता का वाक्यात्मक कथन देने में सक्षम बनाया। वह प्रूफ सहायक Coq में महत्वपूर्ण मात्रा में सिंथेटिक होमोटॉपी सिद्धांत विकसित करने के लिए समकक्षता और सिकुड़न की इन परिभाषाओं का उपयोग करने में सक्षम था; इसने लाइब्रेरी का आधार बनाया जिसे बाद में फ़ाउंडेशन और अंततः यूनीमैथ कहा गया।^[19] विभिन्न धागों का एकीकरण फरवरी 2010 में कार्नेगी मेलन विश्वविद्यालय में अनौपचारिक बैठक के साथ शुरू हुआ, जहां वोवोडस्की ने कान कॉम्प्लेक्स में अपना मॉडल प्रस्तुत किया और एवोडे, वॉरेन, लम्सडाइन, रॉबर्ट हार्पर (कंप्यूटर वैज्ञानिक), डैन लिकाटा, माइकल सहित समूह को अपना कॉक प्रस्तुत किया। शुलमैन (गणितज्ञ), और अन्य। इस बैठक ने प्रमाण की रूपरेखा तैयार की (वॉरेन, लम्सडाइन, लिकाटा और शुलमैन द्वारा) कि हर होमोटॉपी तुल्यता तुल्यता है (वोवोडस्की के अच्छे सुसंगत अर्थ में), समतुल्यता को आसन्न समकक्षों में सुधार के श्रेणी सिद्धांत के विचार पर आधारित है। इसके तुरंत बाद, वोएवोडस्की ने साबित कर दिया कि यूनीवैलेंस एक्सिओम का तात्पर्य कार्य विस्तार से है।

अगली महत्वपूर्ण घटना मार्च 2011 में ओबेरवॉल्फ के गणितीय अनुसंधान संस्थान में स्टीव अवोडे, रिचर्ड गार्नर, प्रति मार्टिन-लोफ और व्लादिमीर वोवोडस्की द्वारा आयोजित मिनी-कार्यशाला थी, जिसका शीर्षक रचनात्मक प्रकार के सिद्धांत की होमोटॉपी व्याख्या थी।^[20] इस कार्यशाला के लिए Coq ट्यूटोरियल के भाग के रूप में, Andrej Bauer ने छोटी Coq लाइब्रेरी लिखी^[21] वोवोद्स्की के विचारों पर आधारित (लेकिन वास्तव में उनके किसी भी कोड का उपयोग नहीं); यह अंततः HoTT Coq लाइब्रेरी के पहले संस्करण का कर्नेल बन गया^[22] (बाद की पहली प्रतिबद्धता^[23] माइकल शुलमैन ने लेडी बाउर की फाइलों पर आधारित विकास को नोट किया है, जिसमें व्लादिमीर वोवोडस्की की फाइलों से लिए गए कई विचार हैं)। लम्सडाइन, शुलमैन, बाउर और वॉरेन के कारण, ओबेरवॉल्फ़ बैठक से निकलने वाली सबसे महत्वपूर्ण चीजों में से उच्च आगमनात्मक प्रकारों का मूल विचार था। प्रतिभागियों ने महत्वपूर्ण खुले प्रश्नों की सूची भी तैयार की, जैसे कि क्या यूनीवैलेंस एक्सिओम कैननिसिटी को संतुष्ट करता है (अभी भी खुला है, हालांकि कुछ विशेष मामलों को सकारात्मक रूप से हल किया गया है)^[24]^[25]), क्या एकरूपता स्वयंसिद्ध में गैरमानक मॉडल हैं (चूंकि शुलमैन द्वारा सकारात्मक उत्तर दिया गया है), और कैसे (अर्ध) सरल प्रकारों को परिभाषित किया जाए (अभी भी एमएलटीटी में खुला है, हालांकि यह वोवोडस्की के होमोटॉपी टाइप सिस्टम (एचटीएस) में किया जा सकता है, प्रकार सिद्धांत के साथ दो समानता प्रकार)।

ओबेरवॉल्फ़ कार्यशाला के तुरंत बाद, होमोटॉपी टाइप थ्योरी वेबसाइट और ब्लॉग^[26] स्थापित किया गया था, और यह विषय उसी नाम से लोकप्रिय होने लगा। इस अवधि के दौरान हुई कुछ महत्वपूर्ण प्रगति का अंदाजा ब्लॉग इतिहास से लगाया जा सकता है।^[27]

असमान नींव

मुहावरा असमान नींव सभी के द्वारा होमोटॉपी प्रकार के सिद्धांत से निकटता से संबंधित होने के लिए सहमत है, लेकिन हर कोई इसे उसी तरह से उपयोग नहीं करता है। यह मूल रूप से व्लादिमीर वोएवोडस्की द्वारा गणित के लिए मूलभूत प्रणाली के अपने दृष्टिकोण को संदर्भित करने के लिए उपयोग किया गया था जिसमें मूल वस्तुएं होमोटॉपी प्रकार हैं, प्रकार के सिद्धांत पर आधारित #The_univalence_axiom |^[28] जैसा कि वोवोद्स्की का काम होमोटोपी प्रकार के सिद्धांत पर काम कर रहे अन्य शोधकर्ताओं के समुदाय के साथ एकीकृत हो गया, कभी-कभी असमान नींव को होमोटॉपी प्रकार के सिद्धांत के साथ दूसरे के रूप में इस्तेमाल किया जाता था,^[29] और अन्य समय केवल मूलभूत प्रणाली के रूप में इसके उपयोग को संदर्भित करने के लिए (उदाहरण के लिए, मॉडल-श्रेणीबद्ध शब्दार्थ या कम्प्यूटेशनल मेटाथ्योरी के अध्ययन को छोड़कर)।^[30] उदाहरण के लिए, IAS विशेष वर्ष के विषय को आधिकारिक तौर पर एकतरफा नींव के रूप में दिया गया था, हालांकि वहां किए गए बहुत से काम नींव के अलावा शब्दार्थ और मेटाथ्योरी पर केंद्रित थे। आईएएस कार्यक्रम में भाग लेने वालों द्वारा तैयार की गई पुस्तक का शीर्षक होमोटॉपी टाइप थ्योरी: यूनिवैलेंट फाउंडेशन्स ऑफ मैथमैटिक्स; हालांकि यह या तो उपयोग को संदर्भित कर सकता है, क्योंकि पुस्तक केवल HoTT को गणितीय आधार के रूप में चर्चा करती है।^[29]

गणित के यूनिवैलेंट फाउंडेशन पर विशेष वर्ष

यूनीवेलेंट फ़ाउंडेशन स्पेशल ईयर प्रोजेक्ट में प्रतिभागियों द्वारा GitHub रिपॉजिटरी पर HoTT बुक के विकास को दर्शाने वाला एनीमेशन।

2012-13 में उन्नत अध्ययन संस्थान के शोधकर्ताओं ने गणित के यूनिवेलेंट फाउंडेशन पर विशेष वर्ष आयोजित किया।^[31] विशेष वर्ष ने टोपोलॉजी, कंप्यूटर विज्ञान, श्रेणी सिद्धांत और गणितीय तर्क में शोधकर्ताओं को साथ लाया। कार्यक्रम का आयोजन स्टीव अवोडे, थिएरी कोक्वांड और व्लादिमीर वोवोडस्की द्वारा किया गया था।

कार्यक्रम के दौरान, पीटर एक्ज़ेल, जो प्रतिभागियों में से थे, ने कार्य समूह की शुरुआत की, जिसने जांच की कि टाइप थ्योरी को अनौपचारिक रूप से लेकिन कठोरता से कैसे किया जाए, शैली में जो सामान्य गणितज्ञों के सेट थ्योरी के अनुरूप है। प्रारंभिक प्रयोगों के बाद यह स्पष्ट हो गया कि यह न केवल संभव था बल्कि अत्यधिक लाभदायक था, और यह कि पुस्तक (तथाकथित HoTT Book)^[29]^[32] लिखा जा सकता है और लिखा जाना चाहिए। परियोजना के कई अन्य प्रतिभागी तब तकनीकी सहायता, लेखन, प्रूफ रीडिंग और विचारों की पेशकश के प्रयास में शामिल हुए। असामान्य रूप से गणित पाठ के लिए, इसे सहयोगी रूप से विकसित किया गया था और गिटहब पर खुले में, क्रिएटिव कामन्स लाइसेंस के तहत जारी किया गया है जो लोगों को पुस्तक के अपने स्वयं के संस्करण को फोर्क (सॉफ्टवेयर विकास) करने की अनुमति देता है, और प्रिंट और डाउनलोड दोनों में मुफ्त में खरीदा जा सकता है। शुल्क।^[33]^[34]^[35]

अधिक सामान्यतः, विशेष वर्ष संपूर्ण विषय के विकास के लिए उत्प्रेरक था; होटटी बुक केवल थी, यद्यपि सबसे अधिक दिखाई देने वाला, परिणाम।

विशेष वर्ष में आधिकारिक प्रतिभागियों

पीटर एक्ज़ेल
बेनेडिक्ट अहरेंस
थॉर्स्टन अलटेनकिर्च
स्टीव अवोडे
ब्रूनो बारास
लेडी बाउर
यवेस बर्टोट
मार्क बेजेम
थिएरी कोक्वांड
एरिक फिनस्टर
डेनियल ग्रेसन
ह्यूगो हर्बेलिन
आंद्रे जोयल
डैन लिकाटा
पीटर लम्सडाइन
असिया महबूबी
प्रति मार्टिन-लोफ
सर्गेई मेलिखोव
अलवारो पेलायो
एंड्रयू पोलोनस्की
माइकल शुलमैन (गणितज्ञ)
मैथ्यू सोज़्यू
बास स्पिटर्स
बेन्नो वैन डेन बर्ग
व्लादिमीर वोवोडस्की
माइकल वॉरेन
नोम ज़ेलबर्गर

ACM कम्प्यूटिंग समीक्षा ने पुस्तक को कंप्यूटिंग के गणित श्रेणी में उल्लेखनीय 2013 प्रकाशन के रूप में सूचीबद्ध किया।^[36]

मुख्य अवधारणाएँ

Intensional type theory	Homotopy theory
types $A$	spaces $A$
terms $a$	points $a$
$a:A$	$a\in A$
dependent type $x:A\ \vdash \ B(x)\$	fibration $B\to A$
identity type $\mathrm {Id} _{A}(a,b)$	path space
$p:\mathrm {Id} _{A}(a,b)$	path $p:a\to b$
$\alpha :\mathrm {Id} _{\mathrm {Id} _{A}(a,b)}(p,q)$	homotopy $\alpha :p\Rightarrow q$

प्रकार के रूप में प्रस्ताव

HoTT प्रकार सिद्धांत के प्रकार सिद्धांत व्याख्या के रूप में प्रस्तावों के संशोधित संस्करण का उपयोग करता है, जिसके अनुसार प्रकार भी प्रस्तावों का प्रतिनिधित्व कर सकते हैं और शर्तें तब सबूतों का प्रतिनिधित्व कर सकती हैं। HoTT में, हालांकि, प्रकार के रूप में मानक प्रस्तावों के विपरीत, 'मात्र प्रस्तावों' द्वारा विशेष भूमिका निभाई जाती है, जो कि, मोटे तौर पर बोलना, वे प्रकार होते हैं जिनमें प्रस्तावात्मक समानता तक अधिकतम शब्द होता है। ये सामान्य प्रकार की तुलना में पारंपरिक तार्किक प्रस्तावों की तरह अधिक हैं, जिसमें वे प्रमाण-अप्रासंगिक हैं।

समानता

समरूपता प्रकार के सिद्धांत की मौलिक अवधारणा पथ (टोपोलॉजी) है। HoTT में, type $a=b$ बिंदु से सभी पथों का प्रकार है $a$ मुद्दे पर $b$ . (इसलिए, सबूत है कि बिंदु $a$ बिंदु के बराबर है $b$ बिंदु से पथ के समान ही है $a$ मुद्दे पर $b$ ।) किसी भी बिंदु के लिए $a$ , प्रकार का पथ मौजूद है $a=a$ समानता की रिफ्लेक्सिव संपत्ति के अनुरूप। प्रकार का मार्ग $a=b$ उलटा जा सकता है, प्रकार का मार्ग बना सकता है $b=a$ समानता की सममित संपत्ति के अनुरूप। प्रकार के दो रास्ते $a=b$ सम्मान। $b=c$ प्रकार का मार्ग बनाते हुए, समाप्‍त किया जा सकता है $a=c$ ; यह समानता की सकर्मक संपत्ति के अनुरूप है।

सबसे महत्वपूर्ण बात, रास्ता दिया $p:a=b$ , और कुछ संपत्ति का प्रमाण $P(a)$ , सबूत को रास्ते में ले जाया जा सकता है $p$ संपत्ति का प्रमाण देने के लिए $P(b)$ . (समकक्ष रूप से कहा गया है, प्रकार का वस्तु $P(a)$ प्रकार की वस्तु में परिवर्तित किया जा सकता है $P(b)$ .) यह प्रथम-क्रम तर्क#समानता और इसके स्वयंसिद्धों के अनुरूप है। यहाँ, HoTT और शास्त्रीय गणित के बीच महत्वपूर्ण अंतर आता है। शास्त्रीय गणित में, बार दो मूल्यों की समानता $a$ और $b$ स्थापित हो गया है, $a$ और $b$ इसके बाद उनके बीच किसी भी तरह के अंतर के संबंध में दूसरे के लिए इस्तेमाल किया जा सकता है। होमोटॉपी प्रकार के सिद्धांत में, हालांकि, कई अलग-अलग रास्ते हो सकते हैं $a=b$ , और किसी वस्तु को दो अलग-अलग रास्तों से ले जाने से दो अलग-अलग परिणाम मिलेंगे। इसलिए, होमोटॉपी प्रकार के सिद्धांत में, प्रतिस्थापन संपत्ति को लागू करते समय, यह बताना आवश्यक है कि किस पथ का उपयोग किया जा रहा है।

सामान्य तौर पर, प्रस्ताव में कई अलग-अलग प्रमाण हो सकते हैं। (उदाहरण के लिए, सभी प्राकृतिक संख्याओं का प्रकार, जब प्रस्ताव के रूप में माना जाता है, तो प्रत्येक प्राकृतिक संख्या प्रमाण के रूप में होती है।) भले ही प्रस्ताव के पास केवल प्रमाण हो $a$ , रास्तों का स्थान $a=a$ किसी तरह गैर-तुच्छ हो सकता है। मात्र प्रस्ताव किसी भी प्रकार का होता है जो या तो खाली होता है, या केवल बिंदु होता है जिसमें तुच्छ पथ स्थान (बीजगणितीय टोपोलॉजी) होता है।

ध्यान दें कि लोग लिखते हैं $a=b$ के लिए $Id_{A}(a,b)$ , इस प्रकार प्रकार छोड़ रहा है $A$ का $a,b$ अंतर्निहित। इसके साथ भ्रमित न हों $id_{A}:A\to A$ , पर पहचान समारोह को दर्शाते हुए $A$ .^{[lower-alpha 3]}

तुल्यता टाइप करें

दो प्रकार $A$ और $B$ किसी ब्रह्मांड से संबंधित $U$ समकक्ष होने के रूप में परिभाषित किया गया है यदि उनके बीच समानता मौजूद है। समानता कार्य है

f:A\to B

जिसमें बाएँ प्रतिलोम और दाएँ प्रतिलोम दोनों हैं, इस अर्थ में कि उपयुक्त रूप से चुना गया है $g$ और $h$ निम्नलिखित प्रकार दोनों आबाद हैं:

Id_{B\rightarrow B}(f\circ g,id_{B}),

Id_{A\rightarrow A}(h\circ f,id_{A}).

अर्थात।

f\circ g=_{B\rightarrow B}id_{B},

h\circ f=_{A\rightarrow A}id_{A}.

यह सामान्य धारणा व्यक्त करता है

f

समानता प्रकारों का उपयोग करते हुए बाएं उलटा और दायां उलटा दोनों होता है। ध्यान दें कि उपरोक्त उलटापन की स्थिति फ़ंक्शन प्रकारों में समानता प्रकार है

A\rightarrow A

और

B\rightarrow B

. आम तौर पर फ़ंक्शन विस्तारात्मक स्वयंसिद्ध मानता है, जो यह सुनिश्चित करता है कि ये निम्न प्रकारों के बराबर हैं जो डोमेन और कोडोमेन पर समानता का उपयोग करके इन्वर्टिबिलिटी व्यक्त करते हैं

A

और

B

:

\Pi _{y:B}.\ Id_{B}((f\circ g)(y),id_{B}(y)),

\Pi _{x:A}.\ Id_{A}((h\circ f)(x),id_{A}(x)).

यानी सभी के लिए

x:A

और

y:B

,

f(g(y))=_{B}y,

h(f(x))=_{A}x.

प्रकार के कार्य

A\to B

साथ प्रमाण के साथ कि वे तुल्यताएँ हैं, द्वारा निरूपित किया जाता है

A\simeq B

.

एकरूपता स्वयंसिद्ध

ऊपर बताए गए समतुल्य कार्यों को परिभाषित करने के बाद, कोई यह दिखा सकता है कि रास्तों को समानताओं में बदलने का विहित तरीका है। दूसरे शब्दों में, प्रकार का कार्य है

(A=B)\to (A\simeq B),

जो उस प्रकार को व्यक्त करता है $A,B$ जो समान हैं, विशेष रूप से, समतुल्य भी हैं।

यूनीवैलेंस एक्सिओम कहता है कि यह फंक्शन अपने आप में इक्वैलेंस है।^[29]^: 115^[18]^: 4–6 इसलिए, हमारे पास है

(A=B)\simeq (A\simeq B)

दूसरे शब्दों में, पहचान समानता के बराबर है। विशेष रूप से, कोई कह सकता है कि 'समतुल्य प्रकार समान हैं'।^[29]^: 4

मार्टिन होट्ज़ेल एस्कार्डो ने दिखाया है कि मार्टिन-लोफ टाइप थ्योरी (एमएलटीटी) की समानता की संपत्ति स्वतंत्रता (गणितीय तर्क) है।^[18]^: 6^{[lower-alpha 4]}

अनुप्रयोग

प्रमेय सिद्ध करना

अधिवक्ताओं का दावा है कि HoTT गणितीय प्रमाणों को कंप्यूटर प्रूफ सहायकों के लिए पहले की तुलना में बहुत आसानी से कंप्यूटर प्रोग्रामिंग भाषा में अनुवादित करने की अनुमति देता है। उनका तर्क है कि यह दृष्टिकोण कंप्यूटर के लिए कठिन प्रमाणों की जांच करने की क्षमता को बढ़ाता है।^[37] हालाँकि, इन दावों को सार्वभौमिक रूप से स्वीकार नहीं किया जाता है और कई शोध प्रयास और प्रूफ सहायक HoTT का उपयोग नहीं करते हैं।

HoTT एकरूपता सिद्धांत को अपनाता है, जो तार्किक-गणितीय प्रस्तावों की समानता को होमोटॉपी सिद्धांत से संबंधित करता है। समीकरण जैसे a=b गणितीय प्रस्ताव है जिसमें दो अलग-अलग प्रतीकों का समान मान होता है। होमोटॉपी प्रकार के सिद्धांत में, इसका अर्थ यह लिया जाता है कि दो आकृतियाँ जो प्रतीकों के मूल्यों का प्रतिनिधित्व करती हैं, सांस्थितिक रूप से समतुल्य हैं।^[37]

ईटीएच ज्यूरिख इंस्टीट्यूट फॉर थियोरेटिकल स्टडीज के निदेशक जॉन फेल्डर का तर्क है कि ये समतुल्य संबंध, होमोटोपी सिद्धांत में बेहतर रूप से तैयार किए जा सकते हैं क्योंकि यह अधिक व्यापक है: होमोटॉपी सिद्धांत न केवल बताता है कि ए बराबर बी क्यों है बल्कि यह भी बताता है कि इसे कैसे प्राप्त किया जाए। सेट थ्योरी में, इस जानकारी को अतिरिक्त रूप से परिभाषित करना होगा, जो अधिवक्ताओं का तर्क है, प्रोग्रामिंग भाषाओं में गणितीय प्रस्तावों के अनुवाद को और अधिक कठिन बना देता है।^[37]

कंप्यूटर प्रोग्रामिंग

2015 तक, होमोटोपी प्रकार के सिद्धांत में यूनीवैलेंस एक्सिओम के कम्प्यूटेशनल व्यवहार को मॉडल और औपचारिक रूप से विश्लेषण करने के लिए गहन शोध कार्य चल रहा था।^[38] क्यूबिकल प्रकार का सिद्धांत होमोटॉपी प्रकार के सिद्धांत को कम्प्यूटेशनल सामग्री देने का प्रयास है।^[39] हालाँकि, यह माना जाता है कि कुछ वस्तुएँ, जैसे अर्ध-सरल प्रकार, सटीक समानता की कुछ धारणा के संदर्भ के बिना निर्मित नहीं की जा सकती हैं। इसलिए, विभिन्न दो-स्तरीय प्रकार के सिद्धांत विकसित किए गए हैं जो उनके प्रकारों को तंतुमय प्रकारों में विभाजित करते हैं, जो पथों का सम्मान करते हैं, और गैर-तंतुमय प्रकार, जो नहीं करते हैं। कार्टेशियन क्यूबिकल कम्प्यूटेशनल टाइप थ्योरी पहला दो-स्तरीय टाइप थ्योरी है जो होमोटॉपी टाइप थ्योरी को पूर्ण कम्प्यूटेशनल व्याख्या देता है।^[40]

यह भी देखें

निर्माण की गणना
करी-हावर्ड पत्राचार
अंतर्ज्ञानवादी प्रकार का सिद्धांत
होमोटॉपी परिकल्पना
असमान नींव

↑ Univalence is a type, a property of the identity type IdU of a universe U —Martín Hötzel Escardó (2018)^[18]^: p.1
↑ "Univalence is a type, and the univalence axiom says that this type has some inhabitant."^[18]^: p.1
↑ Here the type theory convention is used, that type names begin with a capitalized letter, but that function names begin with a lower-case letter.
↑ Martín Hötzel Escardó has shown that the property of univalence, "a property of the identity type IdU of a universe U",^[18]^: 4 may or may not have an inhabitant. By the Univalence Axiom the type 'isUnivalent(U)' has an inhabitant; Hötzel Escardó notes that when reflection is the only way to construct elements of the identity type, other than univalence, one may construct a function J from the identity type, from reflection, and from J.^[18]^{: 2.4 The identity type} Hötzel Escardó proceeds to construct the univalence type, using repeated applications of J. When 'all types are sets' (denoted Axiom K),^[18]^: 2.4 Axiom K implies the type 'isUnivalent(U)' does not have an inhabitant. Thus Hötzel Escardó finds the type 'isUnivalent(U)' is undecided in Martin-Löf Type Theory (MLTT).^[18]^{: 3.2, p.6 The Univalence Axiom}

संदर्भ

↑ Shulman, Michael (2016-01-27). "Homotopy Type Theory: A synthetic approach to higher equalities". arXiv:1601.05035v3 [math.LO]., footnote 1
↑ Hofmann, M.; Streicher, T. (1994). "Groupoid मॉडल पहचान प्रमाणों की विशिष्टता का खंडन करता है". Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science: 208–212. doi:10.1109/LICS.1994.316071. ISBN 0-8186-6310-3. S2CID 19496198.
↑ Hofmann, Martin; Streicher, Thomas (1998). "The groupoid interpretation of type theory". In Sambin, Giovanni; Smith, Jan M. (eds.). रचनात्मक प्रकार के सिद्धांत के पच्चीस वर्ष. Oxford Logic Guides. Vol. 36. Clarendon Press. pp. 83–111. ISBN 978-0-19-158903-4. MR 1686862.
↑ Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael (2015). "असमान श्रेणियां और Rezk पूर्णता". Mathematical Structures in Computer Science. 25 (5): 1010–1039. arXiv:1303.0584. doi:10.1017/S0960129514000486. MR 3340533. S2CID 1135785.
↑ "Foundational Methods in Computer Science 2006, University of Calgary, June 7th - 9th, 2006". University of Calgary. Retrieved 6 June 2021.
↑ Warren, Michael A. (2006). इंटेंशनल टाइप थ्योरी के होमोटॉपी मॉडल (PDF) (Thesis).
↑ "Identity Types - Topological and Categorical Structure, Workshop, Uppsala, November 13-14, 2006". Uppsala University - Department of Mathematics. Retrieved 6 June 2021.
↑ Richard Garner, Factorisation axioms for type theory
↑ Berg, Benno van den; Garner, Richard (27 July 2010). "पहचान प्रकारों के सामयिक और सरल मॉडल". arXiv:1007.4638 [math.LO].
↑ Lumsdaine, Peter LeFanu; Warren, Michael A. (6 November 2014). "The local universes model: an overlooked coherence construction for dependent type theories". ACM Transactions on Computational Logic. 16 (3): 1–31. arXiv:1411.1736. doi:10.1145/2754931. S2CID 14068103.
↑ "86th edition of the Peripatetic Seminar on Sheaves and Logic, Henri Poincaré University, September 8-9, 2007". loria.fr. Archived from the original on 17 December 2014. Retrieved 20 December 2014.
↑ Preliminary list of PSSL86 participants
↑ Awodey, Steve; Warren, Michael A. (3 September 2007). "पहचान प्रकारों के होमोटॉपी सैद्धांतिक मॉडल". Mathematical Proceedings of the Cambridge Philosophical Society. 146 (1): 45. arXiv:0709.0248. Bibcode:2008MPCPS.146...45A. doi:10.1017/S0305004108001783. S2CID 7915709.
↑ Voevodsky, Vladimir (27 September 2006). "A very short note on homotopy λ-calculus". ucr.edu. Retrieved 6 June 2021.
↑ van den Berg, Benno; Garner, Richard (1 December 2007). "प्रकार कमजोर ओमेगा-ग्रुपॉइड हैं". Proceedings of the London Mathematical Society. 102 (2): 370–394. arXiv:0812.0298. doi:10.1112/plms/pdq026. S2CID 5575780.
↑ Lumsdaine, Peter (2010). "टाइप थ्योरी से उच्च श्रेणियाँ" (PDF) (Ph.D.). Carnegie Mellon University.
↑ Notes on homotopy lambda calculus, March 2006
↑ ^18.0 ^18.1 ^18.2 ^18.3 ^18.4 ^18.5 ^18.6 ^18.7 Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom
↑ GitHub repository, Univalent Mathematics
↑ Awodey, Steve; Garner, Richard; Martin-Löf, Per; Voevodsky, Vladimir (27 February – 5 March 2011). "Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory" (PDF). Oberwolfach Reports. Mathematical Research Institute of Oberwolfach: 609–638. doi:10.4171/OWR/2011/11. Retrieved 6 June 2021.
↑ GitHub repository, Andrej Bauer, Homotopy theory in Coq
↑ Bauer, Andrej; Voevodsky, Vladimir (29 April 2011). "बेसिक होमोटॉपी टाइप थ्योरी". GitHub. Retrieved 6 June 2021.
↑ GitHub repository, Homotopy type theory
↑ Shulman, Michael (2015). "व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता". Mathematical Structures in Computer Science. 25 (5): 1203–1277. arXiv:1203.3253. doi:10.1017/S0960129514000565. S2CID 13595170.
↑ Licata, Daniel R.; Harper, Robert (21 July 2011). "Canonicity for 2-Dimensional Type Theory" (PDF). Carnegie Mellon University. Retrieved 6 June 2021.
↑ Homotopy Type Theory and Univalent Foundations Blog
↑ Homotopy Type Theory blog
↑ Type Theory and Univalent Foundations
↑ ^29.0 ^29.1 ^29.2 ^29.3 ^29.4 Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.
↑ Homotopy Type Theory: References
↑ IAS school of mathematics: Special Year on The Univalent Foundations of Mathematics
↑ Official announcement of The HoTT Book, by Steve Awodey, 20 June 2013
↑ Monroe, D (2014). "A New Type of Mathematics?". Comm ACM. 57 (2): 13–15. doi:10.1145/2557446. S2CID 6120947.
↑ Shulman, Mike (20 June 2013). "एचओटीटी बुक". The n-Category Café. Retrieved 6 June 2021 – via University of Texas.
↑ Bauer, Andrej (20 June 2013). "एचओटीटी बुक". Mathematics and Computation. Retrieved 6 June 2021.
↑ ACM Computing Reviews. "Best of 2013".
↑ ^37.0 ^37.1 ^37.2 Meyer, Florian (3 September 2014). "गणित के लिए एक नई नींव". R&D Magazine. Retrieved 29 July 2021.
↑ Sojakova, Kristina (2015). होमोटोपी-प्रारंभिक बीजगणित के रूप में उच्च आगमनात्मक प्रकार. POPL 2015. arXiv:1402.0761. doi:10.1145/2676726.2676983.
↑ Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2015). Cubical Type Theory: a constructive interpretation of the univalence axiom. TYPES 2015.
↑ Anguili, Carlo; Favonia; Harper, Robert (2018). Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities (PDF). Computer Science Logic 2018. Retrieved 26 Aug 2018. (to appear)

ग्रन्थसूची

The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Princeton, NJ: Institute for Advanced Study. MR 3204653. (GitHub version cited in this article.)
Awodey, S.; Warren, M. A. (January 2009). "Homotopy Theoretic Models of Identity Types". Mathematical Proceedings of the Cambridge Philosophical Society. 146 (1): 45–55. arXiv:0709.0248. Bibcode:2008MPCPS.146...45A. doi:10.1017/S0305004108001783. S2CID 7915709. As PDF.
Awodey, Steve (2012). "Type Theory and Homotopy" (PDF). In Dybjer, P.; Lindström, Sten; Palmgren, Erik; et al. (eds.). Epistemology versus Ontology. Logic, Epistemology, and the Unity of Science. Springer. pp. 183–201. CiteSeerX 10.1.1.750.3626. doi:10.1007/978-94-007-4435-6_9. ISBN 978-94-007-4434-9. S2CID 4499538.
Awodey, Steve (2014). "Structuralism, Invariance, and Univalence". Philosophia Mathematica. 22 (1): 1–11. CiteSeerX 10.1.1.691.8113. doi:10.1093/philmat/nkt030.
Hofmann, Martin; Streicher, Thomas (1998). "The groupoid interpretation of type theory". In Sambin, G.; Smith, J.M. (eds.). Twenty Five Years of Constructive Type Theory. Clarendon Press. pp. 83–112. ISBN 978-0-19-158903-4. As postscript.
Rijke, Egbert (2012). Homotopy Type Theory (PDF) (Master's). Utrecht University.
Voevodsky, Vladimir (2006), A Very Short Note on Homotopy Lambda Calculus (PDF)
Voevodsky, Vladimir (2010), The Equivalence Axiom and Univalent Models of Type Theory, arXiv:1402.5556, Bibcode:2014arXiv1402.5556V
Warren, Michael A. (2008). Homotopy Theoretic Aspects of Constructive Type Theory (PDF) (Ph.D.). Carnegie Mellon University.

अग्रिम पठन

David Corfield (2020), Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy, Oxford University Press.
Egbert Rijke (2022), Introduction to Homotopy Type Theory, arXiv:2212.11082. Introductory textbook.

बाहरी संबंध

Homotopy Type Theory
Homotopy type theory at the nLab
Homotopy type theory wiki
Vladimir Voevodsky's webpage on the Univalent Foundations
Homotopy Type Theory and the Univalent Foundations of Mathematics by Steve Awodey
"Constructive Type Theory and Homotopy" – Video lecture by Steve Awodey at the Institute for Advanced Study

औपचारिक गणित के पुस्तकालय

Foundations library (2010-current)
HoTT library (2011-current), 30 January 2022
P-adics library (2011-2012)
RezkCompletion library, January 2022 (अब यूनीमैथ में एकीकृत, जहां आगे विकास होता है)
Ktheory library
UniMath library (2014-current), 25 January 2022

श्रेणी:गणित की नींव श्रेणी:प्रकार सिद्धांत श्रेणी:होमोटोपी सिद्धांत श्रेणी:औपचारिक तरीके श्रेणी:वीडियो क्लिप वाले लेख

[univalenceIsaType-19] Univalence is a type, a property of the identity type IdU of a universe U —Martín Hötzel Escardó (2018)^[18]^: p.1

[2018formulation-20] "Univalence is a type, and the univalence axiom says that this type has some inhabitant."^[18]^: p.1

[ttConvention-39] Here the type theory convention is used, that type names begin with a capitalized letter, but that function names begin with a lower-case letter.

[HötzelEscardó2018-40] Martín Hötzel Escardó has shown that the property of univalence, "a property of the identity type IdU of a universe U",^[18]^: 4 may or may not have an inhabitant. By the Univalence Axiom the type 'isUnivalent(U)' has an inhabitant; Hötzel Escardó notes that when reflection is the only way to construct elements of the identity type, other than univalence, one may construct a function J from the identity type, from reflection, and from J.^[18]^{: 2.4 The identity type} Hötzel Escardó proceeds to construct the univalence type, using repeated applications of J. When 'all types are sets' (denoted Axiom K),^[18]^: 2.4 Axiom K implies the type 'isUnivalent(U)' does not have an inhabitant. Thus Hötzel Escardó finds the type 'isUnivalent(U)' is undecided in Martin-Löf Type Theory (MLTT).^[18]^{: 3.2, p.6 The Univalence Axiom}

[1] Shulman, Michael (2016-01-27). "Homotopy Type Theory: A synthetic approach to higher equalities". arXiv:1601.05035v3 [math.LO]., footnote 1

[2] Hofmann, M.; Streicher, T. (1994). "Groupoid मॉडल पहचान प्रमाणों की विशिष्टता का खंडन करता है". Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science: 208–212. doi:10.1109/LICS.1994.316071. ISBN 0-8186-6310-3. S2CID 19496198.

[3] Hofmann, Martin; Streicher, Thomas (1998). "The groupoid interpretation of type theory". In Sambin, Giovanni; Smith, Jan M. (eds.). रचनात्मक प्रकार के सिद्धांत के पच्चीस वर्ष. Oxford Logic Guides. Vol. 36. Clarendon Press. pp. 83–111. ISBN 978-0-19-158903-4. MR 1686862.

[4] Ahrens, Benedikt; Kapulkin, Krzysztof; Shulman, Michael (2015). "असमान श्रेणियां और Rezk पूर्णता". Mathematical Structures in Computer Science. 25 (5): 1010–1039. arXiv:1303.0584. doi:10.1017/S0960129514000486. MR 3340533. S2CID 1135785.

[5] "Foundational Methods in Computer Science 2006, University of Calgary, June 7th - 9th, 2006". University of Calgary. Retrieved 6 June 2021.

[6] Warren, Michael A. (2006). इंटेंशनल टाइप थ्योरी के होमोटॉपी मॉडल (PDF) (Thesis).

[7] "Identity Types - Topological and Categorical Structure, Workshop, Uppsala, November 13-14, 2006". Uppsala University - Department of Mathematics. Retrieved 6 June 2021.

[8] Richard Garner, Factorisation axioms for type theory

[9] Berg, Benno van den; Garner, Richard (27 July 2010). "पहचान प्रकारों के सामयिक और सरल मॉडल". arXiv:1007.4638 [math.LO].

[10] Lumsdaine, Peter LeFanu; Warren, Michael A. (6 November 2014). "The local universes model: an overlooked coherence construction for dependent type theories". ACM Transactions on Computational Logic. 16 (3): 1–31. arXiv:1411.1736. doi:10.1145/2754931. S2CID 14068103.

[11] "86th edition of the Peripatetic Seminar on Sheaves and Logic, Henri Poincaré University, September 8-9, 2007". loria.fr. Archived from the original on 17 December 2014. Retrieved 20 December 2014.

[12] Preliminary list of PSSL86 participants

[13] Awodey, Steve; Warren, Michael A. (3 September 2007). "पहचान प्रकारों के होमोटॉपी सैद्धांतिक मॉडल". Mathematical Proceedings of the Cambridge Philosophical Society. 146 (1): 45. arXiv:0709.0248. Bibcode:2008MPCPS.146...45A. doi:10.1017/S0305004108001783. S2CID 7915709.

[14] Voevodsky, Vladimir (27 September 2006). "A very short note on homotopy λ-calculus". ucr.edu. Retrieved 6 June 2021.

[15] van den Berg, Benno; Garner, Richard (1 December 2007). "प्रकार कमजोर ओमेगा-ग्रुपॉइड हैं". Proceedings of the London Mathematical Society. 102 (2): 370–394. arXiv:0812.0298. doi:10.1112/plms/pdq026. S2CID 5575780.

[16] Lumsdaine, Peter (2010). "टाइप थ्योरी से उच्च श्रेणियाँ" (PDF) (Ph.D.). Carnegie Mellon University.

[17] Notes on homotopy lambda calculus, March 2006

[HotzelEscardo-18] 18.0 ^18.1 ^18.2 ^18.3 ^18.4 ^18.5 ^18.6 ^18.7 Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom

[UniMath-21] GitHub repository, Univalent Mathematics

[22] Awodey, Steve; Garner, Richard; Martin-Löf, Per; Voevodsky, Vladimir (27 February – 5 March 2011). "Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory" (PDF). Oberwolfach Reports. Mathematical Research Institute of Oberwolfach: 609–638. doi:10.4171/OWR/2011/11. Retrieved 6 June 2021.

[23] GitHub repository, Andrej Bauer, Homotopy theory in Coq

[24] Bauer, Andrej; Voevodsky, Vladimir (29 April 2011). "बेसिक होमोटॉपी टाइप थ्योरी". GitHub. Retrieved 6 June 2021.

[25] GitHub repository, Homotopy type theory

[26] Shulman, Michael (2015). "व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता". Mathematical Structures in Computer Science. 25 (5): 1203–1277. arXiv:1203.3253. doi:10.1017/S0960129514000565. S2CID 13595170.

[27] Licata, Daniel R.; Harper, Robert (21 July 2011). "Canonicity for 2-Dimensional Type Theory" (PDF). Carnegie Mellon University. Retrieved 6 June 2021.

[28] Homotopy Type Theory and Univalent Foundations Blog

[29] Homotopy Type Theory blog

[30] Type Theory and Univalent Foundations

[hott-31] 29.0 ^29.1 ^29.2 ^29.3 ^29.4 Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.

[32] Homotopy Type Theory: References

[33] IAS school of mathematics: Special Year on The Univalent Foundations of Mathematics

[34] Official announcement of The HoTT Book, by Steve Awodey, 20 June 2013

[35] Monroe, D (2014). "A New Type of Mathematics?". Comm ACM. 57 (2): 13–15. doi:10.1145/2557446. S2CID 6120947.

[36] Shulman, Mike (20 June 2013). "एचओटीटी बुक". The n-Category Café. Retrieved 6 June 2021 – via University of Texas.

[37] Bauer, Andrej (20 June 2013). "एचओटीटी बुक". Mathematics and Computation. Retrieved 6 June 2021.

[38] ACM Computing Reviews. "Best of 2013".

[:0-41] 37.0 ^37.1 ^37.2 Meyer, Florian (3 September 2014). "गणित के लिए एक नई नींव". R&D Magazine. Retrieved 29 July 2021.

[42] Sojakova, Kristina (2015). होमोटोपी-प्रारंभिक बीजगणित के रूप में उच्च आगमनात्मक प्रकार. POPL 2015. arXiv:1402.0761. doi:10.1145/2676726.2676983.

[43] Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2015). Cubical Type Theory: a constructive interpretation of the univalence axiom. TYPES 2015.

[44] Anguili, Carlo; Favonia; Harper, Robert (2018). Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities (PDF). Computer Science Logic 2018. Retrieved 26 Aug 2018. (to appear)

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[lower-alpha 1]

[lower-alpha 2]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]

[lower-alpha 3]

[18]

[lower-alpha 4]

[37]

[38]

[39]

[40]

@@ Line 4: / Line 4: @@
 [[File:Hott book cover.png|thumb|होमोटॉपी टाइप थ्योरी का कवर: गणित की असमान नींव।]][[गणितीय तर्क]] और [[कंप्यूटर विज्ञान]] में, होमोटॉपी टाइप थ्योरी (HoTT {{IPAc-en|h|ɒ|t}}) अंतर्ज्ञानवादी प्रकार के सिद्धांत के विकास की विभिन्न पंक्तियों को संदर्भित करता है, जो वस्तुओं के रूप में व्याख्या के आधार पर होता है, जिस पर (अमूर्त) होमोटोपी सिद्धांत का अंतर्ज्ञान लागू होता है।
-इसमें काम की अन्य पंक्तियों के अलावा, इस प्रकार के सिद्धांतों के लिए होमोटोपिकल और उच्च श्रेणी के सिद्धांत का निर्माण | उच्च-श्रेणीबद्ध [[मॉडल (गणितीय तर्क)]] शामिल हैं; अमूर्त समरूपता सिद्धांत और [[उच्च श्रेणी सिद्धांत]] के लिए तर्क (या [[आंतरिक भाषा]]) के रूप में प्रकार सिद्धांत का उपयोग; गणित के एक प्रकार-सैद्धांतिक नींव के भीतर गणित का विकास (पहले से मौजूद गणित और नए गणित दोनों को शामिल करना जो होमोटोपिकल प्रकारों को संभव बनाता है); और कंप्यूटर प्रूफ सहायकों में इनमें से प्रत्येक का [[औपचारिक प्रमाण]]।
+इसमें काम की अन्य पंक्तियों के अलावा, इस प्रकार के सिद्धांतों के लिए होमोटोपिकल और उच्च श्रेणी के सिद्धांत का निर्माण | उच्च-श्रेणीबद्ध [[मॉडल (गणितीय तर्क)]] शामिल हैं; अमूर्त समरूपता सिद्धांत और [[उच्च श्रेणी सिद्धांत]] के लिए तर्क (या [[आंतरिक भाषा]]) के रूप में प्रकार सिद्धांत का उपयोग; गणित के प्रकार-सैद्धांतिक नींव के भीतर गणित का विकास (पहले से मौजूद गणित और नए गणित दोनों को शामिल करना जो होमोटोपिकल प्रकारों को संभव बनाता है); और कंप्यूटर प्रूफ सहायकों में इनमें से प्रत्येक का [[औपचारिक प्रमाण]]।
-होमोटॉपी प्रकार के सिद्धांत के रूप में संदर्भित कार्य के बीच एक बड़ा ओवरलैप है, और एकरूप नींव परियोजना के रूप में। हालांकि न तो सटीक रूप से चित्रित किया गया है, और शब्दों को कभी-कभी एक दूसरे के स्थान पर उपयोग किया जाता है, उपयोग की पसंद भी कभी-कभी दृष्टिकोण और जोर में अंतर से मेल खाती है।<ref>{{cite arXiv|last=Shulman|first=Michael|author-link=Michael Shulman (mathematician) |eprint=1601.05035v3|title=Homotopy Type Theory: A synthetic approach to higher equalities |date=2016-01-27|class=math.LO}}, footnote 1</ref> इस प्रकार, यह लेख समान रूप से क्षेत्र के सभी शोधकर्ताओं के विचारों का प्रतिनिधित्व नहीं कर सकता है। इस तरह की परिवर्तनशीलता अपरिहार्य है जब एक क्षेत्र तेजी से प्रवाह में हो।
+होमोटॉपी प्रकार के सिद्धांत के रूप में संदर्भित कार्य के बीच बड़ा ओवरलैप है, और एकरूप नींव परियोजना के रूप में। हालांकि न तो सटीक रूप से चित्रित किया गया है, और शब्दों को कभी-कभी दूसरे के स्थान पर उपयोग किया जाता है, उपयोग की पसंद भी कभी-कभी दृष्टिकोण और जोर में अंतर से मेल खाती है।<ref>{{cite arXiv|last=Shulman|first=Michael|author-link=Michael Shulman (mathematician) |eprint=1601.05035v3|title=Homotopy Type Theory: A synthetic approach to higher equalities |date=2016-01-27|class=math.LO}}, footnote 1</ref> इस प्रकार, यह लेख समान रूप से क्षेत्र के सभी शोधकर्ताओं के विचारों का प्रतिनिधित्व नहीं कर सकता है। इस तरह की परिवर्तनशीलता अपरिहार्य है जब क्षेत्र तेजी से प्रवाह में हो।
 == इतिहास ==
 === प्रागितिहास: [[groupoid]] मॉडल ===
-एक समय में यह विचार कि अंतर्ज्ञानवादी प्रकार के सिद्धांत #Extensional बनाम उनके पहचान प्रकारों के साथ इंटेंसिव को समूह के रूप में माना जा सकता है, गणितीय लोककथा थी। इसे पहली बार मार्टिन हॉफमैन और [[थॉमस स्ट्रीचर]] के 1994 के पेपर में सटीक रूप से शब्दार्थ बनाया गया था, जिसे द ग्रुपॉइड मॉडल कहा जाता है, जो पहचान प्रमाणों की विशिष्टता का खंडन करता है,<ref>{{Cite journal |last1=Hofmann |first1=M. |last2=Streicher |first2=T. |date=1994 |title=Groupoid मॉडल पहचान प्रमाणों की विशिष्टता का खंडन करता है|url=https://ieeexplore.ieee.org/document/316071 |journal=Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science |pages=208–212 |doi=10.1109/LICS.1994.316071|isbn=0-8186-6310-3 |s2cid=19496198 }}</ref> जिसमें उन्होंने दिखाया कि गहन प्रकार के सिद्धांत का समूह समूह की श्रेणी में एक मॉडल था। यह टाइप थ्योरी का पहला सही मायने में होमोटोपिकल बीजगणित मॉडल था, यद्यपि केवल 1-[[आयाम]]ी ([[सेट की श्रेणी]] में पारंपरिक मॉडल होमोटोपिक रूप से 0-आयामी होते हैं)।
+समय में यह विचार कि अंतर्ज्ञानवादी प्रकार के सिद्धांत #Extensional बनाम उनके पहचान प्रकारों के साथ इंटेंसिव को समूह के रूप में माना जा सकता है, गणितीय लोककथा थी। इसे पहली बार मार्टिन हॉफमैन और [[थॉमस स्ट्रीचर]] के 1994 के पेपर में सटीक रूप से शब्दार्थ बनाया गया था, जिसे द ग्रुपॉइड मॉडल कहा जाता है, जो पहचान प्रमाणों की विशिष्टता का खंडन करता है,<ref>{{Cite journal |last1=Hofmann |first1=M. |last2=Streicher |first2=T. |date=1994 |title=Groupoid मॉडल पहचान प्रमाणों की विशिष्टता का खंडन करता है|url=https://ieeexplore.ieee.org/document/316071 |journal=Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science |pages=208–212 |doi=10.1109/LICS.1994.316071|isbn=0-8186-6310-3 |s2cid=19496198 }}</ref> जिसमें उन्होंने दिखाया कि गहन प्रकार के सिद्धांत का समूह समूह की श्रेणी में मॉडल था। यह टाइप थ्योरी का पहला सही मायने में होमोटोपिकल बीजगणित मॉडल था, यद्यपि केवल 1-[[आयाम]]ी ([[सेट की श्रेणी]] में पारंपरिक मॉडल होमोटोपिक रूप से 0-आयामी होते हैं)।
-उनका फॉलो-अप पेपर<ref>{{cite book |last1=Hofmann |first1=Martin |title=रचनात्मक प्रकार के सिद्धांत के पच्चीस वर्ष|last2=Streicher |first2=Thomas |date=1998 |publisher=Clarendon Press |isbn=978-0-19-158903-4 |editor1-last=Sambin |editor1-first=Giovanni |series=Oxford Logic Guides |volume=36 |pages=83–111 |chapter=The groupoid interpretation of type theory |mr=1686862 |author2-link=Thomas Streicher |editor2-last=Smith |editor2-first=Jan M. |chapter-url=https://books.google.com/books?id=pLnKggT_In4C&pg=PA83}}</ref> होमोटॉपी प्रकार के सिद्धांत में बाद के कई विकासों का पूर्वाभास हुआ। उदाहरण के लिए, उन्होंने नोट किया कि ग्रुपॉइड मॉडल एक नियम को संतुष्ट करता है जिसे उन्होंने ब्रह्मांड विस्तार कहा है, जो कि 1-प्रकार के एकरूपता स्वयंसिद्ध के प्रतिबंध के अलावा और कोई नहीं है जिसे [[व्लादिमीर वोवोडस्की]] ने दस साल बाद प्रस्तावित किया था। (1-प्रकार के लिए स्वयंसिद्ध विशेष रूप से तैयार करने के लिए सरल है, हालांकि, समानता की एक सुसंगत स्थिति धारणा की आवश्यकता नहीं है।) उन्होंने आइसोमोर्फिज्म के साथ श्रेणियों को समानता के रूप में परिभाषित किया और अनुमान लगाया कि ऐसी श्रेणियों के लिए उच्च-आयामी समूह का उपयोग करने वाले मॉडल में किसी के पास समानता होगी समानता है; यह बाद में बेनेडिक्ट अहरेंस, क्रिज़्सटॉफ़ कपुल्किन और [[माइकल शुलमैन (गणितज्ञ)]] द्वारा सिद्ध किया गया था।<ref>{{cite journal |first1=Benedikt |last1=Ahrens |first2=Krzysztof |last2=Kapulkin |first3=Michael |last3=Shulman |author3-link=Michael Shulman (mathematician)|title=असमान श्रेणियां और Rezk पूर्णता|journal=Mathematical Structures in Computer Science |volume=25 |year=2015|issue= 5|pages= 1010–1039|arxiv=1303.0584 |doi=10.1017/S0960129514000486|mr=3340533|s2cid=1135785 }}</ref>
+उनका फॉलो-अप पेपर<ref>{{cite book |last1=Hofmann |first1=Martin |title=रचनात्मक प्रकार के सिद्धांत के पच्चीस वर्ष|last2=Streicher |first2=Thomas |date=1998 |publisher=Clarendon Press |isbn=978-0-19-158903-4 |editor1-last=Sambin |editor1-first=Giovanni |series=Oxford Logic Guides |volume=36 |pages=83–111 |chapter=The groupoid interpretation of type theory |mr=1686862 |author2-link=Thomas Streicher |editor2-last=Smith |editor2-first=Jan M. |chapter-url=https://books.google.com/books?id=pLnKggT_In4C&pg=PA83}}</ref> होमोटॉपी प्रकार के सिद्धांत में बाद के कई विकासों का पूर्वाभास हुआ। उदाहरण के लिए, उन्होंने नोट किया कि ग्रुपॉइड मॉडल नियम को संतुष्ट करता है जिसे उन्होंने ब्रह्मांड विस्तार कहा है, जो कि 1-प्रकार के एकरूपता स्वयंसिद्ध के प्रतिबंध के अलावा और कोई नहीं है जिसे [[व्लादिमीर वोवोडस्की]] ने दस साल बाद प्रस्तावित किया था। (1-प्रकार के लिए स्वयंसिद्ध विशेष रूप से तैयार करने के लिए सरल है, हालांकि, समानता की सुसंगत स्थिति धारणा की आवश्यकता नहीं है।) उन्होंने आइसोमोर्फिज्म के साथ श्रेणियों को समानता के रूप में परिभाषित किया और अनुमान लगाया कि ऐसी श्रेणियों के लिए उच्च-आयामी समूह का उपयोग करने वाले मॉडल में किसी के पास समानता होगी समानता है; यह बाद में बेनेडिक्ट अहरेंस, क्रिज़्सटॉफ़ कपुल्किन और [[माइकल शुलमैन (गणितज्ञ)]] द्वारा सिद्ध किया गया था।<ref>{{cite journal |first1=Benedikt |last1=Ahrens |first2=Krzysztof |last2=Kapulkin |first3=Michael |last3=Shulman |author3-link=Michael Shulman (mathematician)|title=असमान श्रेणियां और Rezk पूर्णता|journal=Mathematical Structures in Computer Science |volume=25 |year=2015|issue= 5|pages= 1010–1039|arxiv=1303.0584 |doi=10.1017/S0960129514000486|mr=3340533|s2cid=1135785 }}</ref>
 === प्रारंभिक इतिहास: मॉडल श्रेणियां और उच्च समूह ===
-[[मॉडल श्रेणी]] का उपयोग करते हुए 2005 में [[स्टीव अवोडे]] और उनके छात्र माइकल वॉरेन द्वारा आकस्मिक प्रकार के सिद्धांत के पहले उच्च-आयामी मॉडल का निर्माण किया गया था। इन परिणामों को पहली बार FMCS 2006 सम्मेलन में सार्वजनिक रूप से प्रस्तुत किया गया था<ref>{{cite web | url=http://pages.cpsc.ucalgary.ca/~robin/FMCS/FMCS_06/FMCS06.html | title=Foundational Methods in Computer Science 2006, University of Calgary, June 7th - 9th, 2006 | publisher=University of Calgary | accessdate=6 June 2021 }}</ref> जिस पर वारेन ने इंटेंसिव टाइप थ्योरी के होमोटॉपी मॉडल शीर्षक से एक वार्ता दी, जो उनकी थीसिस प्रॉस्पेक्टस के रूप में भी काम करती थी (शोध प्रबंध समिति में अवोडे, निकोला गैम्बिनो और एलेक्स सिम्पसन उपस्थित थे)। एक सारांश वॉरेन की थीसिस प्रॉस्पेक्टस सार में निहित है।<ref>{{cite thesis |first=Michael A. |last=Warren |title=इंटेंशनल टाइप थ्योरी के होमोटॉपी मॉडल|date=2006 |url=http://mawarren.net/papers/prospectus.pdf }}</ref>
+[[मॉडल श्रेणी]] का उपयोग करते हुए 2005 में [[स्टीव अवोडे]] और उनके छात्र माइकल वॉरेन द्वारा आकस्मिक प्रकार के सिद्धांत के पहले उच्च-आयामी मॉडल का निर्माण किया गया था। इन परिणामों को पहली बार FMCS 2006 सम्मेलन में सार्वजनिक रूप से प्रस्तुत किया गया था<ref>{{cite web | url=http://pages.cpsc.ucalgary.ca/~robin/FMCS/FMCS_06/FMCS06.html | title=Foundational Methods in Computer Science 2006, University of Calgary, June 7th - 9th, 2006 | publisher=University of Calgary | accessdate=6 June 2021 }}</ref> जिस पर वारेन ने इंटेंसिव टाइप थ्योरी के होमोटॉपी मॉडल शीर्षक से वार्ता दी, जो उनकी थीसिस प्रॉस्पेक्टस के रूप में भी काम करती थी (शोध प्रबंध समिति में अवोडे, निकोला गैम्बिनो और एलेक्स सिम्पसन उपस्थित थे)। सारांश वॉरेन की थीसिस प्रॉस्पेक्टस सार में निहित है।<ref>{{cite thesis |first=Michael A. |last=Warren |title=इंटेंशनल टाइप थ्योरी के होमोटॉपी मॉडल|date=2006 |url=http://mawarren.net/papers/prospectus.pdf }}</ref>
-में [[उप्साला विश्वविद्यालय]] में पहचान प्रकारों के बारे में बाद की कार्यशाला में<ref>{{cite web | url=http://www2.math.uu.se/~palmgren/itt/ | title=Identity Types - Topological and Categorical Structure, Workshop, Uppsala, November 13-14, 2006 | publisher=Uppsala University - Department of Mathematics | accessdate=6 June 2021 }}</ref> गहन प्रकार के सिद्धांत और कारककरण प्रणालियों के बीच संबंध के बारे में दो बातें थीं: एक रिचर्ड गार्नर द्वारा, प्रकार सिद्धांत के लिए कारककरण प्रणाली,<ref>[http://comp.mq.edu.au/~rgarner/Papers/Uppsala.pdf Richard Garner, Factorisation axioms for type theory]</ref> और एक माइकल वॉरेन द्वारा, मॉडल श्रेणियां और गहन पहचान प्रकार। संबंधित विचारों पर स्टीव अवोडी, उच्च-आयामी श्रेणियों के प्रकार सिद्धांत, और थॉमस स्ट्रीचर, पहचान प्रकार बनाम कमजोर ओमेगा-ग्रुपोइड्स: कुछ विचार, कुछ समस्याएं द्वारा वार्ता में चर्चा की गई। उसी सम्मेलन में बेन्नो वैन डेन बर्ग ने कमजोर ओमेगा-श्रेणियों के प्रकार नामक एक वार्ता दी जहां उन्होंने उन विचारों को रेखांकित किया जो बाद में रिचर्ड गार्नर के साथ एक संयुक्त पत्र का विषय बन गए।
+में [[उप्साला विश्वविद्यालय]] में पहचान प्रकारों के बारे में बाद की कार्यशाला में<ref>{{cite web | url=http://www2.math.uu.se/~palmgren/itt/ | title=Identity Types - Topological and Categorical Structure, Workshop, Uppsala, November 13-14, 2006 | publisher=Uppsala University - Department of Mathematics | accessdate=6 June 2021 }}</ref> गहन प्रकार के सिद्धांत और कारककरण प्रणालियों के बीच संबंध के बारे में दो बातें थीं: रिचर्ड गार्नर द्वारा, प्रकार सिद्धांत के लिए कारककरण प्रणाली,<ref>[http://comp.mq.edu.au/~rgarner/Papers/Uppsala.pdf Richard Garner, Factorisation axioms for type theory]</ref> और माइकल वॉरेन द्वारा, मॉडल श्रेणियां और गहन पहचान प्रकार। संबंधित विचारों पर स्टीव अवोडी, उच्च-आयामी श्रेणियों के प्रकार सिद्धांत, और थॉमस स्ट्रीचर, पहचान प्रकार बनाम कमजोर ओमेगा-ग्रुपोइड्स: कुछ विचार, कुछ समस्याएं द्वारा वार्ता में चर्चा की गई। उसी सम्मेलन में बेन्नो वैन डेन बर्ग ने कमजोर ओमेगा-श्रेणियों के प्रकार नामक वार्ता दी जहां उन्होंने उन विचारों को रेखांकित किया जो बाद में रिचर्ड गार्नर के साथ संयुक्त पत्र का विषय बन गए।
-उच्च आयामी मॉडल के सभी प्रारंभिक निर्माणों को निर्भर प्रकार के सिद्धांत के मॉडल के विशिष्ट सुसंगतता की समस्या से निपटना था, और विभिन्न समाधान विकसित किए गए थे। ऐसा ही एक 2009 में वोवोडस्की द्वारा दिया गया था, दूसरा 2010 में वैन डेन बर्ग और गार्नर द्वारा दिया गया था।<ref>{{cite arXiv |first1=Benno van den |last1=Berg |first2=Richard |last2=Garner |title=पहचान प्रकारों के सामयिक और सरल मॉडल|date=27 July 2010 |eprint=1007.4638|class=math.LO }}</ref> एक सामान्य समाधान, वोवोडस्की के निर्माण पर निर्माण, अंततः 2014 में लम्सडाइन और वॉरेन द्वारा दिया गया था।<ref>{{cite journal |first1=Peter LeFanu |last1=Lumsdaine |first2=Michael A. |last2=Warren |title=The local universes model: an overlooked coherence construction for dependent type theories |journal=ACM Transactions on Computational Logic |volume=16 |issue=3 |pages=1–31 |date=6 November 2014 |arxiv=1411.1736 |doi=10.1145/2754931|s2cid=14068103 }}</ref>
+उच्च आयामी मॉडल के सभी प्रारंभिक निर्माणों को निर्भर प्रकार के सिद्धांत के मॉडल के विशिष्ट सुसंगतता की समस्या से निपटना था, और विभिन्न समाधान विकसित किए गए थे। ऐसा ही 2009 में वोवोडस्की द्वारा दिया गया था, दूसरा 2010 में वैन डेन बर्ग और गार्नर द्वारा दिया गया था।<ref>{{cite arXiv |first1=Benno van den |last1=Berg |first2=Richard |last2=Garner |title=पहचान प्रकारों के सामयिक और सरल मॉडल|date=27 July 2010 |eprint=1007.4638|class=math.LO }}</ref> सामान्य समाधान, वोवोडस्की के निर्माण पर निर्माण, अंततः 2014 में लम्सडाइन और वॉरेन द्वारा दिया गया था।<ref>{{cite journal |first1=Peter LeFanu |last1=Lumsdaine |first2=Michael A. |last2=Warren |title=The local universes model: an overlooked coherence construction for dependent type theories |journal=ACM Transactions on Computational Logic |volume=16 |issue=3 |pages=1–31 |date=6 November 2014 |arxiv=1411.1736 |doi=10.1145/2754931|s2cid=14068103 }}</ref>
-में PSSL86 में<ref>{{cite web | url=http://www.loria.fr/~lamarche/psslHomeEN.html | title=86th edition of the Peripatetic Seminar on Sheaves and Logic, Henri Poincaré University, September 8-9, 2007 | publisher=loria.fr | access-date=20 December 2014 | archive-date=17 December 2014 | archive-url=https://archive.today/20141217151510/http://www.loria.fr/~lamarche/psslHomeEN.html | url-status=dead }}</ref> अवोडे ने होमोटॉपी टाइप थ्योरी शीर्षक से एक वार्ता दी (यह उस शब्द का पहला सार्वजनिक उपयोग था, जिसे अवोडी ने गढ़ा था<ref>[http://www.loria.fr/~lamarche/listPart.html Preliminary list of PSSL86 participants]</ref>). Awodey और वॉरेन ने अपने परिणामों को पेपर Homotopy Theoretic Models of Identity Types में संक्षेपित किया, जिसे 2007 में [[ArXiv]] प्रीप्रिंट सर्वर पर पोस्ट किया गया था<ref>{{cite journal |first1=Steve |last1=Awodey |first2=Michael A. |last2=Warren |title=पहचान प्रकारों के होमोटॉपी सैद्धांतिक मॉडल|date=3 September 2007 |arxiv=0709.0248 |doi=10.1017/S0305004108001783 |volume=146 |journal=Mathematical Proceedings of the Cambridge Philosophical Society |issue=1 |page=45|bibcode=2008MPCPS.146...45A |s2cid=7915709 }}</ref> और 2009 में प्रकाशित; 2008 में वॉरेन की थीसिस होमोटॉपी थ्योरिटिक आस्पेक्ट्स ऑफ कंस्ट्रक्टिव टाइप थ्योरी में एक अधिक विस्तृत संस्करण दिखाई दिया।
+में PSSL86 में<ref>{{cite web | url=http://www.loria.fr/~lamarche/psslHomeEN.html | title=86th edition of the Peripatetic Seminar on Sheaves and Logic, Henri Poincaré University, September 8-9, 2007 | publisher=loria.fr | access-date=20 December 2014 | archive-date=17 December 2014 | archive-url=https://archive.today/20141217151510/http://www.loria.fr/~lamarche/psslHomeEN.html | url-status=dead }}</ref> अवोडे ने होमोटॉपी टाइप थ्योरी शीर्षक से वार्ता दी (यह उस शब्द का पहला सार्वजनिक उपयोग था, जिसे अवोडी ने गढ़ा था<ref>[http://www.loria.fr/~lamarche/listPart.html Preliminary list of PSSL86 participants]</ref>). Awodey और वॉरेन ने अपने परिणामों को पेपर Homotopy Theoretic Models of Identity Types में संक्षेपित किया, जिसे 2007 में [[ArXiv]] प्रीप्रिंट सर्वर पर पोस्ट किया गया था<ref>{{cite journal |first1=Steve |last1=Awodey |first2=Michael A. |last2=Warren |title=पहचान प्रकारों के होमोटॉपी सैद्धांतिक मॉडल|date=3 September 2007 |arxiv=0709.0248 |doi=10.1017/S0305004108001783 |volume=146 |journal=Mathematical Proceedings of the Cambridge Philosophical Society |issue=1 |page=45|bibcode=2008MPCPS.146...45A |s2cid=7915709 }}</ref> और 2009 में प्रकाशित; 2008 में वॉरेन की थीसिस होमोटॉपी थ्योरिटिक आस्पेक्ट्स ऑफ कंस्ट्रक्टिव टाइप थ्योरी में अधिक विस्तृत संस्करण दिखाई दिया।
-लगभग उसी समय, व्लादिमीर वोवोडस्की गणित की व्यावहारिक औपचारिकता के लिए एक भाषा की खोज के संदर्भ में स्वतंत्र रूप से प्रकार के सिद्धांत की जांच कर रहे थे। सितंबर 2006 में उन्होंने टाइप्स मेलिंग लिस्ट में होमोटॉपी [[लैम्ब्डा कैलकुलस]] पर एक बहुत ही छोटा नोट पोस्ट किया,<ref>{{cite web | url=http://math.ucr.edu/home/baez/Voevodsky_note.ps | title=A very short note on homotopy λ-calculus | first=Vladimir | last=Voevodsky | date=27 September 2006 | publisher=ucr.edu | accessdate=6 June 2021}}</ref> जिसने आश्रित उत्पादों, योगों और ब्रह्मांडों के साथ एक प्रकार के सिद्धांत की रूपरेखा तैयार की और कान [[सरल सेट]]ों में इस प्रकार के सिद्धांत का एक मॉडल तैयार किया। यह कहकर शुरू हुआ होमोटॉपी λ-कैलकुलस एक काल्पनिक (फिलहाल) प्रकार की प्रणाली है और इस समय समाप्त हो गया है, जो मैंने ऊपर कहा है, वह अनुमानों के स्तर पर है। होमोटॉपी श्रेणी में टीएस के मॉडल की परिभाषा भी गैर-तुच्छ है, जो कि 2009 तक हल नहीं किए गए जटिल सुसंगतता के मुद्दों का जिक्र है। इस नोट में समानता प्रकारों की एक वाक्यात्मक परिभाषा शामिल थी, जिन्हें मॉडल में पथ द्वारा व्याख्या किए जाने का दावा किया गया था- रिक्त स्थान, लेकिन पहचान प्रकारों के लिए प्रति मार्टिन-लोफ के नियमों पर विचार नहीं किया। इसने ब्रह्मांडों को आकार के अलावा होमोटॉपी आयाम द्वारा भी स्तरीकृत किया, एक ऐसा विचार जिसे बाद में ज्यादातर खारिज कर दिया गया था।
+लगभग उसी समय, व्लादिमीर वोवोडस्की गणित की व्यावहारिक औपचारिकता के लिए भाषा की खोज के संदर्भ में स्वतंत्र रूप से प्रकार के सिद्धांत की जांच कर रहे थे। सितंबर 2006 में उन्होंने टाइप्स मेलिंग लिस्ट में होमोटॉपी [[लैम्ब्डा कैलकुलस]] पर बहुत ही छोटा नोट पोस्ट किया,<ref>{{cite web | url=http://math.ucr.edu/home/baez/Voevodsky_note.ps | title=A very short note on homotopy λ-calculus | first=Vladimir | last=Voevodsky | date=27 September 2006 | publisher=ucr.edu | accessdate=6 June 2021}}</ref> जिसने आश्रित उत्पादों, योगों और ब्रह्मांडों के साथ प्रकार के सिद्धांत की रूपरेखा तैयार की और कान [[सरल सेट]]ों में इस प्रकार के सिद्धांत का मॉडल तैयार किया। यह कहकर शुरू हुआ होमोटॉपी λ-कैलकुलस काल्पनिक (फिलहाल) प्रकार की प्रणाली है और इस समय समाप्त हो गया है, जो मैंने ऊपर कहा है, वह अनुमानों के स्तर पर है। होमोटॉपी श्रेणी में टीएस के मॉडल की परिभाषा भी गैर-तुच्छ है, जो कि 2009 तक हल नहीं किए गए जटिल सुसंगतता के मुद्दों का जिक्र है। इस नोट में समानता प्रकारों की वाक्यात्मक परिभाषा शामिल थी, जिन्हें मॉडल में पथ द्वारा व्याख्या किए जाने का दावा किया गया था- रिक्त स्थान, लेकिन पहचान प्रकारों के लिए प्रति मार्टिन-लोफ के नियमों पर विचार नहीं किया। इसने ब्रह्मांडों को आकार के अलावा होमोटॉपी आयाम द्वारा भी स्तरीकृत किया, ऐसा विचार जिसे बाद में ज्यादातर खारिज कर दिया गया था।
-सिंटैक्टिक पक्ष पर, बेन्नो वैन डेन बर्ग ने 2006 में अनुमान लगाया था कि आकस्मिक प्रकार के सिद्धांत में एक प्रकार के पहचान प्रकार के टावर में ω-श्रेणी की संरचना होनी चाहिए, और वास्तव में माइकल के गोलाकार, बीजगणितीय अर्थ में एक ω-ग्रुपॉइड होना चाहिए। बटानिन। यह बाद में पेपर में वैन डेन बर्ग और गार्नर द्वारा स्वतंत्र रूप से सिद्ध किया गया था प्रकार कमजोर ओमेगा-ग्रुपोइड्स हैं (प्रकाशित 2008),<ref>{{cite journal |first1=Benno |last1=van den Berg |first2=Richard |last2=Garner |title=प्रकार कमजोर ओमेगा-ग्रुपॉइड हैं|journal=Proceedings of the London Mathematical Society |volume=102 |issue=2 |pages=370–394 |date=1 December 2007 |arxiv=0812.0298 |doi=10.1112/plms/pdq026|s2cid=5575780 }}</ref> और पीटर लम्सडाइन द्वारा पेपर वीक ω-श्रेणियाँ इंटेंशनल टाइप थ्योरी (2009 में प्रकाशित) और उनके 2010 के पीएचडी के हिस्से के रूप में। थीसिस टाइप थ्योरीज़ से उच्च श्रेणियाँ।<ref>{{cite web |first=Peter |last=Lumsdaine |title=टाइप थ्योरी से उच्च श्रेणियाँ|date=2010 |type=Ph.D. |publisher=Carnegie Mellon University |url=http://lib.rett.org.uk/~peterlefanulumsdaine/research/Lumsdaine-2010-Thesis.pdf}}</ref>
+सिंटैक्टिक पक्ष पर, बेन्नो वैन डेन बर्ग ने 2006 में अनुमान लगाया था कि आकस्मिक प्रकार के सिद्धांत में प्रकार के पहचान प्रकार के टावर में ω-श्रेणी की संरचना होनी चाहिए, और वास्तव में माइकल के गोलाकार, बीजगणितीय अर्थ में ω-ग्रुपॉइड होना चाहिए। बटानिन। यह बाद में पेपर में वैन डेन बर्ग और गार्नर द्वारा स्वतंत्र रूप से सिद्ध किया गया था प्रकार कमजोर ओमेगा-ग्रुपोइड्स हैं (प्रकाशित 2008),<ref>{{cite journal |first1=Benno |last1=van den Berg |first2=Richard |last2=Garner |title=प्रकार कमजोर ओमेगा-ग्रुपॉइड हैं|journal=Proceedings of the London Mathematical Society |volume=102 |issue=2 |pages=370–394 |date=1 December 2007 |arxiv=0812.0298 |doi=10.1112/plms/pdq026|s2cid=5575780 }}</ref> और पीटर लम्सडाइन द्वारा पेपर वीक ω-श्रेणियाँ इंटेंशनल टाइप थ्योरी (2009 में प्रकाशित) और उनके 2010 के पीएचडी के हिस्से के रूप में। थीसिस टाइप थ्योरीज़ से उच्च श्रेणियाँ।<ref>{{cite web |first=Peter |last=Lumsdaine |title=टाइप थ्योरी से उच्च श्रेणियाँ|date=2010 |type=Ph.D. |publisher=Carnegie Mellon University |url=http://lib.rett.org.uk/~peterlefanulumsdaine/research/Lumsdaine-2010-Thesis.pdf}}</ref>
 === एकरूपता स्वयंसिद्ध, सिंथेटिक होमोटॉपी सिद्धांत, और उच्च आगमनात्मक प्रकार ===
-की शुरुआत में वोएवोडस्की द्वारा एक असमान कंपन की अवधारणा पेश की गई थी।<ref>[https://github.com/vladimirias/2006_Mar_Homotopy_lambda_calculus Notes on homotopy lambda calculus, March 2006]</ref>
+की शुरुआत में वोएवोडस्की द्वारा असमान कंपन की अवधारणा पेश की गई थी।<ref>[https://github.com/vladimirias/2006_Mar_Homotopy_lambda_calculus Notes on homotopy lambda calculus, March 2006]</ref>
-हालांकि, संपत्ति पर मार्टिन-लोफ प्रकार के सिद्धांत की सभी प्रस्तुतियों के आग्रह के कारण कि पहचान प्रकार, खाली संदर्भ में, केवल रिफ्लेक्सिविटी हो सकती है, वोवोडस्की ने 2009 तक यह नहीं पहचाना कि इन पहचान प्रकारों का संयोजन में उपयोग किया जा सकता है असमान ब्रह्मांड। विशेष रूप से, यह विचार कि मौजूदा मार्टिन-लोफ प्रकार के सिद्धांत में केवल एक स्वयंसिद्ध जोड़कर एकरूपता को पेश किया जा सकता है, केवल 2009 में दिखाई दिया।{{efn|name= univalenceIsaType |1= Univalence is a type, a property of the [[identity type]] IdU of a universe U —Martín Hötzel Escardó (2018)<ref name= HotzelEscardo/>{{rp|p.1}}}}{{efn|name= 2018formulation|1= "Univalence is a type, and the univalence axiom says that this type has some inhabitant."<ref name= HotzelEscardo/>{{rp|p.1}}}}
+हालांकि, संपत्ति पर मार्टिन-लोफ प्रकार के सिद्धांत की सभी प्रस्तुतियों के आग्रह के कारण कि पहचान प्रकार, खाली संदर्भ में, केवल रिफ्लेक्सिविटी हो सकती है, वोवोडस्की ने 2009 तक यह नहीं पहचाना कि इन पहचान प्रकारों का संयोजन में उपयोग किया जा सकता है असमान ब्रह्मांड। विशेष रूप से, यह विचार कि मौजूदा मार्टिन-लोफ प्रकार के सिद्धांत में केवल स्वयंसिद्ध जोड़कर एकरूपता को पेश किया जा सकता है, केवल 2009 में दिखाई दिया।{{efn|name= univalenceIsaType |1= Univalence is a type, a property of the [[identity type]] IdU of a universe U —Martín Hötzel Escardó (2018)<ref name= HotzelEscardo/>{{rp|p.1}}}}{{efn|name= 2018formulation|1= "Univalence is a type, and the univalence axiom says that this type has some inhabitant."<ref name= HotzelEscardo/>{{rp|p.1}}}}
-इसके अलावा 2009 में, वोएवोडस्की ने कान परिसरों में टाइप थ्योरी के एक मॉडल के विवरण के बारे में अधिक काम किया, और देखा कि एक सार्वभौमिक [[कैन फाइब्रेशन]] के अस्तित्व का उपयोग टाइप थ्योरी के श्रेणीबद्ध मॉडल के लिए सुसंगतता की समस्याओं को हल करने के लिए किया जा सकता है। उन्होंने यह भी साबित किया, ए.के. बोसफील्ड के एक विचार का उपयोग करते हुए, कि यह सार्वभौमिक कंपन एकतरफा था: तंतुओं के बीच जोड़ीदार होमोटॉपी समकक्षों का संबद्ध कंपन आधार के पथ-अंतरिक्ष कंपन के बराबर है।
+इसके अलावा 2009 में, वोएवोडस्की ने कान परिसरों में टाइप थ्योरी के मॉडल के विवरण के बारे में अधिक काम किया, और देखा कि सार्वभौमिक [[कैन फाइब्रेशन]] के अस्तित्व का उपयोग टाइप थ्योरी के श्रेणीबद्ध मॉडल के लिए सुसंगतता की समस्याओं को हल करने के लिए किया जा सकता है। उन्होंने यह भी साबित किया, ए.के. बोसफील्ड के विचार का उपयोग करते हुए, कि यह सार्वभौमिक कंपन एकतरफा था: तंतुओं के बीच जोड़ीदार होमोटॉपी समकक्षों का संबद्ध कंपन आधार के पथ-अंतरिक्ष कंपन के बराबर है।
-एक स्वयंसिद्ध के रूप में एकरूपता तैयार करने के लिए वोवोडस्की ने समतुल्यता को वाक्य-विन्यास के रूप में परिभाषित करने का एक तरीका खोजा, जिसमें महत्वपूर्ण गुण था कि कथन f का प्रतिनिधित्व करने वाला प्रकार एक तुल्यता था (फ़ंक्शन विस्तार की धारणा के तहत) (-1) - काट दिया गया (यानी अगर बसा हुआ है) . इसने उन्हें उच्च आयामों के लिए हॉफमैन और स्ट्रीचर की ब्रह्मांड की व्यापकता को सामान्य करते हुए, एकरूपता का एक वाक्यात्मक कथन देने में सक्षम बनाया। वह प्रूफ सहायक [[Coq]] में महत्वपूर्ण मात्रा में सिंथेटिक होमोटॉपी सिद्धांत विकसित करने के लिए समकक्षता और सिकुड़न की इन परिभाषाओं का उपयोग करने में सक्षम था; इसने लाइब्रेरी का आधार बनाया जिसे बाद में फ़ाउंडेशन और अंततः यूनीमैथ कहा गया।<ref name=UniMath>[https://github.com/UniMath/UniMath GitHub repository, Univalent Mathematics]</ref>
+स्वयंसिद्ध के रूप में एकरूपता तैयार करने के लिए वोवोडस्की ने समतुल्यता को वाक्य-विन्यास के रूप में परिभाषित करने का तरीका खोजा, जिसमें महत्वपूर्ण गुण था कि कथन f का प्रतिनिधित्व करने वाला प्रकार तुल्यता था (फ़ंक्शन विस्तार की धारणा के तहत) (-1) - काट दिया गया (यानी अगर बसा हुआ है) . इसने उन्हें उच्च आयामों के लिए हॉफमैन और स्ट्रीचर की ब्रह्मांड की व्यापकता को सामान्य करते हुए, एकरूपता का वाक्यात्मक कथन देने में सक्षम बनाया। वह प्रूफ सहायक [[Coq]] में महत्वपूर्ण मात्रा में सिंथेटिक होमोटॉपी सिद्धांत विकसित करने के लिए समकक्षता और सिकुड़न की इन परिभाषाओं का उपयोग करने में सक्षम था; इसने लाइब्रेरी का आधार बनाया जिसे बाद में फ़ाउंडेशन और अंततः यूनीमैथ कहा गया।<ref name=UniMath>[https://github.com/UniMath/UniMath GitHub repository, Univalent Mathematics]</ref>
-विभिन्न धागों का एकीकरण फरवरी 2010 में कार्नेगी मेलन विश्वविद्यालय में एक अनौपचारिक बैठक के साथ शुरू हुआ, जहां वोवोडस्की ने कान कॉम्प्लेक्स में अपना मॉडल प्रस्तुत किया और एवोडे, वॉरेन, लम्सडाइन, [[रॉबर्ट हार्पर (कंप्यूटर वैज्ञानिक)]], डैन लिकाटा, माइकल सहित एक समूह को अपना कॉक प्रस्तुत किया। शुलमैन (गणितज्ञ), और अन्य। इस बैठक ने एक प्रमाण की रूपरेखा तैयार की (वॉरेन, लम्सडाइन, लिकाटा और शुलमैन द्वारा) कि हर होमोटॉपी तुल्यता एक तुल्यता है (वोवोडस्की के अच्छे सुसंगत अर्थ में), समतुल्यता को आसन्न समकक्षों में सुधार के श्रेणी सिद्धांत के विचार पर आधारित है। इसके तुरंत बाद, वोएवोडस्की ने साबित कर दिया कि यूनीवैलेंस एक्सिओम का तात्पर्य कार्य विस्तार से है।
+विभिन्न धागों का एकीकरण फरवरी 2010 में कार्नेगी मेलन विश्वविद्यालय में अनौपचारिक बैठक के साथ शुरू हुआ, जहां वोवोडस्की ने कान कॉम्प्लेक्स में अपना मॉडल प्रस्तुत किया और एवोडे, वॉरेन, लम्सडाइन, [[रॉबर्ट हार्पर (कंप्यूटर वैज्ञानिक)]], डैन लिकाटा, माइकल सहित समूह को अपना कॉक प्रस्तुत किया। शुलमैन (गणितज्ञ), और अन्य। इस बैठक ने प्रमाण की रूपरेखा तैयार की (वॉरेन, लम्सडाइन, लिकाटा और शुलमैन द्वारा) कि हर होमोटॉपी तुल्यता तुल्यता है (वोवोडस्की के अच्छे सुसंगत अर्थ में), समतुल्यता को आसन्न समकक्षों में सुधार के श्रेणी सिद्धांत के विचार पर आधारित है। इसके तुरंत बाद, वोएवोडस्की ने साबित कर दिया कि यूनीवैलेंस एक्सिओम का तात्पर्य कार्य विस्तार से है।
-अगली महत्वपूर्ण घटना मार्च 2011 में ओबेरवॉल्फ के गणितीय अनुसंधान संस्थान में स्टीव अवोडे, रिचर्ड गार्नर, प्रति मार्टिन-लोफ और व्लादिमीर वोवोडस्की द्वारा आयोजित एक मिनी-कार्यशाला थी, जिसका शीर्षक रचनात्मक प्रकार के सिद्धांत की होमोटॉपी व्याख्या थी।<ref>{{cite journal | url=https://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf | title=Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory | publisher=Mathematical Research Institute of Oberwolfach | doi=10.4171/OWR/2011/11 | date=27 February – 5 March 2011 | accessdate=6 June 2021 | last1=Awodey | first1=Steve | last2=Garner | first2=Richard | last3=Martin-Löf | first3=Per | last4=Voevodsky | first4=Vladimir | journal=Oberwolfach Reports | pages=609–638 }}</ref> इस कार्यशाला के लिए Coq ट्यूटोरियल के एक भाग के रूप में, Andrej Bauer ने एक छोटी Coq लाइब्रेरी लिखी<ref>[https://github.com/andrejbauer/Homotopy GitHub repository, Andrej Bauer, Homotopy theory in Coq]</ref> वोवोद्स्की के विचारों पर आधारित (लेकिन वास्तव में उनके किसी भी कोड का उपयोग नहीं); यह अंततः HoTT Coq लाइब्रेरी के पहले संस्करण का कर्नेल बन गया<ref>{{cite web | url=https://github.com/HoTT/HoTT/commit/1fb4ed9e5cdc5494f26ae6d13c4ebc851b81e1ba | publisher=GitHub | title=बेसिक होमोटॉपी टाइप थ्योरी| first1=Andrej | last1=Bauer | first2=Vladimir | last2=Voevodsky | date=29 April 2011 | accessdate=6 June 2021 }}</ref> (बाद की पहली प्रतिबद्धता<ref>[https://github.com/HoTT/HoTT GitHub repository, Homotopy type theory]</ref> माइकल शुलमैन ने लेडी बाउर की फाइलों पर आधारित विकास को नोट किया है, जिसमें व्लादिमीर वोवोडस्की की फाइलों से लिए गए कई विचार हैं)। लम्सडाइन, शुलमैन, बाउर और वॉरेन के कारण, ओबेरवॉल्फ़ बैठक से निकलने वाली सबसे महत्वपूर्ण चीजों में से एक उच्च आगमनात्मक प्रकारों का मूल विचार था। प्रतिभागियों ने महत्वपूर्ण खुले प्रश्नों की एक सूची भी तैयार की, जैसे कि क्या यूनीवैलेंस एक्सिओम कैननिसिटी को संतुष्ट करता है (अभी भी खुला है, हालांकि कुछ विशेष मामलों को सकारात्मक रूप से हल किया गया है)<ref>{{cite journal |first=Michael |last=Shulman |title=व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता|journal=Mathematical Structures in Computer Science |volume=25 |issue=5 |pages=1203–1277 |year=2015 |arxiv=1203.3253 |doi=10.1017/S0960129514000565|s2cid=13595170 }}</ref><ref>{{cite web | url=https://www.cs.cmu.edu/~drl/pubs/lh112tt/lh112tt.pdf | title=Canonicity for 2-Dimensional Type Theory | first1=Daniel R. | last1=Licata | first2=Robert | last2=Harper | publisher=Carnegie Mellon University | date=21 July 2011 | accessdate=6 June 2021 }}</ref>), क्या एकरूपता स्वयंसिद्ध में गैरमानक मॉडल हैं (चूंकि शुलमैन द्वारा सकारात्मक उत्तर दिया गया है), और कैसे (अर्ध) सरल प्रकारों को परिभाषित किया जाए (अभी भी एमएलटीटी में खुला है, हालांकि यह वोवोडस्की के होमोटॉपी टाइप सिस्टम (एचटीएस) में किया जा सकता है, एक प्रकार सिद्धांत के साथ दो समानता प्रकार)।
+अगली महत्वपूर्ण घटना मार्च 2011 में ओबेरवॉल्फ के गणितीय अनुसंधान संस्थान में स्टीव अवोडे, रिचर्ड गार्नर, प्रति मार्टिन-लोफ और व्लादिमीर वोवोडस्की द्वारा आयोजित मिनी-कार्यशाला थी, जिसका शीर्षक रचनात्मक प्रकार के सिद्धांत की होमोटॉपी व्याख्या थी।<ref>{{cite journal | url=https://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf | title=Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory | publisher=Mathematical Research Institute of Oberwolfach | doi=10.4171/OWR/2011/11 | date=27 February – 5 March 2011 | accessdate=6 June 2021 | last1=Awodey | first1=Steve | last2=Garner | first2=Richard | last3=Martin-Löf | first3=Per | last4=Voevodsky | first4=Vladimir | journal=Oberwolfach Reports | pages=609–638 }}</ref> इस कार्यशाला के लिए Coq ट्यूटोरियल के भाग के रूप में, Andrej Bauer ने छोटी Coq लाइब्रेरी लिखी<ref>[https://github.com/andrejbauer/Homotopy GitHub repository, Andrej Bauer, Homotopy theory in Coq]</ref> वोवोद्स्की के विचारों पर आधारित (लेकिन वास्तव में उनके किसी भी कोड का उपयोग नहीं); यह अंततः HoTT Coq लाइब्रेरी के पहले संस्करण का कर्नेल बन गया<ref>{{cite web | url=https://github.com/HoTT/HoTT/commit/1fb4ed9e5cdc5494f26ae6d13c4ebc851b81e1ba | publisher=GitHub | title=बेसिक होमोटॉपी टाइप थ्योरी| first1=Andrej | last1=Bauer | first2=Vladimir | last2=Voevodsky | date=29 April 2011 | accessdate=6 June 2021 }}</ref> (बाद की पहली प्रतिबद्धता<ref>[https://github.com/HoTT/HoTT GitHub repository, Homotopy type theory]</ref> माइकल शुलमैन ने लेडी बाउर की फाइलों पर आधारित विकास को नोट किया है, जिसमें व्लादिमीर वोवोडस्की की फाइलों से लिए गए कई विचार हैं)। लम्सडाइन, शुलमैन, बाउर और वॉरेन के कारण, ओबेरवॉल्फ़ बैठक से निकलने वाली सबसे महत्वपूर्ण चीजों में से उच्च आगमनात्मक प्रकारों का मूल विचार था। प्रतिभागियों ने महत्वपूर्ण खुले प्रश्नों की सूची भी तैयार की, जैसे कि क्या यूनीवैलेंस एक्सिओम कैननिसिटी को संतुष्ट करता है (अभी भी खुला है, हालांकि कुछ विशेष मामलों को सकारात्मक रूप से हल किया गया है)<ref>{{cite journal |first=Michael |last=Shulman |title=व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता|journal=Mathematical Structures in Computer Science |volume=25 |issue=5 |pages=1203–1277 |year=2015 |arxiv=1203.3253 |doi=10.1017/S0960129514000565|s2cid=13595170 }}</ref><ref>{{cite web | url=https://www.cs.cmu.edu/~drl/pubs/lh112tt/lh112tt.pdf | title=Canonicity for 2-Dimensional Type Theory | first1=Daniel R. | last1=Licata | first2=Robert | last2=Harper | publisher=Carnegie Mellon University | date=21 July 2011 | accessdate=6 June 2021 }}</ref>), क्या एकरूपता स्वयंसिद्ध में गैरमानक मॉडल हैं (चूंकि शुलमैन द्वारा सकारात्मक उत्तर दिया गया है), और कैसे (अर्ध) सरल प्रकारों को परिभाषित किया जाए (अभी भी एमएलटीटी में खुला है, हालांकि यह वोवोडस्की के होमोटॉपी टाइप सिस्टम (एचटीएस) में किया जा सकता है, प्रकार सिद्धांत के साथ दो समानता प्रकार)।
 ओबेरवॉल्फ़ कार्यशाला के तुरंत बाद, होमोटॉपी टाइप थ्योरी वेबसाइट और ब्लॉग<ref>[http://homotopytypetheory.org Homotopy Type Theory and Univalent Foundations Blog]</ref> स्थापित किया गया था, और यह विषय उसी नाम से लोकप्रिय होने लगा। इस अवधि के दौरान हुई कुछ महत्वपूर्ण प्रगति का अंदाजा ब्लॉग इतिहास से लगाया जा सकता है।<ref>[http://homotopytypetheory.org/blog Homotopy Type Theory blog]</ref>
@@ Line 43: / Line 43: @@
 == असमान नींव ==
-मुहावरा असमान नींव सभी के द्वारा होमोटॉपी प्रकार के सिद्धांत से निकटता से संबंधित होने के लिए सहमत है, लेकिन हर कोई इसे उसी तरह से उपयोग नहीं करता है। यह मूल रूप से व्लादिमीर वोएवोडस्की द्वारा गणित के लिए एक मूलभूत प्रणाली के अपने दृष्टिकोण को संदर्भित करने के लिए उपयोग किया गया था जिसमें मूल वस्तुएं होमोटॉपी प्रकार हैं, एक प्रकार के सिद्धांत पर आधारित #The_univalence_axiom |<ref>[http://homotopytypetheory.org/ Type Theory and Univalent Foundations]</ref>
+मुहावरा असमान नींव सभी के द्वारा होमोटॉपी प्रकार के सिद्धांत से निकटता से संबंधित होने के लिए सहमत है, लेकिन हर कोई इसे उसी तरह से उपयोग नहीं करता है। यह मूल रूप से व्लादिमीर वोएवोडस्की द्वारा गणित के लिए मूलभूत प्रणाली के अपने दृष्टिकोण को संदर्भित करने के लिए उपयोग किया गया था जिसमें मूल वस्तुएं होमोटॉपी प्रकार हैं, प्रकार के सिद्धांत पर आधारित #The_univalence_axiom |<ref>[http://homotopytypetheory.org/ Type Theory and Univalent Foundations]</ref>
-जैसा कि वोवोद्स्की का काम होमोटोपी प्रकार के सिद्धांत पर काम कर रहे अन्य शोधकर्ताओं के समुदाय के साथ एकीकृत हो गया, कभी-कभी असमान नींव को होमोटॉपी प्रकार के सिद्धांत के साथ एक दूसरे के रूप में इस्तेमाल किया जाता था,<ref name=hott/>  और अन्य समय केवल एक मूलभूत प्रणाली के रूप में इसके उपयोग को संदर्भित करने के लिए (उदाहरण के लिए, मॉडल-श्रेणीबद्ध शब्दार्थ या कम्प्यूटेशनल मेटाथ्योरी के अध्ययन को छोड़कर)।<ref>[http://ncatlab.org/homotopytypetheory/show/References Homotopy Type Theory: References]</ref> उदाहरण के लिए, IAS विशेष वर्ष के विषय को आधिकारिक तौर पर एकतरफा नींव के रूप में दिया गया था, हालांकि वहां किए गए बहुत से काम नींव के अलावा शब्दार्थ और मेटाथ्योरी पर केंद्रित थे। आईएएस कार्यक्रम में भाग लेने वालों द्वारा तैयार की गई पुस्तक का शीर्षक होमोटॉपी टाइप थ्योरी: यूनिवैलेंट फाउंडेशन्स ऑफ मैथमैटिक्स; हालांकि यह या तो उपयोग को संदर्भित कर सकता है, क्योंकि पुस्तक केवल HoTT को गणितीय आधार के रूप में चर्चा करती है।<ref name=hott/>
+जैसा कि वोवोद्स्की का काम होमोटोपी प्रकार के सिद्धांत पर काम कर रहे अन्य शोधकर्ताओं के समुदाय के साथ एकीकृत हो गया, कभी-कभी असमान नींव को होमोटॉपी प्रकार के सिद्धांत के साथ दूसरे के रूप में इस्तेमाल किया जाता था,<ref name=hott/>  और अन्य समय केवल मूलभूत प्रणाली के रूप में इसके उपयोग को संदर्भित करने के लिए (उदाहरण के लिए, मॉडल-श्रेणीबद्ध शब्दार्थ या कम्प्यूटेशनल मेटाथ्योरी के अध्ययन को छोड़कर)।<ref>[http://ncatlab.org/homotopytypetheory/show/References Homotopy Type Theory: References]</ref> उदाहरण के लिए, IAS विशेष वर्ष के विषय को आधिकारिक तौर पर एकतरफा नींव के रूप में दिया गया था, हालांकि वहां किए गए बहुत से काम नींव के अलावा शब्दार्थ और मेटाथ्योरी पर केंद्रित थे। आईएएस कार्यक्रम में भाग लेने वालों द्वारा तैयार की गई पुस्तक का शीर्षक होमोटॉपी टाइप थ्योरी: यूनिवैलेंट फाउंडेशन्स ऑफ मैथमैटिक्स; हालांकि यह या तो उपयोग को संदर्भित कर सकता है, क्योंकि पुस्तक केवल HoTT को गणितीय आधार के रूप में चर्चा करती है।<ref name=hott/>
 == गणित के यूनिवैलेंट फाउंडेशन पर विशेष वर्ष ==
-[[File:The making of HoTT book.webm|thumb|यूनीवेलेंट फ़ाउंडेशन स्पेशल ईयर प्रोजेक्ट में प्रतिभागियों द्वारा GitHub रिपॉजिटरी पर HoTT बुक के विकास को दर्शाने वाला एक एनीमेशन।]]2012-13 में [[उन्नत अध्ययन संस्थान]] के शोधकर्ताओं ने गणित के यूनिवेलेंट फाउंडेशन पर एक विशेष वर्ष आयोजित किया।<ref>[https://www.math.ias.edu/sp/univalent IAS school of mathematics:  Special Year on The Univalent Foundations of Mathematics]</ref> विशेष वर्ष ने [[टोपोलॉजी]], कंप्यूटर विज्ञान, [[श्रेणी सिद्धांत]] और गणितीय तर्क में शोधकर्ताओं को एक साथ लाया। कार्यक्रम का आयोजन स्टीव अवोडे, [[थिएरी कोक्वांड]] और व्लादिमीर वोवोडस्की द्वारा किया गया था।
+[[File:The making of HoTT book.webm|thumb|यूनीवेलेंट फ़ाउंडेशन स्पेशल ईयर प्रोजेक्ट में प्रतिभागियों द्वारा GitHub रिपॉजिटरी पर HoTT बुक के विकास को दर्शाने वाला एनीमेशन।]]2012-13 में [[उन्नत अध्ययन संस्थान]] के शोधकर्ताओं ने गणित के यूनिवेलेंट फाउंडेशन पर विशेष वर्ष आयोजित किया।<ref>[https://www.math.ias.edu/sp/univalent IAS school of mathematics:  Special Year on The Univalent Foundations of Mathematics]</ref> विशेष वर्ष ने [[टोपोलॉजी]], कंप्यूटर विज्ञान, [[श्रेणी सिद्धांत]] और गणितीय तर्क में शोधकर्ताओं को साथ लाया। कार्यक्रम का आयोजन स्टीव अवोडे, [[थिएरी कोक्वांड]] और व्लादिमीर वोवोडस्की द्वारा किया गया था।
-कार्यक्रम के दौरान, [[पीटर एक्ज़ेल]], जो प्रतिभागियों में से एक थे, ने एक कार्य समूह की शुरुआत की, जिसने जांच की कि टाइप थ्योरी को अनौपचारिक रूप से लेकिन कठोरता से कैसे किया जाए, एक शैली में जो सामान्य गणितज्ञों के सेट थ्योरी के अनुरूप है। प्रारंभिक प्रयोगों के बाद यह स्पष्ट हो गया कि यह न केवल संभव था बल्कि अत्यधिक लाभदायक था, और यह कि एक पुस्तक (तथाकथित HoTT Book)<ref name=hott>{{cite book|author=Univalent Foundations Program|title=Homotopy Type Theory: Univalent Foundations of Mathematics|year=2013|publisher=Institute for Advanced Study|url=http://homotopytypetheory.org/book/}}</ref><ref>[http://homotopytypetheory.org/2013/06/20/the-hott-book/ Official announcement of The HoTT Book, by Steve Awodey, 20 June 2013]</ref> लिखा जा सकता है और लिखा जाना चाहिए। परियोजना के कई अन्य प्रतिभागी तब तकनीकी सहायता, लेखन, प्रूफ रीडिंग और विचारों की पेशकश के प्रयास में शामिल हुए। असामान्य रूप से एक गणित पाठ के लिए, इसे सहयोगी रूप से विकसित किया गया था और गिटहब पर खुले में, एक [[ क्रिएटिव कामन्स लाइसेंस ]] के तहत जारी किया गया है जो लोगों को पुस्तक के अपने स्वयं के संस्करण को फोर्क (सॉफ्टवेयर विकास) करने की अनुमति देता है, और प्रिंट और डाउनलोड दोनों में मुफ्त में खरीदा जा सकता है। शुल्क।<ref>{{cite journal |first=D |last=Monroe |title=A New Type of Mathematics? |journal=Comm ACM |volume=57 |issue=2 |pages=13–15 |year=2014 |doi=10.1145/2557446 |s2cid=6120947 |url=http://cacm.acm.org/magazines/2014/2/171675-a-new-type-of-mathematics/abstract}}</ref><ref>{{cite web | url=https://golem.ph.utexas.edu/category/2013/06/the_hott_book.html | title=एचओटीटी बुक| first=Mike | last=Shulman | publisher=The n-Category Café | via=University of Texas | date=20 June 2013 | accessdate=6 June 2021 }}</ref><ref>{{cite web | url=http://math.andrej.com/2013/06/20/the-hott-book/ | title=एचओटीटी बुक| first=Andrej | last=Bauer | date=20 June 2013 | publisher=Mathematics and Computation | accessdate=6 June 2021 }}</ref>
+कार्यक्रम के दौरान, [[पीटर एक्ज़ेल]], जो प्रतिभागियों में से थे, ने कार्य समूह की शुरुआत की, जिसने जांच की कि टाइप थ्योरी को अनौपचारिक रूप से लेकिन कठोरता से कैसे किया जाए, शैली में जो सामान्य गणितज्ञों के सेट थ्योरी के अनुरूप है। प्रारंभिक प्रयोगों के बाद यह स्पष्ट हो गया कि यह न केवल संभव था बल्कि अत्यधिक लाभदायक था, और यह कि पुस्तक (तथाकथित HoTT Book)<ref name=hott>{{cite book|author=Univalent Foundations Program|title=Homotopy Type Theory: Univalent Foundations of Mathematics|year=2013|publisher=Institute for Advanced Study|url=http://homotopytypetheory.org/book/}}</ref><ref>[http://homotopytypetheory.org/2013/06/20/the-hott-book/ Official announcement of The HoTT Book, by Steve Awodey, 20 June 2013]</ref> लिखा जा सकता है और लिखा जाना चाहिए। परियोजना के कई अन्य प्रतिभागी तब तकनीकी सहायता, लेखन, प्रूफ रीडिंग और विचारों की पेशकश के प्रयास में शामिल हुए। असामान्य रूप से गणित पाठ के लिए, इसे सहयोगी रूप से विकसित किया गया था और गिटहब पर खुले में, [[ क्रिएटिव कामन्स लाइसेंस ]] के तहत जारी किया गया है जो लोगों को पुस्तक के अपने स्वयं के संस्करण को फोर्क (सॉफ्टवेयर विकास) करने की अनुमति देता है, और प्रिंट और डाउनलोड दोनों में मुफ्त में खरीदा जा सकता है। शुल्क।<ref>{{cite journal |first=D |last=Monroe |title=A New Type of Mathematics? |journal=Comm ACM |volume=57 |issue=2 |pages=13–15 |year=2014 |doi=10.1145/2557446 |s2cid=6120947 |url=http://cacm.acm.org/magazines/2014/2/171675-a-new-type-of-mathematics/abstract}}</ref><ref>{{cite web | url=https://golem.ph.utexas.edu/category/2013/06/the_hott_book.html | title=एचओटीटी बुक| first=Mike | last=Shulman | publisher=The n-Category Café | via=University of Texas | date=20 June 2013 | accessdate=6 June 2021 }}</ref><ref>{{cite web | url=http://math.andrej.com/2013/06/20/the-hott-book/ | title=एचओटीटी बुक| first=Andrej | last=Bauer | date=20 June 2013 | publisher=Mathematics and Computation | accessdate=6 June 2021 }}</ref>
-अधिक सामान्यतः, विशेष वर्ष संपूर्ण विषय के विकास के लिए एक उत्प्रेरक था; होटटी बुक केवल एक थी, यद्यपि सबसे अधिक दिखाई देने वाला, परिणाम।
+अधिक सामान्यतः, विशेष वर्ष संपूर्ण विषय के विकास के लिए उत्प्रेरक था; होटटी बुक केवल थी, यद्यपि सबसे अधिक दिखाई देने वाला, परिणाम।
 विशेष वर्ष में आधिकारिक प्रतिभागियों
@@ Line 85: / Line 85: @@
 {{div col end}}
-ACM कम्प्यूटिंग समीक्षा ने पुस्तक को कंप्यूटिंग के गणित श्रेणी में एक उल्लेखनीय 2013 प्रकाशन के रूप में सूचीबद्ध किया।<ref>''ACM Computing Reviews''. [http://computingreviews.com/recommend/bestof/notableitems_2013.cfm "Best of 2013"].</ref>
+ACM कम्प्यूटिंग समीक्षा ने पुस्तक को कंप्यूटिंग के गणित श्रेणी में उल्लेखनीय 2013 प्रकाशन के रूप में सूचीबद्ध किया।<ref>''ACM Computing Reviews''. [http://computingreviews.com/recommend/bestof/notableitems_2013.cfm "Best of 2013"].</ref>
@@ Line 109: / Line 109: @@
 === प्रकार के रूप में प्रस्ताव ===
-HoTT प्रकार सिद्धांत के प्रकार सिद्धांत व्याख्या के रूप में प्रस्तावों के एक संशोधित संस्करण का उपयोग करता है, जिसके अनुसार प्रकार भी प्रस्तावों का प्रतिनिधित्व कर सकते हैं और शर्तें तब सबूतों का प्रतिनिधित्व कर सकती हैं। HoTT में, हालांकि, प्रकार के रूप में मानक प्रस्तावों के विपरीत, 'मात्र प्रस्तावों' द्वारा एक विशेष भूमिका निभाई जाती है, जो कि, मोटे तौर पर बोलना, वे प्रकार होते हैं जिनमें प्रस्तावात्मक समानता तक अधिकतम एक शब्द होता है। ये सामान्य प्रकार की तुलना में पारंपरिक तार्किक प्रस्तावों की तरह अधिक हैं, जिसमें वे प्रमाण-अप्रासंगिक हैं।
+HoTT प्रकार सिद्धांत के प्रकार सिद्धांत व्याख्या के रूप में प्रस्तावों के संशोधित संस्करण का उपयोग करता है, जिसके अनुसार प्रकार भी प्रस्तावों का प्रतिनिधित्व कर सकते हैं और शर्तें तब सबूतों का प्रतिनिधित्व कर सकती हैं। HoTT में, हालांकि, प्रकार के रूप में मानक प्रस्तावों के विपरीत, 'मात्र प्रस्तावों' द्वारा विशेष भूमिका निभाई जाती है, जो कि, मोटे तौर पर बोलना, वे प्रकार होते हैं जिनमें प्रस्तावात्मक समानता तक अधिकतम शब्द होता है। ये सामान्य प्रकार की तुलना में पारंपरिक तार्किक प्रस्तावों की तरह अधिक हैं, जिसमें वे प्रमाण-अप्रासंगिक हैं।
 === समानता ===
-समरूपता प्रकार के सिद्धांत की मौलिक अवधारणा [[पथ (टोपोलॉजी)]] है। HoTT में, type <math>a = b</math> बिंदु से सभी पथों का प्रकार है <math>a</math> मुद्दे पर <math>b</math>. (इसलिए, एक सबूत है कि एक बिंदु <math>a</math> एक बिंदु के बराबर है <math>b</math> बिंदु से पथ के समान ही है <math>a</math> मुद्दे पर <math>b</math>।) किसी भी बिंदु के लिए <math>a</math>, प्रकार का एक पथ मौजूद है <math>a = a</math>समानता की रिफ्लेक्सिव संपत्ति के अनुरूप। प्रकार का मार्ग <math>a = b</math> उलटा जा सकता है, प्रकार का मार्ग बना सकता है <math>b = a</math>समानता की सममित संपत्ति के अनुरूप। प्रकार के दो रास्ते <math>a = b</math> सम्मान। <math>b = c</math> प्रकार का मार्ग बनाते हुए, समाप्‍त किया जा सकता है <math>a = c</math>; यह समानता की सकर्मक संपत्ति के अनुरूप है।
+समरूपता प्रकार के सिद्धांत की मौलिक अवधारणा [[पथ (टोपोलॉजी)]] है। HoTT में, type <math>a = b</math> बिंदु से सभी पथों का प्रकार है <math>a</math> मुद्दे पर <math>b</math>. (इसलिए, सबूत है कि बिंदु <math>a</math> बिंदु के बराबर है <math>b</math> बिंदु से पथ के समान ही है <math>a</math> मुद्दे पर <math>b</math>।) किसी भी बिंदु के लिए <math>a</math>, प्रकार का पथ मौजूद है <math>a = a</math>समानता की रिफ्लेक्सिव संपत्ति के अनुरूप। प्रकार का मार्ग <math>a = b</math> उलटा जा सकता है, प्रकार का मार्ग बना सकता है <math>b = a</math>समानता की सममित संपत्ति के अनुरूप। प्रकार के दो रास्ते <math>a = b</math> सम्मान। <math>b = c</math> प्रकार का मार्ग बनाते हुए, समाप्‍त किया जा सकता है <math>a = c</math>; यह समानता की सकर्मक संपत्ति के अनुरूप है।
-सबसे महत्वपूर्ण बात, एक रास्ता दिया <math>p:a=b</math>, और कुछ संपत्ति का प्रमाण <math>P(a)</math>, सबूत को रास्ते में ले जाया जा सकता है <math>p</math> संपत्ति का प्रमाण देने के लिए <math>P(b)</math>. (समकक्ष रूप से कहा गया है, प्रकार का एक वस्तु <math>P(a)</math> प्रकार की वस्तु में परिवर्तित किया जा सकता है <math>P(b)</math>.) यह प्रथम-क्रम तर्क#समानता और इसके स्वयंसिद्धों के अनुरूप है। यहाँ, HoTT और शास्त्रीय गणित के बीच एक महत्वपूर्ण अंतर आता है। शास्त्रीय गणित में, एक बार दो मूल्यों की समानता <math>a</math> और <math>b</math> स्थापित हो गया है, <math>a</math> और <math>b</math> इसके बाद उनके बीच किसी भी तरह के अंतर के संबंध में एक दूसरे के लिए इस्तेमाल किया जा सकता है। होमोटॉपी प्रकार के सिद्धांत में, हालांकि, कई अलग-अलग रास्ते हो सकते हैं <math>a = b</math>, और किसी वस्तु को दो अलग-अलग रास्तों से ले जाने से दो अलग-अलग परिणाम मिलेंगे। इसलिए, होमोटॉपी प्रकार के सिद्धांत में, प्रतिस्थापन संपत्ति को लागू करते समय, यह बताना आवश्यक है कि किस पथ का उपयोग किया जा रहा है।
+सबसे महत्वपूर्ण बात, रास्ता दिया <math>p:a=b</math>, और कुछ संपत्ति का प्रमाण <math>P(a)</math>, सबूत को रास्ते में ले जाया जा सकता है <math>p</math> संपत्ति का प्रमाण देने के लिए <math>P(b)</math>. (समकक्ष रूप से कहा गया है, प्रकार का वस्तु <math>P(a)</math> प्रकार की वस्तु में परिवर्तित किया जा सकता है <math>P(b)</math>.) यह प्रथम-क्रम तर्क#समानता और इसके स्वयंसिद्धों के अनुरूप है। यहाँ, HoTT और शास्त्रीय गणित के बीच महत्वपूर्ण अंतर आता है। शास्त्रीय गणित में, बार दो मूल्यों की समानता <math>a</math> और <math>b</math> स्थापित हो गया है, <math>a</math> और <math>b</math> इसके बाद उनके बीच किसी भी तरह के अंतर के संबंध में दूसरे के लिए इस्तेमाल किया जा सकता है। होमोटॉपी प्रकार के सिद्धांत में, हालांकि, कई अलग-अलग रास्ते हो सकते हैं <math>a = b</math>, और किसी वस्तु को दो अलग-अलग रास्तों से ले जाने से दो अलग-अलग परिणाम मिलेंगे। इसलिए, होमोटॉपी प्रकार के सिद्धांत में, प्रतिस्थापन संपत्ति को लागू करते समय, यह बताना आवश्यक है कि किस पथ का उपयोग किया जा रहा है।
-सामान्य तौर पर, एक प्रस्ताव में कई अलग-अलग प्रमाण हो सकते हैं। (उदाहरण के लिए, सभी प्राकृतिक संख्याओं का प्रकार, जब एक प्रस्ताव के रूप में माना जाता है, तो प्रत्येक प्राकृतिक संख्या एक प्रमाण के रूप में होती है।) भले ही एक प्रस्ताव के पास केवल एक प्रमाण हो <math>a</math>, रास्तों का स्थान <math>a = a</math> किसी तरह गैर-तुच्छ हो सकता है। मात्र प्रस्ताव किसी भी प्रकार का होता है जो या तो खाली होता है, या केवल एक बिंदु होता है जिसमें तुच्छ [[पथ स्थान (बीजगणितीय टोपोलॉजी)]] होता है।
+सामान्य तौर पर, प्रस्ताव में कई अलग-अलग प्रमाण हो सकते हैं। (उदाहरण के लिए, सभी प्राकृतिक संख्याओं का प्रकार, जब प्रस्ताव के रूप में माना जाता है, तो प्रत्येक प्राकृतिक संख्या प्रमाण के रूप में होती है।) भले ही प्रस्ताव के पास केवल प्रमाण हो <math>a</math>, रास्तों का स्थान <math>a = a</math> किसी तरह गैर-तुच्छ हो सकता है। मात्र प्रस्ताव किसी भी प्रकार का होता है जो या तो खाली होता है, या केवल बिंदु होता है जिसमें तुच्छ [[पथ स्थान (बीजगणितीय टोपोलॉजी)]] होता है।
 ध्यान दें कि लोग लिखते हैं <math>a = b</math> के लिए <math>Id_A(a,b)</math>,
@@ Line 123: / Line 123: @@
 === तुल्यता टाइप करें ===
-दो प्रकार <math>A</math> और <math>B</math> किसी ब्रह्मांड से संबंधित <math>U</math> समकक्ष होने के रूप में परिभाषित किया गया है यदि उनके बीच समानता मौजूद है। एक समानता एक कार्य है
+दो प्रकार <math>A</math> और <math>B</math> किसी ब्रह्मांड से संबंधित <math>U</math> समकक्ष होने के रूप में परिभाषित किया गया है यदि उनके बीच समानता मौजूद है। समानता कार्य है
 :<math>f:A \to B</math>
 जिसमें बाएँ प्रतिलोम और दाएँ प्रतिलोम दोनों हैं, इस अर्थ में कि उपयुक्त रूप से चुना गया है <math>g</math> और <math>h</math>निम्नलिखित प्रकार दोनों आबाद हैं:
@@ Line 129: / Line 129: @@
 :<math>Id_{A \rarr A}(h \circ f, id_A).</math> अर्थात।
 :<math>f \circ g =_{B\rightarrow B} id_B,</math>
-:<math>h \circ f =_{A\rightarrow A} id_A.</math> यह एक सामान्य धारणा व्यक्त करता है<math>f</math> समानता प्रकारों का उपयोग करते हुए बाएं उलटा और दायां उलटा दोनों होता है। ध्यान दें कि उपरोक्त उलटापन की स्थिति फ़ंक्शन प्रकारों में समानता प्रकार है <math>A\rarr A</math> और <math>B\rarr B</math>. एक आम तौर पर फ़ंक्शन विस्तारात्मक स्वयंसिद्ध मानता है, जो यह सुनिश्चित करता है कि ये निम्न प्रकारों के बराबर हैं जो डोमेन और कोडोमेन पर समानता का उपयोग करके इन्वर्टिबिलिटी व्यक्त करते हैं <math>A</math> और <math>B</math>:
+:<math>h \circ f =_{A\rightarrow A} id_A.</math> यह सामान्य धारणा व्यक्त करता है<math>f</math> समानता प्रकारों का उपयोग करते हुए बाएं उलटा और दायां उलटा दोनों होता है। ध्यान दें कि उपरोक्त उलटापन की स्थिति फ़ंक्शन प्रकारों में समानता प्रकार है <math>A\rarr A</math> और <math>B\rarr B</math>. आम तौर पर फ़ंक्शन विस्तारात्मक स्वयंसिद्ध मानता है, जो यह सुनिश्चित करता है कि ये निम्न प्रकारों के बराबर हैं जो डोमेन और कोडोमेन पर समानता का उपयोग करके इन्वर्टिबिलिटी व्यक्त करते हैं <math>A</math> और <math>B</math>:
 :<math>\Pi_{y:B}.\ Id_B((f \circ g)(y), id_B(y)),</math>
 :<math>\Pi_{x:A}.\ Id_A((h \circ f)(x), id_A(x)).</math> यानी सभी के लिए <math>x:A</math> और <math>y:B</math>,
@@ Line 136: / Line 136: @@
 प्रकार के कार्य
 :<math>A \to B</math>
-एक साथ एक प्रमाण के साथ कि वे तुल्यताएँ हैं, द्वारा निरूपित किया जाता है
+साथ प्रमाण के साथ कि वे तुल्यताएँ हैं, द्वारा निरूपित किया जाता है
 :<math>A \simeq B</math>.
 === एकरूपता स्वयंसिद्ध ===
-ऊपर बताए गए समतुल्य कार्यों को परिभाषित करने के बाद, कोई यह दिखा सकता है कि रास्तों को समानताओं में बदलने का एक विहित तरीका है।
+ऊपर बताए गए समतुल्य कार्यों को परिभाषित करने के बाद, कोई यह दिखा सकता है कि रास्तों को समानताओं में बदलने का विहित तरीका है।
-दूसरे शब्दों में, प्रकार का एक कार्य है
+दूसरे शब्दों में, प्रकार का कार्य है
 :<math>(A = B) \to (A \simeq B),</math>
 जो उस प्रकार को व्यक्त करता है <math>A,B</math> जो समान हैं, विशेष रूप से, समतुल्य भी हैं।
-यूनीवैलेंस एक्सिओम कहता है कि यह फंक्शन अपने आप में एक इक्वैलेंस है।<ref name=hott />{{rp|115}}<ref name= HotzelEscardo >Martín Hötzel Escardó (October 18, 2018) [https://arxiv.org/pdf/1803.02294.pdf A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom]</ref>{{rp|4-6}} इसलिए, हमारे पास है
+यूनीवैलेंस एक्सिओम कहता है कि यह फंक्शन अपने आप में इक्वैलेंस है।<ref name=hott />{{rp|115}}<ref name= HotzelEscardo >Martín Hötzel Escardó (October 18, 2018) [https://arxiv.org/pdf/1803.02294.pdf A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom]</ref>{{rp|4-6}} इसलिए, हमारे पास है
 : <math>(A = B) \simeq (A \simeq B)</math>
@@ Line 158: / Line 158: @@
-HoTT एकरूपता सिद्धांत को अपनाता है, जो तार्किक-गणितीय प्रस्तावों की समानता को होमोटॉपी सिद्धांत से संबंधित करता है। एक समीकरण जैसे a=b एक गणितीय प्रस्ताव है जिसमें दो अलग-अलग प्रतीकों का समान मान होता है। होमोटॉपी प्रकार के सिद्धांत में, इसका अर्थ यह लिया जाता है कि दो आकृतियाँ जो प्रतीकों के मूल्यों का प्रतिनिधित्व करती हैं, सांस्थितिक रूप से समतुल्य हैं।<ref name=":0" />
+HoTT एकरूपता सिद्धांत को अपनाता है, जो तार्किक-गणितीय प्रस्तावों की समानता को होमोटॉपी सिद्धांत से संबंधित करता है। समीकरण जैसे a=b गणितीय प्रस्ताव है जिसमें दो अलग-अलग प्रतीकों का समान मान होता है। होमोटॉपी प्रकार के सिद्धांत में, इसका अर्थ यह लिया जाता है कि दो आकृतियाँ जो प्रतीकों के मूल्यों का प्रतिनिधित्व करती हैं, सांस्थितिक रूप से समतुल्य हैं।<ref name=":0" />
 ईटीएच ज्यूरिख इंस्टीट्यूट फॉर थियोरेटिकल स्टडीज के निदेशक [[जॉन फेल्डर]] का तर्क है कि ये समतुल्य संबंध, होमोटोपी सिद्धांत में बेहतर रूप से तैयार किए जा सकते हैं क्योंकि यह अधिक व्यापक है: होमोटॉपी सिद्धांत न केवल बताता है कि ए बराबर बी क्यों है बल्कि यह भी बताता है कि इसे कैसे प्राप्त किया जाए। सेट थ्योरी में, इस जानकारी को अतिरिक्त रूप से परिभाषित करना होगा, जो अधिवक्ताओं का तर्क है, प्रोग्रामिंग भाषाओं में गणितीय प्रस्तावों के अनुवाद को और अधिक कठिन बना देता है।<ref name=":0" />
@@ Line 165: / Line 166: @@
 === कंप्यूटर प्रोग्रामिंग ===
 तक, होमोटोपी प्रकार के सिद्धांत में यूनीवैलेंस एक्सिओम के कम्प्यूटेशनल व्यवहार को मॉडल और औपचारिक रूप से विश्लेषण करने के लिए गहन शोध कार्य चल रहा था।<ref>{{Cite conference|url = http://dl.acm.org/citation.cfm?id=2676983|title = होमोटोपी-प्रारंभिक बीजगणित के रूप में उच्च आगमनात्मक प्रकार|last = Sojakova|first = Kristina|date = 2015|conference = POPL 2015|doi = 10.1145/2676726.2676983|arxiv = 1402.0761}}</ref>
-क्यूबिकल प्रकार का सिद्धांत होमोटॉपी प्रकार के सिद्धांत को कम्प्यूटेशनल सामग्री देने का एक प्रयास है।<ref>{{cite conference|title=Cubical Type Theory: a constructive interpretation of the univalence axiom|url=https://hal-iogs.archives-ouvertes.fr/INRIA/hal-01378906v2|last1=Cohen|first1=Cyril|last2=Coquand|first2=Thierry|last3=Huber|first3=Simon|last4=Mörtberg |first4=Anders|conference=TYPES 2015|year=2015}}</ref>
+क्यूबिकल प्रकार का सिद्धांत होमोटॉपी प्रकार के सिद्धांत को कम्प्यूटेशनल सामग्री देने का प्रयास है।<ref>{{cite conference|title=Cubical Type Theory: a constructive interpretation of the univalence axiom|url=https://hal-iogs.archives-ouvertes.fr/INRIA/hal-01378906v2|last1=Cohen|first1=Cyril|last2=Coquand|first2=Thierry|last3=Huber|first3=Simon|last4=Mörtberg |first4=Anders|conference=TYPES 2015|year=2015}}</ref>
 हालाँकि, यह माना जाता है कि कुछ वस्तुएँ, जैसे अर्ध-सरल प्रकार, सटीक समानता की कुछ धारणा के संदर्भ के बिना निर्मित नहीं की जा सकती हैं। इसलिए, विभिन्न दो-स्तरीय प्रकार के सिद्धांत विकसित किए गए हैं जो उनके प्रकारों को तंतुमय प्रकारों में विभाजित करते हैं, जो पथों का सम्मान करते हैं, और गैर-तंतुमय प्रकार, जो नहीं करते हैं। कार्टेशियन क्यूबिकल कम्प्यूटेशनल टाइप थ्योरी पहला दो-स्तरीय टाइप थ्योरी है जो होमोटॉपी टाइप थ्योरी को पूर्ण कम्प्यूटेशनल व्याख्या देता है।<ref>{{cite conference|title=Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities| last1=Anguili|first1=Carlo|last2=Favonia|last3=Harper|first3=Robert|conference=Computer Science Logic 2018|url=https://www.cs.cmu.edu/~rwh/papers/cartesian/paper.pdf|year=2018|access-date=26 Aug 2018}} (to appear)</ref>

v t e Major topics in Foundations of Mathematics
Mathematical logic	Peano axioms Mathematical induction Formal system Axiomatic system Hilbert system Natural deduction Mathematical proof Model theory Mathematical constructivism Modal logic List of mathematical logic topics
Set theory	Set Naive set theory Axiomatic set theory Zermelo set theory Zermelo–Fraenkel set theory Constructive set theory Descriptive set theory Determinacy Russell's paradox List of set theory topics
Type theory	Axiom of reducibility Simple type theory Dependent type theory Intuitionistic type theory Homotopy type theory Univalent foundations Girard's paradox
Category theory	Category Topos theory Category of sets Higher category theory ∞-groupoid ∞-topos theory Mathematical structuralism Glossary of category theory List of category theory topics

Anonymous

Search

होमोटॉपी प्रकार सिद्धांत: Difference between revisions

Namespaces

More

Page actions

Revision as of 06:17, 27 May 2023

Contents

इतिहास

प्रागितिहास: groupoid मॉडल

प्रारंभिक इतिहास: मॉडल श्रेणियां और उच्च समूह

एकरूपता स्वयंसिद्ध, सिंथेटिक होमोटॉपी सिद्धांत, और उच्च आगमनात्मक प्रकार

असमान नींव

गणित के यूनिवैलेंट फाउंडेशन पर विशेष वर्ष

मुख्य अवधारणाएँ

प्रकार के रूप में प्रस्ताव

समानता

तुल्यता टाइप करें

एकरूपता स्वयंसिद्ध

अनुप्रयोग

प्रमेय सिद्ध करना

कंप्यूटर प्रोग्रामिंग

यह भी देखें

टिप्पणियाँ

संदर्भ

ग्रन्थसूची

अग्रिम पठन

बाहरी संबंध

औपचारिक गणित के पुस्तकालय

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

होमोटॉपी प्रकार सिद्धांत: Difference between revisions

Revision as of 06:17, 27 May 2023

इतिहास

प्रागितिहास: groupoid मॉडल

प्रारंभिक इतिहास: मॉडल श्रेणियां और उच्च समूह

एकरूपता स्वयंसिद्ध, सिंथेटिक होमोटॉपी सिद्धांत, और उच्च आगमनात्मक प्रकार

असमान नींव

गणित के यूनिवैलेंट फाउंडेशन पर विशेष वर्ष

मुख्य अवधारणाएँ

प्रकार के रूप में प्रस्ताव

समानता

तुल्यता टाइप करें

एकरूपता स्वयंसिद्ध

अनुप्रयोग

प्रमेय सिद्ध करना

कंप्यूटर प्रोग्रामिंग

यह भी देखें

टिप्पणियाँ

संदर्भ

ग्रन्थसूची

अग्रिम पठन

बाहरी संबंध

औपचारिक गणित के पुस्तकालय

Navigation

Wiki tools

Page tools

Other projects

Hidden categories