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

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

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

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

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

इतिहास

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

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

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

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

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

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

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

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

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

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

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

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

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

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

असमान नींव

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

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

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

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

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

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

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

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

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

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

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$.

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

दो प्रकार $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$ जो समान हैं, विशेष रूप से, समतुल्य भी हैं।

यूनीवैलेंस एक्सिओम कहता है कि यह फंक्शन अपने आप में एक इक्वैलेंस है। इसलिए, हमारे पास है

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

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

मार्टिन होट्ज़ेल एस्कार्डो ने दिखाया है कि मार्टिन-लोफ टाइप थ्योरी (एमएलटीटी) की समानता की संपत्ति स्वतंत्रता (गणितीय तर्क) है।

अनुप्रयोग

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

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

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

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

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

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

यह भी देखें

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

ग्रन्थसूची

• 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

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