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

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

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

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

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

इतिहास

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

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

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

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

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

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

उच्च आयामी मॉडल के सभी प्रारंभिक निर्माणों को निर्भर प्रकार के सिद्धांत के मॉडल के विशिष्ट सुसंगतता की समस्या से निपटना था, और विभिन्न समाधान विकसित किए गए थे। ऐसा ही एक 2009 में वोवोडस्की द्वारा दिया गया था, दूसरा 2010 में वैन डेन बर्ग और गार्नर द्वारा दिया गया था। एक सामान्य समाधान, वोवोडस्की के निर्माण पर निर्माण, अंततः 2014 में लम्सडाइन और वॉरेन द्वारा दिया गया था।

2007 में PSSL86 में अवोडे ने होमोटॉपी प्रकार सिद्धांत (यह उस शब्द का पहला सार्वजनिक उपयोग था, जिसे अवोडे द्वारा गढ़ा गया था) शीर्षक से एक वार्ता दी थी। अवोडे और वारेन ने अपने परिणामों को "पहचान प्रकारों के होमोटॉपी थ्योरिटिक मॉडल" पेपर में संक्षेपित किया, जिसे 2007 में ArXiv प्रीप्रिंट सर्वर पर पोस्ट किया गया था और 2009 में प्रकाशित किया गया था; 2008 में वारेन की थीसिस "रचनात्मक प्रकार के सिद्धांत के होमोटोपी सैद्धांतिक पहलुओं" में एक अधिक विस्तृत संस्करण दिखाई दिया।

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

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

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

2006 के प्रारंभ में वोएवोडस्की द्वारा असमान कंपन की अवधारणा प्रस्तुत की गई थी।

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

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

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

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

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

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

असमान नींव

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

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

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

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

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

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

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

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

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

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

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

आकस्मिक प्रकार का सिद्धांत	होमोटॉपी सिद्धांत
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 में, प्रकार $a=b$ बिंदु $a$ से बिंदु $b$ तक सभी पथों का प्रकार है। (इसलिए, एक प्रमाण है कि एक बिंदु $a$ एक बिंदु $b$ के बराबर है, बिंदु $a$ से बिंदु $b$ तक के पथ के समान है।) किसी भी बिंदु के लिए, समानता की रिफ्लेक्सिव गुण के अनुरूप, प्रकार $a=a$ का पथ उपस्थित है। समानता की सममित गुण के अनुरूप, प्रकार $b=a$ का पथ बनाने, प्रकार $a=b$ का पथ उलटा जा सकता है। $a=b$ प्रकार के दो पथ क्रमशः $b=c$ को श्रेणीबद्ध किया जा सकता है, जिससे $a=c$ प्रकार का पथ बन सकता है; यह समानता की सकर्मक गुण के अनुरूप है।

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

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

ध्यान दें कि लोग $a=b$ के लिए $Id_{A}(a,b)$ लिखते हैं,

जिससे $a,b$ का प्रकार $A$ निहित रहता है। इसे $id_{A}:A\to A$ के साथ भ्रमित न करें, जो $A$ पर पहचान फलन को दर्शाता है।

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

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

$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 अवोडे
• "Constructive Type Theory and Homotopy" – Video lecture by Steve अवोडे 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

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