Homotopy type theory
गणितीय तर्क और कंप्यूटर विज्ञान में, होमोटॉपी प्रकार सिद्धांत (एचओटीटी) अंतर्ज्ञानी प्रकार सिद्धांत के विकास की विभिन्न पंक्तियों को संदर्भित करता है, जो वस्तुओं के रूप में प्रकारों की व्याख्या पर आधारित है, जिन पर (अमूर्त) होमोटॉपी सिद्धांत का अंतर्ज्ञान लागू होता है। इसमें, काम की अन्य पंक्तियों के बीच, ऐसे प्रकार के सिद्धांतों के लिए समस्थानिक और उच्च-श्रेणी के मॉडल का निर्माण शामिल है; अमूर्त समस्थानिक सिद्धांत और उच्च श्रेणी सिद्धांत के लिए एक तर्क (या आंतरिक भाषा) के रूप में प्रकार सिद्धांत का उपयोग; एक प्रकार-सैद्धांतिक नींव के भीतर गणित का विकास (जिसमें पहले से मौजूद गणित और नए गणित दोनों शामिल हैं जो समस्थानिक प्रकार संभव बनाते हैं); और कंप्यूटर प्रूफ सहायकों में इनमें से प्रत्येक का औपचारिकरण। होमोटॉपी प्रकार सिद्धांत के रूप में संदर्भित कार्य और अविभाज्य नींव परियोजना के बीच एक बड़ा ओवरलैप है। हालांकि दोनों में से किसी को भी सटीक रूप से चित्रित नहीं किया गया है, और शब्दों का उपयोग कभी-कभी एक दूसरे के स्थान पर किया जाता है, उपयोग का विकल्प भी कभी-कभी दृष्टिकोण और जोर में अंतर के अनुरूप होता है। इस प्रकार, यह लेख इन क्षेत्रों में सभी शोधकर्ताओं के विचारों को समान रूप से प्रस्तुत नहीं कर सकता है। जब कोई क्षेत्र तीव्र प्रवाह में होता है तो इस तरह की परिवर्तनशीलता अपरिहार्य होती है। इतिहास ग्रुपॉइड मॉडल एक समय में यह विचार कि गहन प्रकार के सिद्धांत में उनके पहचान प्रकारों को ग्रुपॉइड के रूप में माना जा सकता है, गणितीय लोककथा थी। इसे पहली बार मार्टिन हॉफमैन और थॉमस स्ट्रीचर के 1994 के पेपर में सटीक रूप से बनाया गया था, जिसे "ग्रुपॉइड मॉडल पहचान प्रमाण की विशिष्टता का खंडन करता है" कहा जाता है, जिसमें उन्होंने दिखाया कि इंटेंशनल टाइप थ्योरी में ग्रुपॉइड की श्रेणी में एक मॉडल था। यह प्रकार सिद्धांत का पहला सही मायने में "समस्थानिक" मॉडल था, हालांकि केवल "1-आयामी" (सेटों की श्रेणी में पारंपरिक मॉडल समस्थानिक रूप से 0-आयामी थे)। उनके अनुवर्ती पत्र ने होमोटॉपी प्रकार सिद्धांत में कई बाद के विकास का पूर्वाभास दिया। उदाहरण के लिए, उन्होंने नोट किया कि समूहबद्ध मॉडल एक नियम को संतुष्ट करता है जिसे वे "ब्रह्मांड विस्तार" कहते हैं, जो कि दस साल बाद व्लादिमीर वोवोद्स्की द्वारा प्रस्तावित 1-प्रकार के एकत्व स्वयंसिद्ध के प्रतिबंध के अलावा और कुछ नहीं है। (1-प्रकार के लिए स्वयंसिद्ध को तैयार करना विशेष रूप से सरल है, हालांकि, क्योंकि "समानता" की एक सुसंगत धारणा की आवश्यकता नहीं है। उन्होंने "समरूपता वाली श्रेणियों को समानता के रूप में परिभाषित किया" और अनुमान लगाया कि उच्च-आयामी समूह का उपयोग करने वाले मॉडल में, ऐसी श्रेणियों के लिए "समानता समानता है"; यह बाद में बेनेडिक्ट अह्रेंस, क्रिज़्ज़्टोफ़ कपुल्किन और माइकल शुलमैन द्वारा साबित किया गया था। प्रारंभिक इतिहासः मॉडल श्रेणियाँ और उच्च समूह गहन प्रकार सिद्धांत के पहले उच्च-आयामी मॉडल का निर्माण स्टीव अवोडी और उनके छात्र माइकल वारेन द्वारा 2005 में क्विलन मॉडल श्रेणियों का उपयोग करके किया गया था। इन परिणामों को पहली बार सम्मेलन एफ. एम. सी. एस. 2006 में सार्वजनिक रूप से प्रस्तुत किया गया था, जिसमें वारेन ने "तीव्र प्रकार सिद्धांत के होमोटोपी मॉडल" शीर्षक से एक व्याख्यान दिया था, जो उनके शोध प्रबंध विवरण के रूप में भी कार्य करता था (शोध प्रबंध समिति में अवोडे, निकोला गैम्बिनो और एलेक्स सिम्पसन उपस्थित थे)। सारांश वारेन की थीसिस प्रॉस्पेक्टस एब्स्ट्रैक्ट में निहित है। 2006 में उप्साला विश्वविद्यालय में पहचान के प्रकारों के बारे में एक बाद की कार्यशाला में गहन प्रकार सिद्धांत और गुणनखंडन प्रणालियों के बीच संबंध के बारे में दो चर्चाएं हुईंः एक रिचर्ड गार्नर द्वारा, "प्रकार सिद्धांत के लिए गुणनखंडन प्रणाली", और एक माइकल वारेन द्वारा, "मॉडल श्रेणियां और गहन पहचान प्रकार"। स्टीव ओवोडी, "उच्च-आयामी श्रेणियों का प्रकार सिद्धांत", और थॉमस स्ट्रीचर, "पहचान प्रकार बनाम कमजोर ऑमेगा-समूहः कुछ विचार, कुछ समस्याएं" द्वारा वार्ताओं में संबंधित विचारों पर चर्चा की गई थी। उसी सम्मेलन में बेन्नो वैन डेन बर्ग ने "कमजोर ऑमेगा-श्रेणियों के रूप में प्रकार" शीर्षक से एक व्याख्यान दिया, जिसमें उन्होंने उन विचारों को रेखांकित किया जो बाद में रिचर्ड गार्नर के साथ एक संयुक्त पत्र का विषय बन गए। उच्च आयामी मॉडल के सभी प्रारंभिक निर्माणों को आश्रित प्रकार सिद्धांत के मॉडल के विशिष्ट सुसंगतता की समस्या से निपटना था, और विभिन्न समाधान विकसित किए गए थे। ऐसा एक 2009 में वोवोडस्की द्वारा दिया गया था, दूसरा 2010 में वैन डेन बर्ग और गार्नर द्वारा दिया गया था। वोवोडस्की के निर्माण पर एक सामान्य समाधान, अंततः 2014 में लुम्सडेन और वारेन द्वारा दिया गया था। 2007 में पी. एस. एस. एल. 86 में अवोडे ने "होमोटोपी टाइप थ्योरी" शीर्षक से एक व्याख्यान दिया (यह उस शब्द का पहला सार्वजनिक उपयोग था, जिसे अवोडे ने गढ़ा था)। अवोडी और वारेन ने अपने परिणामों को "पहचान प्रकारों के होमोटोपी सैद्धांतिक मॉडल" पेपर में संक्षेपित किया, जिसे 2007 में आर्क्सिव प्रीप्रिंट सर्वर पर पोस्ट किया गया था और 2009 में प्रकाशित किया गया था; एक अधिक विस्तृत संस्करण 2008 में वारेन की थीसिस "रचनात्मक प्रकार सिद्धांत के होमोटोपी सैद्धांतिक पहलुओं" में दिखाई दिया। लगभग उसी समय, व्लादिमीर वोवोद्स्की स्वतंत्र रूप से गणित के व्यावहारिक औपचारिकरण के लिए एक भाषा की खोज के संदर्भ में प्रकार सिद्धांत की जांच कर रहे थे। सितंबर 2006 में उन्होंने टाइप मेलिंग सूची में "होमोटॉपी लैम्ब्डा कैलकुलस पर एक बहुत छोटा नोट" पोस्ट किया, जिसने आश्रित उत्पादों, योग और ब्रह्मांडों के साथ एक प्रकार सिद्धांत की रूपरेखा तैयार की और कान सरल सेटों में इस प्रकार के सिद्धांत के एक मॉडल की रूपरेखा तैयार की। यह यह कहते हुए शुरू हुआ कि "होमोटॉपी λ-कैलकुलस एक काल्पनिक (इस समय) प्रकार की प्रणाली है" और "इस समय मैंने जो ऊपर कहा है वह अनुमानों के स्तर पर है। यहाँ तक कि होमोटॉपी श्रेणी में टी. एस. के मॉडल की परिभाषा भी गैर-तुच्छ है जो जटिल सुसंगतता मुद्दों का उल्लेख करती है जिन्हें 2009 तक हल नहीं किया गया था। इस नोट में "समानता प्रकारों" की एक वाक्यात्मक परिभाषा शामिल थी जिसे पथ-स्थानों द्वारा मॉडल में व्याख्या करने का दावा किया गया था, लेकिन पहचान प्रकारों के लिए पर मार्टिन-लॉफ के नियमों पर विचार नहीं किया गया था। इसने ब्रह्मांड को आकार के अलावा समस्थानिक आयाम द्वारा भी स्तरीकृत किया, एक विचार जिसे बाद में ज्यादातर त्याग दिया गया था। वाक्यविन्यास पक्ष पर, बेन्नो वैन डेन बर्ग ने 2006 में अनुमान लगाया कि गहन प्रकार सिद्धांत में एक प्रकार के पहचान प्रकारों के टावर में एक ω-श्रेणी की संरचना होनी चाहिए, और वास्तव में एक ω-समूह होना चाहिए, माइकल बैटनिन के "गोलाकार, बीजगणितीय" अर्थ में। यह बाद में वैन डेन बर्ग और गार्नर द्वारा स्वतंत्र रूप से पेपर "टाइप्स आर वीक ओमेगा-ग्रुपॉइड्स" (2008 में प्रकाशित) में और पीटर लम्सडेन द्वारा पेपर "वीक ω-कैटेगरीज फ्रॉम इंटेंशनल टाइप थ्योरी" (2009 में प्रकाशित) में और उनके 2010 के पीएचडी थीसिस "हायर कैटेगरीज फ्रॉम टाइप थियरीज" के हिस्से के रूप में साबित किया गया था। अविभाज्य स्वयंसिद्ध, सिंथेटिक होमोटॉपी सिद्धांत और उच्च प्रेरक प्रकार एक अविभाज्य फाइब्रेशन की अवधारणा 2006 की शुरुआत में वोवोडस्की द्वारा पेश की गई थी। हालाँकि, इस संपत्ति पर मार्टिन-लॉफ प्रकार के सिद्धांत की सभी प्रस्तुतियों के आग्रह के कारण कि पहचान प्रकार, खाली संदर्भ में, केवल रिफ्लेक्सिविटी हो सकती है, वोवोड्स्की ने 2009 तक यह नहीं पहचाना कि इन पहचान प्रकारों का उपयोग अविभाज्य ब्रह्मांडों के साथ संयोजन में किया जा सकता है। विशेष रूप से, यह विचार कि मौजूदा मार्टिन-लॉफ प्रकार के सिद्धांत में एक स्वयंसिद्ध जोड़कर समानता को पेश किया जा सकता है, केवल 2009 में दिखाई दिया। इसके अलावा 2009 में, वोवोडस्की ने कान परिसरों में प्रकार सिद्धांत के एक मॉडल के अधिक विवरण पर काम किया, और देखा कि एक सार्वभौमिक कान तंतु के अस्तित्व का उपयोग प्रकार सिद्धांत के श्रेणीबद्ध मॉडल के लिए सुसंगतता समस्याओं को हल करने के लिए किया जा सकता है। उन्होंने ए. के. बोसफील्ड के एक विचार का उपयोग करते हुए यह भी साबित किया कि यह सार्वभौमिक तंतु असमान थाः तंतुओं के बीच जोड़ीदार समस्थानिक समतुल्यता का संबंधित तंतु आधार के पथ-अंतरिक्ष तंतु के बराबर है। एक स्वयंसिद्ध के रूप में एकरूपता को तैयार करने के लिए वोवोड्स्की ने "समानताओं" को वाक्यात्मक रूप से परिभाषित करने का एक तरीका खोजा जिसमें महत्वपूर्ण गुण था कि कथन "f एक समानता है" का प्रतिनिधित्व करने वाला प्रकार (फलन विस्तार की धारणा के तहत) (-1)-खंडित (यानी। यदि निवासित है तो संविदात्मक)। इसने उन्हें हॉफमैन और स्ट्रीचर की "ब्रह्मांड विस्तार" को उच्च आयामों में सामान्यीकृत करते हुए, एकरूपता का एक वाक्यात्मक कथन देने में सक्षम बनाया। वह प्रमाण सहायक सी. ओ. क्यू. में "सिंथेटिक होमोटॉपी सिद्धांत" की महत्वपूर्ण मात्रा विकसित करना शुरू करने के लिए समानताओं और संकुचनशीलता की इन परिभाषाओं का उपयोग करने में भी सक्षम थे; इसने बाद में "फाउंडेशन" और अंततः "यूनिमैथ" नामक पुस्तकालय का आधार बनाया। विभिन्न धागों का एकीकरण फरवरी 2010 में कार्नेगी मेलन विश्वविद्यालय में एक अनौपचारिक बैठक के साथ शुरू हुआ, जहां वोवोडस्की ने कान परिसरों में अपना मॉडल और अपना सी. ओ. क्यू. कोड एक समूह को प्रस्तुत किया, जिसमें अवोडे, वारेन, लम्सडेन, रॉबर्ट हार्पर, डैन लिकाटा, माइकल शुलमैन और अन्य शामिल थे। इस बैठक ने एक प्रमाण (वारेन, लुम्सडेन, लिकाटा और शुलमैन द्वारा) की रूपरेखा तैयार की कि प्रत्येक समरूपता समानता एक समानता है (वोवोड्स्की के अच्छे सुसंगत अर्थ में), जो समतुल्यता में सुधार के श्रेणी सिद्धांत के विचार पर आधारित है। इसके तुरंत बाद, वोवोडस्की ने साबित कर दिया कि एकरूपता स्वयंसिद्ध का अर्थ कार्य विस्तार है। अगला महत्वपूर्ण कार्यक्रम मार्च 2011 में ओबेरवोल्फैक के गणितीय अनुसंधान संस्थान में स्टीव ओवोडी, रिचर्ड गार्नर, पर मार्टिन-लॉफ और व्लादिमीर वोवोडस्की द्वारा आयोजित एक छोटी कार्यशाला थी, जिसका शीर्षक था "रचनात्मक प्रकार सिद्धांत की समरूपता व्याख्या"। इस कार्यशाला के लिए एक कोक ट्यूटोरियल के हिस्से के रूप में, आंद्रेज बाउर ने वोवोडस्की के विचारों के आधार पर एक छोटी सी कोक लाइब्रेरी लिखी (लेकिन वास्तव में उनके किसी भी कोड का उपयोग नहीं किया); यह अंततः "एचओटीटी" कोक लाइब्रेरी के पहले संस्करण का कर्नेल बन गया (माइकल शुलमैन द्वारा बाद वाले का पहला कमिट नोट करता है "विकास आंद्रेज बाउर की फ़ाइलों पर आधारित है, जिसमें व्लादिमीर वोवोडस्की की फ़ाइलों से लिए गए कई विचार हैं")। ओबेरवोल्फैक की बैठक से निकलने वाली सबसे महत्वपूर्ण चीजों में से एक उच्च प्रेरक प्रकारों का मूल विचार था, जो लुम्सडेन, शुलमैन, बाउर और वारेन के कारण था। प्रतिभागियों ने महत्वपूर्ण खुले प्रश्नों की एक सूची भी तैयार की, जैसे कि क्या एकरूपता स्वयंसिद्ध सिद्धांत प्रामाणिकता को संतुष्ट करता है (अभी भी खुला है, हालांकि कुछ विशेष मामलों को सकारात्मक रूप से हल किया गया है), क्या एकरूपता स्वयंसिद्ध में गैर-मानक मॉडल हैं (जब से शुलमैन द्वारा सकारात्मक उत्तर दिया गया है), और (अर्ध) सरल प्रकारों को कैसे परिभाषित किया जाए (अभी भी एमएलटीटी में खुला है, हालांकि यह वोवोडस्की के होमोटोपी टाइप सिस्टम (एचटीएस) में किया जा सकता है, जो दो समानता प्रकारों के साथ एक प्रकार सिद्धांत है)। ओबेरवोल्फैक कार्यशाला के तुरंत बाद, होमोटोपी टाइप थ्योरी वेबसाइट और ब्लॉग की स्थापना की गई, और इस विषय को उस नाम के तहत लोकप्रिय बनाया जाने लगा। इस अवधि के दौरान कुछ महत्वपूर्ण प्रगति का अंदाजा ब्लॉग इतिहास से प्राप्त किया जा सकता है। समान आधार सभी इस बात पर सहमत हैं कि वाक्यांश "समान आधार" समरूपता प्रकार सिद्धांत से निकटता से संबंधित है, लेकिन हर कोई इसे समान रूप से उपयोग नहीं करता है। इसका उपयोग मूल रूप से व्लादिमीर वोवोद्स्की द्वारा गणित के लिए एक मूलभूत प्रणाली की अपनी दृष्टि को संदर्भित करने के लिए किया गया था जिसमें मूल वस्तुएं समरूपी प्रकार हैं, जो एक प्रकार के सिद्धांत पर आधारित हैं जो § एकत्व स्वयंसिद्ध को संतुष्ट करते हैं, और एक कंप्यूटर प्रूफ सहायक में औपचारिक रूप से उपयोग किए जाते हैं। जैसे-जैसे वोवोडस्की का काम होमोटॉपी प्रकार सिद्धांत पर काम करने वाले अन्य शोधकर्ताओं के समुदाय के साथ एकीकृत हो गया, "अविभाज्य नींव" का उपयोग कभी-कभी "होमोटॉपी प्रकार सिद्धांत" के साथ किया जाता था, और अन्य बार केवल एक मूलभूत प्रणाली के रूप में इसके उपयोग को संदर्भित करने के लिए (उदाहरण के लिए, मॉडल-श्रेणीगत शब्दार्थ या कम्प्यूटेशनल मेटाथियरी के अध्ययन को छोड़कर)। उदाहरण के लिए, आई. ए. एस. विशेष वर्ष के विषय को आधिकारिक तौर पर "अविभाज्य नींव" के रूप में दिया गया था, हालांकि वहां किया गया बहुत काम नींव के अलावा शब्दार्थ और मेटाथियरी पर केंद्रित था। आई. ए. एस. कार्यक्रम में प्रतिभागियों द्वारा निर्मित पुस्तक का शीर्षक "होमोटोपी प्रकार सिद्धांतः गणित की अविभाज्य नींव" था; हालाँकि यह किसी भी उपयोग को संदर्भित कर सकता है, क्योंकि पुस्तक में केवल एच. ओ. टी. टी. को गणितीय आधार के रूप में चर्चा की गई है। इंस्टीट्यूट फॉर एडवांस्ड स्टडी के शोधकर्ताओं ने "गणित की अद्वितीय नींव पर एक विशेष वर्ष" का आयोजन किया। विशेष वर्ष ने टोपोलॉजी, कंप्यूटर विज्ञान, श्रेणी सिद्धांत और गणितीय तर्क में शोधकर्ताओं को एक साथ लाया। कार्यक्रम का आयोजन स्टीव अवोडे, थिएरी कोक्वांड और व्लादिमीर वोवोडस्की द्वारा किया गया था। कार्यक्रम के दौरान पीटर एक्ज़ेल, जो प्रतिभागियों में से एक थे, ने एक कार्य समूह की शुरुआत की जिसने जाँच की कि प्रकार सिद्धांत को अनौपचारिक रूप से लेकिन सख्ती से कैसे किया जाए, एक ऐसी शैली में जो सेट सिद्धांत करने वाले सामान्य गणितविदों के समान है। प्रारंभिक प्रयोगों के बाद यह स्पष्ट हो गया कि यह न केवल संभव था बल्कि अत्यधिक फायदेमंद था, और यह कि एक पुस्तक (तथाकथित एचओटीटी पुस्तक) लिखी जा सकती थी और लिखी जानी चाहिए। परियोजना के कई अन्य प्रतिभागी तब तकनीकी सहायता, लेखन, प्रूफ रीडिंग और विचारों की पेशकश के साथ प्रयास में शामिल हुए। असामान्य रूप से एक गणित पाठ के लिए, इसे सहयोगात्मक रूप से और गिटहब पर खुले में विकसित किया गया था, जिसे क्रिएटिव कॉमन्स लाइसेंस के तहत जारी किया गया है जो लोगों को पुस्तक के अपने संस्करण को फाँटने की अनुमति देता है, और इसे प्रिंट में खरीदा जा सकता है और मुफ्त में डाउनलोड किया जा सकता है। आम तौर पर, विशेष वर्ष पूरे विषय के विकास के लिए एक उत्प्रेरक था; एचओटीटी पुस्तक केवल एक थी, हालांकि सबसे अधिक दिखाई देने वाला, परिणाम। विशेष वर्ष में आधिकारिक प्रतिभागियों पीटर एज़ेल बेनेडिक्ट अह्रेंस थोर्स्टन एल्टेंकिर्च स्टीव अवोडे ब्रूनो बैरास आंद्रेज बाउर यवेस बर्टोट मार्क बेज़ेम थिएरी कोक्वांड एरिक फ़िन्स्टर डैनियल ग्रेसन ह्यूगो हर्बेलिन आंद्रे जॉयल डैन लिकाटा पीटर लुम्सडेन एसिया महबूबबी पर मार्टिन-लॉफ़ सर्गेई मेलिखोव अल्वारो पेलायो एंड्रयू पोलोंस्की माइकल शुलमैन मैथ्यू सोज़ो स्पिटर्स बेनो वैन डेन बर्ग व्लादिमीर वोवोडस्की माइकल वारेन नोम ज़ीलबर्गर एसीएम कम्प्यूटिंग रिव्यूज़ ने पुस्तक को "मैथमेटिक्स ऑफ़ कंप्यूटिंग" श्रेणी में 2013 के उल्लेखनीय प्रकाशन के रूप में सूचीबद्ध किया। प्रमुख अवधारणाएँ "प्रकार के रूप में प्रस्ताव" एचओटीटी प्रकार सिद्धांत की "प्रकार के रूप में प्रस्ताव" व्याख्या के एक संशोधित संस्करण का उपयोग करता है, जिसके अनुसार प्रकार भी प्रस्तावों का प्रतिनिधित्व कर सकते हैं और शब्द फिर प्रमाणों का प्रतिनिधित्व कर सकते हैं। एच. ओ. टी. टी. में, हालांकि, मानक "प्रकार के रूप में प्रस्तावों" के विपरीत, एक विशेष भूमिका 'मात्र प्रस्तावों' द्वारा निभाई जाती है, जो मोटे तौर पर, प्रस्तावात्मक समानता तक अधिकतम एक शब्द वाले प्रकार हैं। ये सामान्य प्रकारों की तुलना में पारंपरिक तार्किक प्रस्तावों की तरह हैं, क्योंकि वे प्रमाण-अप्रासंगिक हैं। समानता समरूपता प्रकार सिद्धांत की मौलिक अवधारणा मार्ग है। एचओटीटी में, प्रकार बिंदु से बिंदु तक सभी रास्तों का प्रकार है। (इसलिए, एक प्रमाण कि एक बिंदु एक बिंदु के बराबर है, वह बिंदु से बिंदु तक के मार्ग के समान है।) किसी भी बिंदु के लिए, समानता के प्रतिवर्त गुण के अनुरूप प्रकार का एक मार्ग मौजूद है। एक प्रकार के पथ को उल्टा किया जा सकता है, जो समानता के सममित गुण के अनुरूप एक प्रकार का पथ बनाता है। रेस्प प्रकार के दो मार्ग। एक प्रकार का मार्ग बनाते हुए इसे संयोजित किया जा सकता है; यह समानता के सकर्मक गुण से मेल खाता है। सबसे महत्वपूर्ण बात यह है कि एक मार्ग और कुछ संपत्ति का प्रमाण दिए जाने पर, संपत्ति का प्रमाण देने के लिए प्रमाण को रास्ते में "ले जाया" जा सकता है। (समान रूप से कहा गया है, एक प्रकार की वस्तु को एक प्रकार की वस्तु में बदला जा सकता है।) यह समानता के प्रतिस्थापन गुण से मेल खाता है। यहाँ, एचओटीटी और शास्त्रीय गणित के बीच एक महत्वपूर्ण अंतर आता है। शास्त्रीय गणित में, एक बार दो मूल्यों की समानता स्थापित हो गई है, और उसके बाद उनके बीच किसी भी अंतर की परवाह किए बिना, एक दूसरे के स्थान पर उपयोग किया जा सकता है। होमोटॉपी प्रकार सिद्धांत में, हालांकि, कई अलग-अलग रास्ते हो सकते हैं, और एक वस्तु को दो अलग-अलग रास्तों पर ले जाने से दो अलग-अलग परिणाम मिलेंगे। इसलिए, होमोटॉपी प्रकार सिद्धांत में, प्रतिस्थापन गुण को लागू करते समय, यह बताना आवश्यक है कि किस पथ का उपयोग किया जा रहा है। सामान्य तौर पर, एक "प्रस्ताव" में कई अलग-अलग प्रमाण हो सकते हैं। (उदाहरण के लिए, सभी प्राकृतिक संख्याओं के प्रकार, जब एक प्रस्ताव के रूप में माना जाता है, तो प्रमाण के रूप में प्रत्येक प्राकृतिक संख्या होती है।) भले ही किसी प्रस्ताव के पास केवल एक प्रमाण हो, पथ का स्थान किसी न किसी तरह से गैर-तुच्छ हो सकता है। एक "मात्र प्रस्ताव" कोई भी प्रकार है जो या तो खाली है, या एक तुच्छ पथ स्थान के साथ केवल एक बिंदु रखता है। ध्यान दें कि लोग इसके लिए लिखते हैं, जिससे अंतर्निहित के प्रकार को छोड़ दिया जाता है। आइडेंटिटी फंक्शन के साथ इसे भ्रमित न करें। प्रकार समतुल्यता दो प्रकार और कुछ ब्रह्मांड से संबंधित को समतुल्य होने के रूप में परिभाषित किया जाता है यदि उनके बीच कोई समतुल्यता मौजूद है। समतुल्यता एक ऐसा फलन है जिसमें बाएँ व्युत्क्रम और दाएँ व्युत्क्रम दोनों होते हैं, इस अर्थ में कि उपयुक्त रूप से चुने जाने के लिए और निम्नलिखित प्रकार दोनों ही आबाद हैंः अर्थात। यह समानता प्रकारों का उपयोग करते हुए "बाएं व्युत्क्रम और दाएं व्युत्क्रम दोनों" की एक सामान्य धारणा को व्यक्त करता है। ध्यान दें कि उपरोक्त व्युत्क्रमता स्थितियाँ फलन प्रकार और में समानता प्रकार हैं। एक आम तौर पर कार्य विस्तार स्वयंसिद्ध मानता है, जो यह सुनिश्चित करता है कि ये निम्नलिखित प्रकारों के बराबर हैं जो डोमेन और कोडोमैन पर समानता का उपयोग करके व्युत्क्रमता को व्यक्त करते हैं और अर्थात्ः सभी के लिए और, प्रकार के कार्यों को एक प्रमाण के साथ दर्शाया जाता है कि वे समतुल्य हैं। समानतावाद स्वयंसिद्ध उन कार्यों को परिभाषित करने के बाद जो ऊपर के रूप में समतुल्य हैं, कोई यह दिखा सकता है कि समतुल्यता के लिए पथ को बदलने का एक विहित तरीका है। दूसरे शब्दों में, उस प्रकार का एक कार्य है जो व्यक्त करता है कि जो प्रकार समान हैं, विशेष रूप से, वे भी समतुल्य हैं। एकरूपता स्वयंसिद्ध में कहा गया है कि यह फलन अपने आप में एक समतुल्यता है। इसलिए, हमारे पास "दूसरे शब्दों में, पहचान समतुल्यता के बराबर है। विशेष रूप से, कोई कह सकता है कि 'समतुल्य प्रकार समान हैं'। मार्टिन होट्ज़ेल एस्कार्डो ने दिखाया है कि एकरूपता का गुण मार्टिन-लॉफ प्रकार सिद्धांत (एमएलटीटी) से स्वतंत्र है। एप्लीकेशन थ्योरम साबित करने वाले अधिवक्ताओं का दावा है कि एचओटीटी गणितीय प्रमाणों को कंप्यूटर प्रूफ सहायकों के लिए कंप्यूटर प्रोग्रामिंग भाषा में पहले की तुलना में बहुत आसानी से अनुवादित करने की अनुमति देता है। उनका तर्क है कि यह दृष्टिकोण कंप्यूटर के लिए कठिन प्रमाणों की जांच करने की क्षमता को बढ़ाता है। हालाँकि, इन दावों को सार्वभौमिक रूप से स्वीकार नहीं किया जाता है और कई शोध प्रयास और प्रमाण सहायक एचओटीटी का उपयोग नहीं करते हैं। एचओटीटी एकत्व स्वयंसिद्ध को अपनाता है, जो तार्किक-गणितीय प्रस्तावों की समानता को समरूपता सिद्धांत से संबंधित करता है। "a = b" जैसे समीकरण एक गणितीय प्रस्ताव है जिसमें दो अलग-अलग प्रतीकों का मूल्य समान होता है। होमोटॉपी प्रकार सिद्धांत में, इसका अर्थ यह लिया जाता है कि दो आकृतियाँ जो प्रतीकों के मूल्यों का प्रतिनिधित्व करती हैं, वे स्थलाकृतिक रूप से समतुल्य हैं। ई. टी. एच. ज्यूरिख इंस्टीट्यूट फॉर थियोरेटिकल स्टडीज के निदेशक जियोवन्नी फेल्डर का तर्क है कि इन समानता संबंधों को होमोटॉपी सिद्धांत में बेहतर तरीके से तैयार किया जा सकता है क्योंकि यह अधिक व्यापक हैः होमोटॉपी सिद्धांत न केवल बताता है कि "ए बी के बराबर क्यों है" बल्कि यह भी बताता है कि इसे कैसे प्राप्त किया जाए। सेट सिद्धांत में, इस जानकारी को अतिरिक्त रूप से परिभाषित करना होगा, जो अधिवक्ताओं का तर्क है कि गणितीय प्रस्तावों का प्रोग्रामिंग भाषाओं में अनुवाद करना अधिक कठिन बनाता है। कंप्यूटर प्रोग्रामिंग 2015 तक, होमोटॉपी प्रकार सिद्धांत में अविभाज्य स्वयंसिद्ध के कम्प्यूटेशनल व्यवहार को मॉडल और औपचारिक रूप से विश्लेषण करने के लिए गहन शोध कार्य चल रहा था। क्यूबिकल टाइप थ्योरी होमोटॉपी टाइप थ्योरी को कम्प्यूटेशनल सामग्री देने का एक प्रयास है। हालांकि, यह माना जाता है कि कुछ वस्तुओं, जैसे कि अर्ध-सरल प्रकार, का निर्माण सटीक समानता की कुछ धारणा के संदर्भ के बिना नहीं किया जा सकता है। इसलिए, विभिन्न दो-स्तरीय प्रकार के सिद्धांत विकसित किए गए हैं जो अपने प्रकार को रेशेदार प्रकारों में विभाजित करते हैं, जो पथ का सम्मान करते हैं, और गैर-रेशेदार प्रकार, जो नहीं करते हैं। कार्टेशियन क्यूबिकल कम्प्यूटेशनल प्रकार सिद्धांत पहला दो-स्तरीय प्रकार का सिद्धांत है जो होमोटॉपी प्रकार सिद्धांत को एक पूर्ण कम्प्यूटेशनल व्याख्या देता है। करी-हॉवर्ड पत्राचार अंतर्ज्ञानी प्रकार सिद्धांत की गणना भी देखें होमोटोपी परिकल्पना अविभाज्य नींव नोट्स संदर्भ ग्रंथ सूची (इस लेख में उद्धृत गिटहब संस्करण)। पी. डी. एफ. के रूप में। पोस्टस्क्रिप्ट के रूप में। आगे पढ़ने के लिए डेविड कॉर्फील्ड (2020), मॉडल होमोटोपी टाइप थ्योरीः द प्रॉस्पेक्ट ऑफ ए न्यू लॉजिक फॉर फिलॉसफी, ऑक्सफोर्ड यूनिवर्सिटी प्रेस। एगबर्ट रिजके (2022), होमोटोपी प्रकार सिद्धांत का परिचय। परिचयात्मक पाठ्यपुस्तक। बाहरी लिंक होमोटोपी प्रकार सिद्धांत विकि व्लादिमीर वोवोडस्की का वेबपेज अद्वितीय नींव होमोटोपी प्रकार सिद्धांत और स्टीव ओवोडी द्वारा गणित की अद्वितीय नींव "रचनात्मक प्रकार सिद्धांत और होमोटोपी"-औपचारिक गणित के उन्नत अध्ययन पुस्तकालय संस्थान में स्टीव ओवोडी द्वारा वीडियो व्याख्यान (अब यूनिमैथ में एकीकृत, जहां आगे विकास होता है) गणित प्रकार सिद्धांत की नींव होमोटोपी सिद्धांत औपचारिक विधियाँ वीडियो क्लिप वाले लेख