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

From Vigyanwiki
No edit summary
No edit summary
 
(7 intermediate revisions by 3 users not shown)
Line 1: Line 1:
{{Short description|Type theory in logic and mathematics}}
{{Short description|Type theory in logic and mathematics}}


[[File:Hott book cover.png|thumb|होमोटॉपी टाइप थ्योरी का कवर: गणित की असमान नींव।]][[गणितीय तर्क]] और [[कंप्यूटर विज्ञान]] में, होमोटॉपी टाइप थ्योरी (HoTT {{IPAc-en|h|ɒ|t}}) अंतर्ज्ञानवादी प्रकार के सिद्धांत के विकास की विभिन्न पंक्तियों को संदर्भित करता है, जो वस्तुओं के रूप में व्याख्या के आधार पर होता है, जिस पर (अमूर्त) होमोटोपी सिद्धांत का अंतर्ज्ञान लागू होता है।
[[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]] मॉडल ===
=== प्रागितिहास: [[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-आयामी होते हैं)।
एक समय में यह विचार कि उनके पहचान प्रकारों के साथ आकस्मिक प्रकार के सिद्धांत को समूह के रूप में माना जा सकता है, गणितीय लोककथा थी। इसे पहली बार मार्टिन हॉफमैन और [[थॉमस स्ट्रीचर]] के 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 में [[स्टीव अवोडे]] और उनके छात्र माइकल वॉरेन द्वारा आकस्मिक प्रकार के सिद्धांत के पहले उच्च-आयामी मॉडल का निर्माण किया गया था। इन परिणामों को पहली बार एफएमसीएस 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>
2006 में [[उप्साला विश्वविद्यालय]] में पहचान प्रकारों के बारे में बाद की कार्यशाला में<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> और माइकल वॉरेन द्वारा, मॉडल श्रेणियां और गहन पहचान प्रकार। संबंधित विचारों पर स्टीव अवोडी, उच्च-आयामी श्रेणियों के प्रकार सिद्धांत, और थॉमस स्ट्रीचर, पहचान प्रकार बनाम कमजोर ओमेगा-ग्रुपोइड्स: कुछ विचार, कुछ समस्याएं द्वारा वार्ता में चर्चा की गई। उसी सम्मेलन में बेन्नो वैन डेन बर्ग ने कमजोर ओमेगा-श्रेणियों के प्रकार नामक वार्ता दी जहां उन्होंने उन विचारों को रेखांकित किया जो बाद में रिचर्ड गार्नर के साथ संयुक्त पत्र का विषय बन गए।
 
2006 में [[उप्साला विश्वविद्यालय]] में पहचान प्रकारों के बारे में एक बाद की फलनशाला में<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>
2007 में 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>) शीर्षक से एक वार्ता दी थी। अवोडे और वारेन ने अपने परिणामों को "पहचान प्रकारों के होमोटॉपी थ्योरिटिक मॉडल" पेपर में संक्षेपित किया, जिसे 2007<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> में [[ArXiv]] प्रीप्रिंट सर्वर पर पोस्ट किया गया था और 2009 में प्रकाशित किया गया था; 2008 में वारेन की थीसिस "रचनात्मक प्रकार के सिद्धांत के होमोटोपी सैद्धांतिक पहलुओं" में एक अधिक विस्तृत संस्करण दिखाई दिया।
2007 में 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>




=== एकरूपता स्वयंसिद्ध, सिंथेटिक होमोटॉपी सिद्धांत, और उच्च आगमनात्मक प्रकार ===
=== एकरूपता स्वयंसिद्ध, सिंथेटिक होमोटॉपी सिद्धांत, और उच्च आगमनात्मक प्रकार ===
2006 की शुरुआत में वोएवोडस्की द्वारा असमान कंपन की अवधारणा पेश की गई थी।<ref>[https://github.com/vladimirias/2006_Mar_Homotopy_lambda_calculus Notes on homotopy lambda calculus, March 2006]</ref>
2006 के प्रारंभ में वोएवोडस्की द्वारा असमान कंपन की अवधारणा प्रस्तुत की गई थी।<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 में, वोएवोडस्की ने कान परिसरों में प्रकार सिद्धांत के मॉडल के विवरण के बारे में अधिक काम किया, और देखा कि सार्वभौमिक [[कैन फाइब्रेशन]] के अस्तित्व का उपयोग प्रकार सिद्धांत के श्रेणीबद्ध मॉडल के लिए सुसंगतता की समस्याओं का समाधान करने के लिए किया जा सकता है। उन्होंने यह भी सिद्ध किया, ए.के. बोसफील्ड के विचार का उपयोग करते हुए, कि यह सार्वभौमिक कंपन एकपक्षीय था: तंतुओं के बीच जोड़ीदार होमोटॉपी समकक्षों का संबद्ध कंपन आधार के पथ-अंतरिक्ष कंपन के बराबर है।
 
स्वयंसिद्ध के रूप में एकरूपता तैयार करने के लिए वोवोडस्की ने समतुल्यता को वाक्य-विन्यास के रूप में परिभाषित करने की विधि खोजा, जिसमें महत्वपूर्ण गुण था जो कि कथन f का प्रतिनिधित्व (फलन विस्तार की धारणा के अनुसार) (-1) - छंटनी (अर्थात् यदि बसे हो तो सिकुड़ा हुआ) करने वाला प्रकार तुल्यता था। इसने उन्हें उच्च आयामों के लिए हॉफमैन और स्ट्रीचर की ब्रह्मांड की व्यापकता को सामान्य करते हुए, एकरूपता का वाक्यात्मक कथन देने में सक्षम बनाया। वह प्रमाण सहायक [[Coq]] में महत्वपूर्ण मात्रा में सिंथेटिक होमोटॉपी सिद्धांत विकसित करने के लिए समकक्षता और सिकुड़न की इन परिभाषाओं का उपयोग करने में सक्षम था; इसने लाइब्रेरी का आधार बनाया जिसे बाद में फ़ाउंडेशन और अंततः यूनीमैथ कहा गया।<ref name="UniMath">[https://github.com/UniMath/UniMath GitHub repository, Univalent Mathematics]</ref>


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


स्वयंसिद्ध के रूप में एकरूपता तैयार करने के लिए वोवोडस्की ने समतुल्यता को वाक्य-विन्यास के रूप में परिभाषित करने का तरीका खोजा, जिसमें महत्वपूर्ण गुण था कि कथन f का प्रतिनिधित्व करने वाला प्रकार तुल्यता था (फ़ंक्शन विस्तार की धारणा के तहत) (-1) - काट दिया गया (यानी अगर बसा हुआ है) . इसने उन्हें उच्च आयामों के लिए हॉफमैन और स्ट्रीचर की ब्रह्मांड की व्यापकता को सामान्य करते हुए, एकरूपता का वाक्यात्मक कथन देने में सक्षम बनाया। वह प्रूफ सहायक [[Coq]] में महत्वपूर्ण मात्रा में सिंथेटिक होमोटॉपी सिद्धांत विकसित करने के लिए समकक्षता और सिकुड़न की इन परिभाषाओं का उपयोग करने में सक्षम था; इसने लाइब्रेरी का आधार बनाया जिसे बाद में फ़ाउंडेशन और अंततः यूनीमैथ कहा गया।<ref name=UniMath>[https://github.com/UniMath/UniMath GitHub repository, Univalent Mathematics]</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 ट्यूटोरियल के भाग के रूप में, आंद्रेज बाउर ने छोटी Coq लाइब्रेरी लिखी थी<ref>[https://github.com/andrejbauer/Homotopy GitHub repository, Andrej Bauer, Homotopy theory in Coq]</ref> वोवोद्स्की के विचारों पर आधारित (किन्तु वास्तव में उनके किसी भी कोड का उपयोग नहीं); यह अंततः HoTT Coq लाइब्रेरी के पहले संस्करण (बाद की पहली प्रतिबद्धता<ref>[https://github.com/HoTT/HoTT GitHub repository, Homotopy type theory]</ref> माइकल शुलमैन ने लेडी बाउर की फाइलों पर आधारित विकास को नोट किया है, जिसमें व्लादिमीर वोवोडस्की की फाइलों से लिए गए कई विचार हैं) का कर्नेल बन गया था।<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>{{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>, क्या एकरूपता स्वयंसिद्ध में गैरमानक मॉडल (चूंकि शुलमैन द्वारा सकारात्मक उत्तर दिया गया है) और कैसे परिभाषित (अर्ध) करें सरल प्रकार (अभी भी एमएलटीटी में खुला है, चूंकि यह वोवोडस्की के होमोटॉपी टाइप सिस्टम (एचटीएस) में दो समानता प्रकारों के साथ एक प्रकार का सिद्धांत किया जा सकता है) है।
विभिन्न धागों का एकीकरण फरवरी 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>), क्या एकरूपता स्वयंसिद्ध में गैरमानक मॉडल हैं (चूंकि शुलमैन द्वारा सकारात्मक उत्तर दिया गया है), और कैसे (अर्ध) सरल प्रकारों को परिभाषित किया जाए (अभी भी एमएलटीटी में खुला है, हालांकि यह वोवोडस्की के होमोटॉपी टाइप सिस्टम (एचटीएस) में किया जा सकता है, प्रकार सिद्धांत के साथ दो समानता प्रकार)।
ओबेरवॉल्फ़ फलनशाला के तुरंत बाद, होमोटॉपी प्रकार सिद्धांत वेबसाइट और ब्लॉग<ref>[http://homotopytypetheory.org Homotopy Type Theory and Univalent Foundations Blog]</ref> की स्थापना की गई और इस नाम के अनुसार इस विषय को लोकप्रिय बनाया जाने लगा। इस अवधि के समय हुई कुछ महत्वपूर्ण प्रगति का अंदाजा ब्लॉग इतिहास से लगाया जा सकता है।<ref>[http://homotopytypetheory.org/blog Homotopy Type Theory blog]</ref>


ओबेरवॉल्फ़ कार्यशाला के तुरंत बाद, होमोटॉपी टाइप थ्योरी वेबसाइट और ब्लॉग<ref>[http://homotopytypetheory.org Homotopy Type Theory and Univalent Foundations Blog]</ref> स्थापित किया गया था, और यह विषय उसी नाम से लोकप्रिय होने लगा। इस अवधि के दौरान हुई कुछ महत्वपूर्ण प्रगति का अंदाजा ब्लॉग इतिहास से लगाया जा सकता है।<ref>[http://homotopytypetheory.org/blog Homotopy Type Theory blog]</ref>




== असमान नींव ==
== असमान नींव ==
मुहावरा असमान नींव सभी के द्वारा होमोटॉपी प्रकार के सिद्धांत से निकटता से संबंधित होने के लिए सहमत है, लेकिन हर कोई इसे उसी तरह से उपयोग नहीं करता है। यह मूल रूप से व्लादिमीर वोएवोडस्की द्वारा गणित के लिए मूलभूत प्रणाली के अपने दृष्टिकोण को संदर्भित करने के लिए उपयोग किया गया था जिसमें मूल वस्तुएं होमोटॉपी प्रकार हैं, प्रकार के सिद्धांत पर आधारित #The_univalence_axiom |<ref>[http://homotopytypetheory.org/ Type Theory and Univalent Foundations]</ref>
मुहावरा असमान नींव सभी के द्वारा होमोटॉपी प्रकार के सिद्धांत से निकटता से संबंधित होने के लिए सहमत है, किन्तु प्रत्येक कोई इसे उसी प्रकार से उपयोग नहीं करता है। यह मूल रूप से व्लादिमीर वोएवोडस्की द्वारा गणित के लिए मूलभूत प्रणाली के अपने दृष्टिकोण को संदर्भित करने के लिए उपयोग किया गया था जिसमें मूल वस्तुएं होमोटोपी प्रकार हैं, एक प्रकार के सिद्धांत पर आधारित है जो एकरूप सिद्धांत को संतुष्ट करता है, और एक कंप्यूटर प्रूफ सहायक में औपचारिक रूप दिया गया है।<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> उदाहरण के लिए, आईएएस विशेष वर्ष के विषय को आधिकारिक तौर पर एकपक्षीय नींव के रूप में दिया गया था, चूंकि वहां किए गए बहुत से काम नींव के अतिरिक्त शब्दार्थ और मेटासिद्धांत पर केंद्रित थे। आईएएस फलनक्रम में भाग लेने वालों द्वारा तैयार की गई पुस्तक का शीर्षक होमोटोपी टाइप थ्योरी: यूनीवेलेंट फाउंडेशन ऑफ मैथमेटिक्स था; चूंकि यह या तो उपयोग को संदर्भित कर सकता है, क्योंकि पुस्तक केवल 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 पुस्तक)<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 91:
{{div col end}}
{{div col end}}


ACM कम्प्यूटिंग समीक्षा ने पुस्तक को कंप्यूटिंग के गणित श्रेणी में उल्लेखनीय 2013 प्रकाशन के रूप में सूचीबद्ध किया।<ref>''ACM Computing Reviews''. [http://computingreviews.com/recommend/bestof/notableitems_2013.cfm "Best of 2013"].</ref>
एसीएम कम्प्यूटिंग समीक्षा ने पुस्तक को कंप्यूटिंग के गणित श्रेणी में उल्लेखनीय 2013 प्रकाशन के रूप में सूचीबद्ध किया था।<ref>''ACM Computing Reviews''. [http://computingreviews.com/recommend/bestof/notableitems_2013.cfm "Best of 2013"].</ref>




== मुख्य अवधारणाएँ ==
== मुख्य अवधारणाएँ ==
{| class=wikitable style="float: right; margin: 1em 0em 0em 1em;"
{| class=wikitable style="float: right; margin: 1em 0em 0em 1em;"
! Intensional type theory                                         !! Homotopy theory
! आकस्मिक प्रकार का सिद्धांत                                         !! होमोटॉपी सिद्धांत
|-
|-
| types <math>A</math>                                            || spaces <math>A</math>
| types <math>A</math>                                            || spaces <math>A</math>
Line 109: Line 115:


=== प्रकार के रूप में प्रस्ताव ===
=== प्रकार के रूप में प्रस्ताव ===
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 में, प्रकार <math>a = b</math> बिंदु <math>a</math> से बिंदु <math>b</math> तक सभी पथों का प्रकार है। (इसलिए, एक प्रमाण है कि एक बिंदु <math>a</math> एक बिंदु <math>b</math> के बराबर है, बिंदु <math>a</math> से बिंदु <math>b</math> तक के पथ के समान है।) किसी भी बिंदु के लिए, समानता की रिफ्लेक्सिव गुण के अनुरूप, प्रकार <math>a = a</math> का पथ उपस्थित है। समानता की सममित गुण के अनुरूप, प्रकार <math>b = a</math> का पथ बनाने, प्रकार <math>a = b</math> का पथ उलटा जा सकता है। <math>a = b</math> प्रकार के दो पथ क्रमशः <math>b = c</math> को श्रेणीबद्ध किया जा सकता है, जिससे <math>a = c</math> प्रकार का पथ बन सकता है; यह समानता की सकर्मक गुण के अनुरूप है।
 
सबसे महत्वपूर्ण बात यह है कि एक पथ <math>p:a=b</math> दिया गया है, और कुछ गुण <math>P(a)</math> का प्रमाण दिया गया है, तो गुण <math>P(b)</math> का प्रमाण प्राप्त करने के लिए सबूत को पथ <math>p</math> के साथ "परिवहन" किया जा सकता है। (समरूप रूप से कहा गया है, <math>P(a)</math> प्रकार की वस्तु को <math>P(b)</math> प्रकार की वस्तु में बदला जा सकता है।) यह समानता की प्रतिस्थापन गुण से मेल खाती है। यहाँ, HoTT और शास्त्रीय गणित के बीच एक महत्वपूर्ण अंतर सामने आता है। शास्त्रीय गणित में, बार दो मूल्यों की समानता स्थापित हो गया है, <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> लिखते हैं,


ध्यान दें कि लोग लिखते हैं <math>a = b</math> के लिए <math>Id_A(a,b)</math>,
जिससे <math>a, b</math> का प्रकार <math>A</math> निहित रहता है। इसे <math>id_A : A\to A</math> के साथ भ्रमित न करें, जो <math>A</math> पर पहचान फलन को दर्शाता है।{{efn|name= ttConvention|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.}}
इस प्रकार प्रकार छोड़ रहा है <math>A</math> का <math>a, b</math> अंतर्निहित।
इसके साथ भ्रमित न हों <math>id_A : A\to A</math>, पर पहचान समारोह को दर्शाते हुए <math>A</math>.{{efn|name= ttConvention|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.}}


=== तुल्यता टाइप करें ===
=== तुल्यता टाइप करें ===
दो प्रकार <math>A</math> और <math>B</math> किसी ब्रह्मांड से संबंधित <math>U</math> समकक्ष होने के रूप में परिभाषित किया गया है यदि उनके बीच समानता मौजूद है। समानता कार्य है
कुछ ब्रह्मांड <math>U</math> से संबंधित दो प्रकार <math>A</math> और <math>B</math> को समकक्ष होने के रूप में परिभाषित किया गया है यदि उनके बीच समानता उपस्थित है। एक समानता एक फलन है
:<math>f:A \to B</math>
:<math>f:A \to B</math>
जिसमें बाएँ प्रतिलोम और दाएँ प्रतिलोम दोनों हैं, इस अर्थ में कि उपयुक्त रूप से चुना गया है <math>g</math> और <math>h</math>निम्नलिखित प्रकार दोनों आबाद हैं:
जिसमें एक बायां व्युत्क्रम और एक दायां व्युत्क्रम इस अर्थ में है कि उपयुक्त रूप से चुने गए <math>g</math> और <math>h</math> के लिए निम्नलिखित प्रकार दोनों बसे हुए हैं:
:<math>Id_{B\rightarrow B}(f \circ g, id_B),</math>
:<math>Id_{B\rightarrow B}(f \circ g, id_B),</math>
:<math>Id_{A \rarr A}(h \circ f, id_A).</math> अर्थात।
:<math>Id_{A \rarr A}(h \circ f, id_A).</math>  
:अर्थात।
:<math>f \circ g =_{B\rightarrow B} id_B,</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_{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>,
:<math>\Pi_{x:A}.\ Id_A((h \circ f)(x), id_A(x)).</math>  
:अर्थात् सभी के लिए <math>x:A</math> और <math>y:B</math>,
:<math>f(g(y)) =_B y,</math>
:<math>f(g(y)) =_B y,</math>
:<math>h(f(x)) =_A x.</math>
:<math>h(f(x)) =_A x.</math>
प्रकार के कार्य
प्रकार के फलन
:<math>A \to B</math>
:<math>A \to B</math>
साथ प्रमाण के साथ कि वे तुल्यताएँ हैं, द्वारा निरूपित किया जाता है
साथ प्रमाण के साथ कि वे तुल्यताएँ हैं, द्वारा निरूपित किया जाता है
Line 140: Line 149:


=== एकरूपता स्वयंसिद्ध ===
=== एकरूपता स्वयंसिद्ध ===
ऊपर बताए गए समतुल्य कार्यों को परिभाषित करने के बाद, कोई यह दिखा सकता है कि रास्तों को समानताओं में बदलने का विहित तरीका है।
ऊपर बताए गए समतुल्य फलनों को परिभाषित करने के बाद, कोई यह दिखा सकता है कि पथों को समानताओं में बदलने का विहित विधि है।
दूसरे शब्दों में, प्रकार का कार्य है
 
दूसरे शब्दों में, प्रकार का फलन है
:<math>(A = B) \to (A \simeq B),</math>
:<math>(A = B) \to (A \simeq B),</math>
जो उस प्रकार को व्यक्त करता है <math>A,B</math> जो समान हैं, विशेष रूप से, समतुल्य भी हैं।
जो उस प्रकार को व्यक्त करता है <math>A,B</math> जो समान हैं, विशेष रूप से, समतुल्य भी हैं।
Line 150: Line 160:
दूसरे शब्दों में, पहचान समानता के बराबर है। विशेष रूप से, कोई कह सकता है कि 'समतुल्य प्रकार समान हैं'।<ref name=hott />{{rp|4}}
दूसरे शब्दों में, पहचान समानता के बराबर है। विशेष रूप से, कोई कह सकता है कि 'समतुल्य प्रकार समान हैं'।<ref name=hott />{{rp|4}}


मार्टिन होट्ज़ेल एस्कार्डो ने दिखाया है कि मार्टिन-लोफ टाइप थ्योरी (एमएलटीटी) की समानता की संपत्ति [[स्वतंत्रता (गणितीय तर्क)]] है।<ref name= HotzelEscardo/>{{rp|6}}{{efn|name=HötzelEscardó2018|1= Martín Hötzel Escardó has shown that the property of univalence, "a property of the identity type IdU of a universe U",<ref name= HotzelEscardo/>{{rp|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.<ref name= HotzelEscardo/>{{rp|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),<ref name= HotzelEscardo/>{{rp|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).<ref name= HotzelEscardo/>{{rp|3.2, p.6 The Univalence Axiom}} }}
मार्टिन होट्ज़ेल एस्कार्डो ने दिखाया है कि मार्टिन-लोफ प्रकार सिद्धांत (एमएलटीटी) की समानता की गुण [[स्वतंत्रता (गणितीय तर्क)]] है।<ref name= HotzelEscardo/>{{rp|6}}{{efn|name=HötzelEscardó2018|1= Martín Hötzel Escardó has shown that the property of univalence, "a property of the identity type IdU of a universe U",<ref name= HotzelEscardo/>{{rp|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.<ref name= HotzelEscardo/>{{rp|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),<ref name= HotzelEscardo/>{{rp|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).<ref name= HotzelEscardo/>{{rp|3.2, p.6 The Univalence Axiom}} }}


== अनुप्रयोग ==
== अनुप्रयोग ==


=== प्रमेय सिद्ध करना ===
=== प्रमेय सिद्ध करना ===
अधिवक्ताओं का दावा है कि HoTT गणितीय प्रमाणों को कंप्यूटर प्रूफ सहायकों के लिए पहले की तुलना में बहुत आसानी से [[कंप्यूटर प्रोग्रामिंग भाषा]] में अनुवादित करने की अनुमति देता है। उनका तर्क है कि यह दृष्टिकोण कंप्यूटर के लिए कठिन प्रमाणों की जांच करने की क्षमता को बढ़ाता है।<ref name=":0">{{Cite web|url = https://www.rdworldonline.com/a-new-foundation-for-mathematics|title = गणित के लिए एक नई नींव|date = 3 September 2014|access-date = 29 July 2021|publisher = R&D Magazine|last = Meyer|first = Florian}}</ref> हालाँकि, इन दावों को सार्वभौमिक रूप से स्वीकार नहीं किया जाता है और कई शोध प्रयास और प्रूफ सहायक HoTT का उपयोग नहीं करते हैं।
अधिवक्ताओं का दावा है कि HoTT गणितीय प्रमाणों को कंप्यूटर प्रमाण सहायकों के लिए पहले की तुलना में बहुत आसानी से [[कंप्यूटर प्रोग्रामिंग भाषा]] में अनुवादित करने की अनुमति देता है। उनका तर्क है कि यह दृष्टिकोण कंप्यूटर के लिए कठिन प्रमाणों की जांच करने की क्षमता को बढ़ाता है।<ref name=":0">{{Cite web|url = https://www.rdworldonline.com/a-new-foundation-for-mathematics|title = गणित के लिए एक नई नींव|date = 3 September 2014|access-date = 29 July 2021|publisher = R&D Magazine|last = Meyer|first = Florian}}</ref> चूँकि, इन दावों को सार्वभौमिक रूप से स्वीकार नहीं किया जाता है और कई शोध प्रयास और प्रमाण सहायक HoTT का उपयोग नहीं करते हैं।




Line 161: Line 171:
HoTT एकरूपता सिद्धांत को अपनाता है, जो तार्किक-गणितीय प्रस्तावों की समानता को होमोटॉपी सिद्धांत से संबंधित करता है। समीकरण जैसे a=b गणितीय प्रस्ताव है जिसमें दो अलग-अलग प्रतीकों का समान मान होता है। होमोटॉपी प्रकार के सिद्धांत में, इसका अर्थ यह लिया जाता है कि दो आकृतियाँ जो प्रतीकों के मूल्यों का प्रतिनिधित्व करती हैं, सांस्थितिक रूप से समतुल्य हैं।<ref name=":0" />
HoTT एकरूपता सिद्धांत को अपनाता है, जो तार्किक-गणितीय प्रस्तावों की समानता को होमोटॉपी सिद्धांत से संबंधित करता है। समीकरण जैसे a=b गणितीय प्रस्ताव है जिसमें दो अलग-अलग प्रतीकों का समान मान होता है। होमोटॉपी प्रकार के सिद्धांत में, इसका अर्थ यह लिया जाता है कि दो आकृतियाँ जो प्रतीकों के मूल्यों का प्रतिनिधित्व करती हैं, सांस्थितिक रूप से समतुल्य हैं।<ref name=":0" />


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




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




Line 201: Line 214:
==अग्रिम पठन==
==अग्रिम पठन==
* [[David Corfield]] (2020), ''Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy'', Oxford University Press.
* [[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.
* Egbert Rijke (2022), ''Introduction to Homotopy Type Theory'', {{arxiv|2212.11082}}. Introductory textbook.




Line 210: Line 223:
* [http://ncatlab.org/homotopytypetheory/show/HomePage Homotopy type theory wiki]
* [http://ncatlab.org/homotopytypetheory/show/HomePage Homotopy type theory wiki]
* [http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html Vladimir Voevodsky's webpage on the Univalent Foundations]
* [http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html Vladimir Voevodsky's webpage on the Univalent Foundations]
* [http://www.andrew.cmu.edu/user/awodey/htt.html Homotopy Type Theory and the Univalent Foundations of Mathematics] by Steve Awodey
* [http://www.andrew.cmu.edu/user/awodey/htt.html Homotopy Type Theory and the Univalent Foundations of Mathematics] by Steve अवोडे
* [http://video.ias.edu/univalent/awodey "Constructive Type Theory and Homotopy"] – Video lecture by Steve Awodey at the [[Institute for Advanced Study]]
* [http://video.ias.edu/univalent/awodey "Constructive Type Theory and Homotopy"] – Video lecture by Steve अवोडे at the [[Institute for Advanced Study]]




Line 234: Line 247:
श्रेणी:वीडियो क्लिप वाले लेख
श्रेणी:वीडियो क्लिप वाले लेख


 
[[Category:Collapse templates]]
[[Category: Machine Translated Page]]
[[Category:Commons category link from Wikidata]]
[[Category:Created On 24/05/2023]]
[[Category:Created On 24/05/2023]]
[[Category:Lua-based templates]]
[[Category:Machine Translated Page]]
[[Category:Multi-column templates]]
[[Category:Navigational boxes| ]]
[[Category:Navigational boxes without horizontal lists]]
[[Category:Official website not in Wikidata]]
[[Category:Pages using div col with small parameter]]
[[Category:Pages with maths render errors]]
[[Category:Pages with script errors]]
[[Category:Sidebars with styles needing conversion]]
[[Category:Template documentation pages|Documentation/doc]]
[[Category:Templates Vigyan Ready]]
[[Category:Templates generating microformats]]
[[Category:Templates that add a tracking category]]
[[Category:Templates that are not mobile friendly]]
[[Category:Templates that generate short descriptions]]
[[Category:Templates using TemplateData]]
[[Category:Templates using under-protected Lua modules]]
[[Category:Wikipedia fully protected templates|Div col]]
[[Category:Wikipedia metatemplates]]

Latest revision as of 19:06, 15 June 2023

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

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

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

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

इतिहास

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

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

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


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

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

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

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

2007 में PSSL86 में[11] अवोडे ने होमोटॉपी प्रकार सिद्धांत (यह उस शब्द का पहला सार्वजनिक उपयोग था, जिसे अवोडे द्वारा गढ़ा गया था[12]) शीर्षक से एक वार्ता दी थी। अवोडे और वारेन ने अपने परिणामों को "पहचान प्रकारों के होमोटॉपी थ्योरिटिक मॉडल" पेपर में संक्षेपित किया, जिसे 2007[13] में ArXiv प्रीप्रिंट सर्वर पर पोस्ट किया गया था और 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 ट्यूटोरियल के भाग के रूप में, आंद्रेज बाउर ने छोटी Coq लाइब्रेरी लिखी थी[21] वोवोद्स्की के विचारों पर आधारित (किन्तु वास्तव में उनके किसी भी कोड का उपयोग नहीं); यह अंततः HoTT Coq लाइब्रेरी के पहले संस्करण (बाद की पहली प्रतिबद्धता[22] माइकल शुलमैन ने लेडी बाउर की फाइलों पर आधारित विकास को नोट किया है, जिसमें व्लादिमीर वोवोडस्की की फाइलों से लिए गए कई विचार हैं) का कर्नेल बन गया था।[23] लम्सडाइन, शुलमैन, बाउर और वॉरेन के कारण, ओबेरवॉल्फ़ बैठक से निकलने वाली सबसे महत्वपूर्ण चीजों में से उच्च आगमनात्मक प्रकारों का मूल विचार था। प्रतिभागियों ने महत्वपूर्ण खुले प्रश्नों की सूची भी तैयार की, जैसे कि क्या यूनीवैलेंस एक्सिओम कैननिसिटी को संतुष्ट करता है (अभी भी खुला है, चूंकि कुछ विशेष स्थितियों को सकारात्मक रूप से समाधान किया गया है)[24][25], क्या एकरूपता स्वयंसिद्ध में गैरमानक मॉडल (चूंकि शुलमैन द्वारा सकारात्मक उत्तर दिया गया है) और कैसे परिभाषित (अर्ध) करें सरल प्रकार (अभी भी एमएलटीटी में खुला है, चूंकि यह वोवोडस्की के होमोटॉपी टाइप सिस्टम (एचटीएस) में दो समानता प्रकारों के साथ एक प्रकार का सिद्धांत किया जा सकता है) है।

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


असमान नींव

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

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


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

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

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

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

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

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

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

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


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

आकस्मिक प्रकार का सिद्धांत होमोटॉपी सिद्धांत
types spaces
terms points
dependent type fibration
identity type path space
path
homotopy


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

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

समानता

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

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

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

ध्यान दें कि लोग के लिए लिखते हैं,

जिससे का प्रकार निहित रहता है। इसे के साथ भ्रमित न करें, जो पर पहचान फलन को दर्शाता है।[lower-alpha 3]

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

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

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

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

प्रकार के फलन

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

.

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

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

दूसरे शब्दों में, प्रकार का फलन है

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

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

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

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

अनुप्रयोग

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

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


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

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


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

2015 तक, होमोटोपी प्रकार के सिद्धांत में यूनीवैलेंस एक्सिओम के कम्प्यूटेशनल व्यवहार को मॉडल और औपचारिक रूप से विश्लेषण करने के लिए आकस्मिक शोध फलन चल रहा था।[38] क्यूबिकल प्रकार का सिद्धांत होमोटॉपी प्रकार के सिद्धांत को कम्प्यूटेशनल सामग्री देने का प्रयास है।[39]

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


यह भी देखें

टिप्पणियाँ

  1. ↑ Univalence is a type, a property of the identity type IdU of a universe U —Martín Hötzel Escardó (2018)[18]: p.1 
  2. ↑ "Univalence is a type, and the univalence axiom says that this type has some inhabitant."[18]: p.1 
  3. ↑ 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.
  4. ↑ 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
  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
  19. ↑ GitHub repository, Univalent Mathematics
  20. ↑ 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.
  21. ↑ GitHub repository, Andrej Bauer, Homotopy theory in Coq
  22. ↑ GitHub repository, Homotopy type theory
  23. ↑ Bauer, Andrej; Voevodsky, Vladimir (29 April 2011). "बेसिक होमोटॉपी टाइप थ्योरी". GitHub. Retrieved 6 June 2021.
  24. ↑ Shulman, Michael (2015). "व्युत्क्रम आरेखों और समरूपता विहितता के लिए एकरूपता". Mathematical Structures in Computer Science. 25 (5): 1203–1277. arXiv:1203.3253. doi:10.1017/S0960129514000565. S2CID 13595170.
  25. ↑ Licata, Daniel R.; Harper, Robert (21 July 2011). "Canonicity for 2-Dimensional Type Theory" (PDF). Carnegie Mellon University. Retrieved 6 June 2021.
  26. ↑ Homotopy Type Theory and Univalent Foundations Blog
  27. ↑ Homotopy Type Theory blog
  28. ↑ Type Theory and Univalent Foundations
  29. ↑ 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.
  30. ↑ Homotopy Type Theory: References
  31. ↑ IAS school of mathematics: Special Year on The Univalent Foundations of Mathematics
  32. ↑ Official announcement of The HoTT Book, by Steve Awodey, 20 June 2013
  33. ↑ Monroe, D (2014). "A New Type of Mathematics?". Comm ACM. 57 (2): 13–15. doi:10.1145/2557446. S2CID 6120947.
  34. ↑ Shulman, Mike (20 June 2013). "एचओटीटी बुक". The n-Category Café. Retrieved 6 June 2021 – via University of Texas.
  35. ↑ Bauer, Andrej (20 June 2013). "एचओटीटी बुक". Mathematics and Computation. Retrieved 6 June 2021.
  36. ↑ ACM Computing Reviews. "Best of 2013".
  37. ↑ 37.0 37.1 37.2 Meyer, Florian (3 September 2014). "गणित के लिए एक नई नींव". R&D Magazine. Retrieved 29 July 2021.
  38. ↑ Sojakova, Kristina (2015). होमोटोपी-प्रारंभिक बीजगणित के रूप में उच्च आगमनात्मक प्रकार. POPL 2015. arXiv:1402.0761. doi:10.1145/2676726.2676983.
  39. ↑ Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2015). Cubical Type Theory: a constructive interpretation of the univalence axiom. TYPES 2015.
  40. ↑ 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)


ग्रन्थसूची


अग्रिम पठन

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


बाहरी संबंध

Wikimedia Commons has media related to [[commons:Category:होमोटॉपी प्रकार सिद्धांत|होमोटॉपी प्रकार सिद्धांत]].



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

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

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=होमोटॉपी_प्रकार_सिद्धांत&oldid=188355’