Homotopy type theory
கணித தர்க்கம் மற்றும் கணினி அறிவியலில், ஹோமோடாபி வகைக் கோட்பாடு (எச்ஓடிடி) என்பது உள்ளுணர்வு வகைக் கோட்பாட்டின் வளர்ச்சியின் பல்வேறு வரிகளைக் குறிக்கிறது, இது (சுருக்கமான) ஹோமோடாபி கோட்பாட்டின் உள்ளுணர்வு பொருந்தும் பொருள்களாக வகைகளின் விளக்கத்தை அடிப்படையாகக் கொண்டது. இது மற்ற பணிகளில் அடங்கும், அத்தகைய வகைக் கோட்பாடுகளுக்கான ஒரே மாதிரியான மற்றும் உயர் வகை மாதிரிகளின் கட்டுமானம்; சுருக்கமான ஒரே மாதிரியான கோட்பாடு மற்றும் உயர் வகைக் கோட்பாட்டிற்கான ஒரு தர்க்கமாக (அல்லது உள் மொழி) வகைக் கோட்பாட்டைப் பயன்படுத்துதல்; ஒரு வகை-கோட்பாட்டு அடித்தளத்திற்குள் கணிதத்தின் வளர்ச்சி (முன்பு இருந்த கணிதம் மற்றும் ஒரே மாதிரியான வகைகளை சாத்தியமாக்கும் புதிய கணிதம் உட்பட); மற்றும் கணினி ஆதார உதவியாளர்களில் இவை ஒவ்வொன்றையும் முறைப்படுத்துதல். ஹோமோடாபி வகை கோட்பாடு என்று குறிப்பிடப்படும் வேலைக்கும், சமமற்ற அடித்தளங்கள் திட்டத்திற்கும் இடையே ஒரு பெரிய ஒன்றுடன் ஒன்று உள்ளது. இரண்டுமே துல்லியமாக வரையறுக்கப்படவில்லை என்றாலும், சில நேரங்களில் சொற்கள் ஒன்றுக்கொன்று மாற்றாகப் பயன்படுத்தப்படுகின்றன, பயன்பாட்டின் தேர்வும் சில நேரங்களில் கண்ணோட்டம் மற்றும் வலியுறுத்தலில் உள்ள வேறுபாடுகளுடன் ஒத்திருக்கிறது. எனவே, இந்தக் கட்டுரை இந்தத் துறைகளில் உள்ள அனைத்து ஆராய்ச்சியாளர்களின் கருத்துகளையும் சமமாக பிரதிநிதித்துவப்படுத்தாமல் போகலாம். ஒரு புலம் விரைவான பாய்ச்சலில் இருக்கும்போது இந்த வகையான மாறுபாடு தவிர்க்க முடியாதது. வரலாறு குரூபாய்டு மாதிரி ஒரு காலத்தில் தீவிர வகை கோட்பாட்டில் அவற்றின் அடையாள வகைகளுடன் வகைப்படுத்தப்படுவதை குரூபாய்டுகளாகக் கருதலாம் என்ற கருத்து கணித நாட்டுப்புறக் கதையாக இருந்தது. மார்ட்டின் ஹாஃப்மேன் மற்றும் தாமஸ் ஸ்ட்ரீச்சர் ஆகியோரின் 1994 ஆம் ஆண்டு ஆய்வறிக்கையில் "குரூபாய்டு மாதிரி அடையாளச் சான்றுகளின் தனித்துவத்தை நிராகரிக்கிறது" என்று அழைக்கப்பட்ட ஆய்வறிக்கையில் இது முதன்முதலில் துல்லியமான சொற்பொருளாக செய்யப்பட்டது, இதில் தீவிர வகைக் கோட்பாடு குரூபாய்டுகளின் பிரிவில் ஒரு மாதிரியைக் கொண்டுள்ளது என்பதை அவர்கள் காட்டினர். இது வகைக் கோட்பாட்டின் முதல் உண்மையான "ஒரே மாதிரியான" மாதிரியாகும், இருப்பினும் "1-பரிமாணம்" மட்டுமே (தொகுப்புகளின் பிரிவில் உள்ள பாரம்பரிய மாதிரிகள் ஒரே மாதிரியாக 0-பரிமாணமாக உள்ளன). அவர்களின் பின்தொடர்தல் கட்டுரை ஹோமோடாபி வகை கோட்பாட்டில் பல பிற்கால முன்னேற்றங்களை முன்னறிவித்தது. உதாரணமாக, குரூபாய்டு மாதிரி "பிரபஞ்ச விரிவாக்கம்" என்று அவர்கள் அழைத்த ஒரு விதியை திருப்திப்படுத்துகிறது என்று அவர்கள் குறிப்பிட்டனர், இது பத்து ஆண்டுகளுக்குப் பிறகு விளாடிமிர் வோவோட்ஸ்கி முன்மொழிந்த ஒற்றுமை கோட்பாட்டின் 1-வகையான கட்டுப்பாடு தவிர வேறில்லை. (1-வகைகளுக்கான கோட்பாட்டை உருவாக்குவது குறிப்பிடத்தக்க வகையில் எளிதானது, இருப்பினும், "சமநிலை" பற்றிய ஒத்திசைவான கருத்து தேவையில்லை என்பதால்.) அவர்கள் "ஐசோமார்பிசத்துடன் கூடிய வகைகளை சமத்துவம்" என்றும் வரையறுத்தனர், மேலும் உயர் பரிமாண குழுமங்களைப் பயன்படுத்தும் ஒரு மாதிரியில், அத்தகைய வகைகளுக்கு ஒருவர் "சமநிலை என்பது சமத்துவம்" என்று அனுமானித்தனர்; இது பின்னர் பெனடிக்ட் அஹ்ரென்ஸ், கிரிஸ்டோஃப் கபுல்கின் மற்றும் மைக்கேல் ஷுல்மேன் ஆகியோரால் நிரூபிக்கப்பட்டது. ஆரம்பகால வரலாறுஃ மாதிரி பிரிவுகள் மற்றும் உயர் குழுக்கள் தீவிர வகை கோட்பாட்டின் முதல் உயர் பரிமாண மாதிரிகள் ஸ்டீவ் அவோடியும் அவரது மாணவர் மைக்கேல் வாரனும் 2005 ஆம் ஆண்டில் குய்லன் மாதிரி வகைகளைப் பயன்படுத்தி உருவாக்கினர். இந்த முடிவுகள் முதன்முதலில் எஃப்எம்சிஎஸ் 2006 மாநாட்டில் பொதுவில் முன்வைக்கப்பட்டன, அதில் வாரன் "தீவிர வகை கோட்பாட்டின் ஹோமோடோபி மாதிரிகள்" என்ற தலைப்பில் ஒரு உரையை நிகழ்த்தினார், இது அவரது ஆய்வறிக்கை ஆவணமாகவும் செயல்பட்டது (ஆய்வுக் குழுவில் அவோடி, நிக்கோலா காம்பினோ மற்றும் அலெக்ஸ் சிம்ப்சன் ஆகியோர் கலந்து கொண்டனர்). ஒரு சுருக்கம் வாரனின் ஆய்வறிக்கை பிராஸ்பெக்டஸ் சுருக்கத்தில் உள்ளது. 2006 ஆம் ஆண்டில் உப்சாலா பல்கலைக்கழகத்தில் அடையாள வகைகள் பற்றிய அடுத்தடுத்த பட்டறையில் தீவிர வகை கோட்பாடு மற்றும் காரணிமயமாக்கல் அமைப்புகளுக்கு இடையிலான உறவு குறித்து இரண்டு பேச்சுக்கள் இருந்தனஃ ஒன்று ரிச்சர்ட் கார்னர், "வகை கோட்பாட்டிற்கான காரணிமயமாக்கல் அமைப்புகள்", மற்றும் ஒன்று மைக்கேல் வாரன், "மாதிரி பிரிவுகள் மற்றும் தீவிர அடையாள வகைகள்". ஸ்டீவ் அவோடி, "உயர் பரிமாண வகைகளின் வகைக் கோட்பாடு", மற்றும் தாமஸ் ஸ்ட்ரீச்சர், "அடையாள வகைகள் எதிராக பலவீனமான ஒமேகா-குழுக்கள்ஃ சில கருத்துக்கள், சில சிக்கல்கள்" ஆகியோரின் பேச்சுகளில் தொடர்புடைய கருத்துக்கள் விவாதிக்கப்பட்டன. அதே மாநாட்டில் பென்னோ வான் டென் பெர்க் "பலவீனமான ஒமேகா வகைகளாக வகைகள்" என்ற தலைப்பில் ஒரு உரையை நிகழ்த்தினார், அங்கு அவர் ரிச்சர்ட் கார்னருடன் ஒரு கூட்டு ஆய்வறிக்கையின் பொருளாக மாறிய கருத்துக்களை கோடிட்டுக் காட்டினார். உயர் பரிமாண மாதிரிகளின் அனைத்து ஆரம்ப கட்டமைப்புகளும் சார்பு வகை கோட்பாட்டின் மாதிரிகளின் பொதுவான ஒத்திசைவின் சிக்கலைக் கையாள வேண்டியிருந்தது, மேலும் பல்வேறு தீர்வுகள் உருவாக்கப்பட்டன. அத்தகைய ஒன்று 2009 இல் வோவோட்ஸ்கியால் வழங்கப்பட்டது, மற்றொன்று 2010 இல் வான் டென் பெர்க் மற்றும் கார்னர் ஆகியோரால் வழங்கப்பட்டது. வோவோட்ஸ்கியின் கட்டுமானத்தை அடிப்படையாகக் கொண்ட ஒரு பொதுவான தீர்வு, இறுதியில் லும்ஸ்டைன் மற்றும் வாரன் ஆகியோரால் 2014 இல் வழங்கப்பட்டது. 2007 ஆம் ஆண்டில் பி. எஸ். எஸ். எல் 86 இல் அவோடி "ஹோமோடோபி வகை கோட்பாடு" என்ற தலைப்பில் ஒரு உரையை நிகழ்த்தினார் (இது அவோடி உருவாக்கிய அந்த வார்த்தையின் முதல் பொதுப் பயன்பாடாகும்). அவோடியும் வாரனும் தங்கள் முடிவுகளை "அடையாள வகைகளின் ஹோமோடோபி கோட்பாட்டு மாதிரிகள்" என்ற கட்டுரையில் சுருக்கமாகக் கூறினர், இது 2007 இல் ஆர்க்ஸிவ் முன் அச்சு சேவையகத்தில் வெளியிடப்பட்டு 2009 இல் வெளியிடப்பட்டது; 2008 இல் வாரனின் ஆய்வறிக்கையான "ஆக்கபூர்வமான வகை கோட்பாட்டின் ஹோமோடோபி கோட்பாட்டு அம்சங்கள்" இல் இன்னும் விரிவான பதிப்பு தோன்றியது. ஏறக்குறைய அதே நேரத்தில், விளாடிமிர் வோவோட்ஸ்கி கணிதத்தின் நடைமுறை முறைப்படுத்தலுக்கான ஒரு மொழியைத் தேடும் சூழலில் வகைக் கோட்பாட்டை சுயாதீனமாக ஆராய்ந்தார். செப்டம்பர் 2006 இல் அவர் வகை அஞ்சல் பட்டியலில் "ஹோமோடாபி லாம்ப்டா கால்குலஸ் பற்றிய ஒரு குறுகிய குறிப்பு" என்ற பதிவை வெளியிட்டார், இது சார்பு தயாரிப்புகள், தொகைகள் மற்றும் பிரபஞ்சங்களுடன் ஒரு வகை கோட்பாட்டின் வெளிப்புறங்களையும், கான் எளிமையான தொகுப்புகளில் இந்த வகை கோட்பாட்டின் மாதிரியையும் வரைந்தது. இது "ஹோமோடாபி λ-கால்குலஸ் ஒரு கற்பனையான (தற்போது) வகை அமைப்பு" என்று கூறி தொடங்கி, "இந்த நேரத்தில் நான் மேலே சொன்னவற்றில் பெரும்பாலானவை யூகங்களின் மட்டத்தில் உள்ளன" என்று முடிவடைந்தது. ஹோமோடாபி பிரிவில் டி. எஸ் மாதிரியின் வரையறை கூட அற்பமானது அல்ல, இது 2009 வரை தீர்க்கப்படாத சிக்கலான ஒத்திசைவு சிக்கல்களைக் குறிக்கிறது. இந்த குறிப்பு "சமத்துவ வகைகளின்" ஒரு சொற்பொருள் வரையறையை உள்ளடக்கியது, அவை மாதிரியில் பாதை-இடைவெளிகள் மூலம் விளக்கப்பட்டதாகக் கூறப்பட்டன, ஆனால் அடையாள வகைகளுக்கான பெர் மார்ட்டின்-லோஃப்பின் விதிகளை கருத்தில் கொள்ளவில்லை. இது அளவுடன் கூடுதலாக ஒரே மாதிரியான பரிமாணத்தால் பிரபஞ்சங்களை அடுக்குப்படுத்தியது, இது பின்னர் பெரும்பாலும் நிராகரிக்கப்பட்டது. சொற்பொருள் பக்கத்தில், பென்னோ வான் டென் பெர்க் 2006 ஆம் ஆண்டில் தீவிர வகை கோட்பாட்டில் ஒரு வகையின் அடையாள வகைகளின் கோபுரம் ஒரு ω-வகையின் கட்டமைப்பைக் கொண்டிருக்க வேண்டும் என்றும், உண்மையில் மைக்கேல் படானின் "உலகளாவிய, இயற்கணித" அர்த்தத்தில் ஒரு ω-குழுவாக இருக்க வேண்டும் என்றும் ஊகித்தார். இது பின்னர் வான் டென் பெர்க் மற்றும் கார்னர் ஆகியோரால் "வகைகள் பலவீனமான ஒமேகா-குழுக்கள்" (2008 இல் வெளியிடப்பட்டது) என்ற கட்டுரையிலும், பீட்டர் லும்ஸ்டைன் என்பவரால் "தீவிர வகை கோட்பாட்டிலிருந்து பலவீனமான ω-பிரிவுகள்" (2009 இல் வெளியிடப்பட்டது) மற்றும் அவரது 2010 பி. எச். டி ஆய்வறிக்கையின் ஒரு பகுதியாக "வகை கோட்பாடுகளிலிருந்து உயர் பிரிவுகள்" என்ற கட்டுரையிலும் சுயாதீனமாக நிரூபிக்கப்பட்டது. ஒற்றுமை கோட்பாடு, செயற்கை ஹோமோடாபி கோட்பாடு மற்றும் உயர் தூண்டல் வகைகள் ஒரு சமநிலையற்ற இழையின் கருத்து 2006 ஆம் ஆண்டின் தொடக்கத்தில் வோவோட்ஸ்கியால் அறிமுகப்படுத்தப்பட்டது. இருப்பினும், மார்ட்டின்-லோஃப் வகை கோட்பாட்டின் அனைத்து விளக்கக்காட்சிகளின் வலியுறுத்தலின் காரணமாக, அடையாள வகைகள், வெற்று சூழலில், பிரதிபலிப்பை மட்டுமே கொண்டிருக்கலாம், வோவோட்ஸ்கி 2009 வரை இந்த அடையாள வகைகளை சமநிலையற்ற பிரபஞ்சங்களுடன் இணைந்து பயன்படுத்த முடியும் என்பதை அங்கீகரிக்கவில்லை. குறிப்பாக, தற்போதுள்ள மார்ட்டின்-லோஃப் வகை கோட்பாட்டிற்கு ஒரு கோட்பாட்டைச் சேர்ப்பதன் மூலம் ஒற்றுமையை அறிமுகப்படுத்த முடியும் என்ற கருத்து 2009 இல் மட்டுமே தோன்றியது. 2009 ஆம் ஆண்டில், வோவோட்ஸ்கி கான் வளாகங்களில் வகைக் கோட்பாட்டின் மாதிரியின் கூடுதல் விவரங்களை உருவாக்கினார், மேலும் வகைக் கோட்பாட்டின் வகைப்படுத்தப்பட்ட மாதிரிகளுக்கான ஒத்திசைவு சிக்கல்களைத் தீர்க்க ஒரு உலகளாவிய கான் இழையின் இருப்பைப் பயன்படுத்தலாம் என்பதைக் கவனித்தார். ஏ. கே. பவுஸ்ஃபீல்டின் ஒரு கருத்தைப் பயன்படுத்தி, இந்த உலகளாவிய ஃபைப்ரேஷன் சமநிலையற்றது என்பதை அவர் நிரூபித்தார்ஃ இழைகளுக்கு இடையிலான ஜோடி வாரியான ஹோமோடோபி சமநிலைகளின் தொடர்புடைய ஃபைப்ரேஷன் அடித்தளத்தின் பாதைகள்-விண்வெளி ஃபைப்ரேஷனுக்கு சமம். "f என்பது ஒரு சமநிலை" என்ற கூற்றைக் குறிக்கும் வகை (செயல்பாட்டு விரிவாக்கத்தின் அனுமானத்தின் கீழ்) (-1)-சிதைக்கப்பட்டது (அதாவது. குடியிருப்பு இருந்தால் ஒப்பந்தமாகும்). இது ஹாஃப்மேன் மற்றும் ஸ்ட்ரீச்சரின் "பிரபஞ்ச விரிவாக்கத்தை" உயர்ந்த பரிமாணங்களுக்கு பொதுமைப்படுத்தி, ஒற்றுமையின் ஒரு சொற்பொருள் அறிக்கையை வழங்க அவருக்கு உதவியது. ஆதார உதவியாளர் Coq இல் குறிப்பிடத்தக்க அளவு "செயற்கை ஹோமோடாபி கோட்பாட்டை" உருவாக்கத் தொடங்குவதற்கு சமன்பாடுகள் மற்றும் ஒப்பந்தத்தன்மை பற்றிய இந்த வரையறைகளைப் பயன்படுத்தவும் அவரால் முடிந்தது; இது பின்னர் "அடித்தளங்கள்" மற்றும் இறுதியில் "யூனிமாத்" என்று அழைக்கப்படும் நூலகத்தின் அடிப்படையை உருவாக்கியது. பல்வேறு நூல்களின் ஒருங்கிணைப்பு பிப்ரவரி 2010 இல் கார்னகி மெலன் பல்கலைக்கழகத்தில் ஒரு முறைசாரா சந்திப்புடன் தொடங்கியது, அங்கு வோவோட்ஸ்கி கான் வளாகங்களில் தனது மாதிரியையும், அவோடி, வாரன், லுஂஸ்டைன், ராபர்ட் ஹார்பர், டான் லிகாட்டா, மைக்கேல் ஷுல்மேன் மற்றும் பலர் அடங்கிய குழுவுக்கு தனது கோக் குறியீட்டையும் வழங்கினார். இந்த கூட்டம் (வாரன், லும்ஸ்டைன், லிகாட்டா மற்றும் ஷுல்மேன் ஆகியோரால்) ஒவ்வொரு ஹோமோடாபி சமநிலையும் ஒரு சமநிலை (வோவோட்ஸ்கியின் நல்ல ஒத்திசைவான அர்த்தத்தில்) என்பதற்கான ஆதாரத்தின் வெளிப்பாடுகளை உருவாக்கியது, இது சமன்பாடுகளை மேம்படுத்துவதற்கான வகைக் கோட்பாட்டின் கருத்தை அடிப்படையாகக் கொண்டது. விரைவில், வோவோட்ஸ்கி ஒற்றுமை கோட்பாடு செயல்பாட்டு விரிவாக்கத்தை குறிக்கிறது என்பதை நிரூபித்தார். அடுத்த முக்கிய நிகழ்வு மார்ச் 2011 இல் ஓபர்வோல்ஃபாக்கின் கணித ஆராய்ச்சி நிறுவனத்தில் ஸ்டீவ் அவோடி, ரிச்சர்ட் கார்னர், பெர் மார்ட்டின்-லோஃப் மற்றும் விளாடிமிர் வோவோட்ஸ்கி ஆகியோரால் ஏற்பாடு செய்யப்பட்ட ஒரு சிறிய பணிமனை ஆகும், இது "ஆக்கபூர்வமான வகை கோட்பாட்டின் ஓரினச்சேர்க்கை விளக்கம்" என்ற தலைப்பில் இருந்தது. இந்த பட்டறைக்கான கோக் பயிற்சியின் ஒரு பகுதியாக, ஆண்ட்ரேஜ் பாயர் வோவோட்ஸ்கியின் யோசனைகளை அடிப்படையாகக் கொண்டு ஒரு சிறிய கோக் நூலகத்தை எழுதினார் (ஆனால் உண்மையில் அவரது குறியீடு எதையும் பயன்படுத்தவில்லை); இது இறுதியில் "ஹோட்" கோக் நூலகத்தின் முதல் பதிப்பின் கர்னலாக மாறியது (மைக்கேல் ஷுல்மேனின் பிந்தையவரின் முதல் கமிட் "ஆண்ட்ரேஜ் பாயரின் கோப்புகளை அடிப்படையாகக் கொண்ட மேம்பாடு, விளாடிமிர் வோவோட்ஸ்கியின் கோப்புகளிலிருந்து எடுக்கப்பட்ட பல யோசனைகளுடன்"). லும்ஸ்டைன், ஷுல்மேன், பாயர் மற்றும் வாரன் காரணமாக ஓபர்வோல்ஃபாக் கூட்டத்திலிருந்து வெளிவரும் மிக முக்கியமான விஷயங்களில் ஒன்று உயர் தூண்டல் வகைகளின் அடிப்படை யோசனையாகும். பங்கேற்பாளர்கள் முக்கியமான திறந்த கேள்விகளின் பட்டியலையும் உருவாக்கினர், அதாவது ஒற்றுமை கோட்பாடு நம்பகத்தன்மையை திருப்திப்படுத்துகிறதா (இன்னும் திறந்திருந்தாலும், சில சிறப்பு வழக்குகள் நேர்மறையாக தீர்க்கப்பட்டிருந்தாலும்), ஒற்றுமை கோட்பாட்டில் தரமற்ற மாதிரிகள் உள்ளதா (ஷுல்மேனால் நேர்மறையாக பதிலளிக்கப்பட்டதிலிருந்து), மற்றும் (அரை) எளிமையான வகைகளை எவ்வாறு வரையறுப்பது (இன்னும் எம். எல். டி. டி. யில் திறந்திருந்தாலும், இது வோவோட்ஸ்கியின் ஹோமோடோபி வகை அமைப்பில் (எச். டி. எஸ்) செய்யப்படலாம், இது இரண்டு சமத்துவ வகைகளைக் கொண்ட ஒரு வகை கோட்பாடு). ஓபர்வோல்ஃபாக் பட்டறைக்குப் பிறகு, ஹோமோடோபி வகை கோட்பாடு வலைத்தளம் மற்றும் வலைப்பதிவு நிறுவப்பட்டது, மேலும் இந்த பொருள் அந்த பெயரில் பிரபலமடையத் தொடங்கியது. இந்த காலகட்டத்தில் சில முக்கியமான முன்னேற்றங்களைப் பற்றிய ஒரு யோசனையை வலைப்பதிவு வரலாற்றிலிருந்து பெறலாம். சமமற்ற அடித்தளங்கள் "சமமற்ற அடித்தளங்கள்" என்ற சொற்றொடர் ஹோமோடாபி வகை கோட்பாட்டுடன் நெருக்கமாக தொடர்புடையது என்று அனைவரும் ஒப்புக்கொள்கிறார்கள், ஆனால் எல்லோரும் அதை ஒரே மாதிரியாகப் பயன்படுத்துவதில்லை. இது முதலில் விளாடிமிர் வோவோட்ஸ்கியால் கணிதத்திற்கான ஒரு அடித்தள அமைப்பைப் பற்றிய அவரது பார்வையைக் குறிக்கப் பயன்படுத்தப்பட்டது, இதில் அடிப்படை பொருள்கள் ஒரே மாதிரியான வகைகளாகும், இது ஒரு வகை கோட்பாட்டின் அடிப்படையில் § ஒற்றுமை கோட்பாட்டை திருப்திப்படுத்துகிறது, மேலும் கணினி ஆதார உதவியாளராக முறைப்படுத்தப்படுகிறது. வோவோட்ஸ்கியின் பணி ஹோமோடாபி வகைக் கோட்பாட்டில் பணிபுரியும் பிற ஆராய்ச்சியாளர்களின் சமூகத்துடன் ஒருங்கிணைக்கப்படுவதால், "சமநிலையற்ற அடித்தளங்கள்" சில நேரங்களில் "ஹோமோடாபி வகைக் கோட்பாட்டுடன்" ஒன்றுக்கொன்று மாற்றாகப் பயன்படுத்தப்பட்டன, மற்ற நேரங்களில் அதன் பயன்பாட்டை ஒரு அடித்தள அமைப்பாக மட்டுமே குறிப்பிடுகின்றன (எடுத்துக்காட்டாக, மாதிரி-வகைப்பாட்டு சொற்பொருள் அல்லது கணக்கீட்டு மெட்டாதியரி ஆய்வு தவிர). உதாரணமாக, ஐஏஎஸ் சிறப்பு ஆண்டின் பொருள் அதிகாரப்பூர்வமாக "சமநிலையற்ற அடித்தளங்கள்" என்று வழங்கப்பட்டது, இருப்பினும் அங்கு செய்யப்பட்ட பல வேலைகள் அடித்தளங்களுடன் கூடுதலாக சொற்பொருள் மற்றும் மெட்டாதியரியில் கவனம் செலுத்தின. ஐ. ஏ. எஸ் திட்டத்தில் பங்கேற்பாளர்களால் தயாரிக்கப்பட்ட புத்தகத்தின் தலைப்பு "ஹோமோடோபி வகை கோட்பாடுஃ கணிதத்தின் தனித்துவமான அடித்தளங்கள்"; இது பயன்பாட்டைக் குறிக்கலாம் என்றாலும், புத்தகம் HOTT ஐ ஒரு கணித அடித்தளமாக மட்டுமே விவாதிக்கிறது. கணிதத்தின் சமமற்ற அடித்தளங்கள் குறித்த சிறப்பு ஆண்டு 2012-13 மேம்பட்ட ஆய்வு நிறுவனத்தின் ஆராய்ச்சியாளர்கள் "கணிதத்தின் சமமற்ற அடித்தளங்கள் குறித்த ஒரு சிறப்பு ஆண்டு" நடத்தினர். இந்த சிறப்பு ஆண்டு இடவியல், கணினி அறிவியல், வகைக் கோட்பாடு மற்றும் கணித தர்க்கம் ஆகியவற்றில் ஆராய்ச்சியாளர்களை ஒன்றிணைத்தது. இந்த நிகழ்ச்சியை ஸ்டீவ் அவோடி, தியரி கோகுவாண்ட் மற்றும் விளாடிமிர் வோவோட்ஸ்கி ஆகியோர் ஏற்பாடு செய்தனர். நிகழ்ச்சியின் போது, பங்கேற்பாளர்களில் ஒருவரான பீட்டர் அக்ஸெல், ஒரு பணிக்குழுவைத் தொடங்கினார், இது வகைக் கோட்பாட்டை முறைசாரா முறையில் ஆனால் கடுமையாக எவ்வாறு செய்வது என்பதை ஆராய்ந்தது, இது செட் கோட்பாட்டைச் செய்யும் சாதாரண கணிதவியலாளர்களுக்கு ஒத்த பாணியில் உள்ளது. ஆரம்ப சோதனைகளுக்குப் பிறகு, இது சாத்தியம் மட்டுமல்ல, மிகவும் பயனுள்ளதாகவும், ஒரு புத்தகத்தை (ஹோட் புத்தகம் என்று அழைக்கப்படுபவை) எழுத முடியும், எழுதப்பட வேண்டும் என்பதும் தெளிவாகியது. திட்டத்தின் பல பங்கேற்பாளர்கள் தொழில்நுட்ப ஆதரவு, எழுதுதல், ஆதார வாசிப்பு மற்றும் யோசனைகளை வழங்குவதன் மூலம் இந்த முயற்சியில் இணைந்தனர். ஒரு கணித உரைக்கு வழக்கத்திற்கு மாறாக, இது ஒத்துழைப்புடன் உருவாக்கப்பட்டது மற்றும் கிட்ஹப்பில் திறந்த நிலையில், கிரியேட்டிவ் காமன்ஸ் உரிமத்தின் கீழ் வெளியிடப்பட்டது, இது மக்கள் தங்கள் புத்தகத்தின் சொந்த பதிப்பை முடக்க அனுமதிக்கிறது, மேலும் இது அச்சில் வாங்கக்கூடியது மற்றும் இலவசமாக பதிவிறக்கம் செய்யக்கூடியது. மேலும் பொதுவாக, சிறப்பு ஆண்டு முழு பாடத்தின் வளர்ச்சிக்கு ஒரு ஊக்கியாக இருந்தது; HOTT புத்தகம் ஒன்று மட்டுமே, மிகவும் புலப்படும், விளைவாக இருந்தது. சிறப்பு ஆண்டில் அதிகாரப்பூர்வ பங்கேற்பாளர்கள் பீட்டர் அக்ஸெல் பெனடிக்ட் அஹ்ரென்ஸ் தோர்ஸ்டன் ஆல்டென்கிர்ச் ஸ்டீவ் அவோடி புருனோ பாராஸ் ஆண்ட்ரேஜ் பாயர் யவ்ஸ் பெர்டோட் மார்க் பெசெம் தியரி கோக்வாண்ட் எரிக் ஃபின்ஸ்டர் டேனியல் கிரேசன் ஹ்யூகோ ஹெர்பெலின் ஆண்ட்ரே ஜோயல் டான் லிகாட்டா பீட்டர் லும்ஸ்டைன் ஆசியா மஹ்பூபி பெர் மார்ட்டின்-லோஃப் செர்ஜி மெலிக்கோவ் அல்வாரோ பெலாயோ ஆண்ட்ரூ பொலோன்ஸ்கி மைக்கேல் ஷுல்மேன் மத்தியூ சோஸோ பாஸிட்டர்ஸ் பென்னோ வான் டென் விளாடிமிர் வோவோட்ஸ்கி மைக்கேல் வாரன் நோம் சைல்பெர்கர் ஏசிஎம் கம்ப்யூட்டிங் விமர்சனங்கள் இந்த புத்தகத்தை "கம்ப்யூட்டிங் கணிதம்" என்ற பிரிவில் குறிப்பிடத்தக்க 2013 வெளியீடாக பட்டியலிட்டன. முக்கிய கருத்துக்கள் "வகைகளாக முன்மொழிவுகள்" HOTT வகைக் கோட்பாட்டின் "வகைகளாக முன்மொழிவுகள்" விளக்கத்தின் மாற்றியமைக்கப்பட்ட பதிப்பைப் பயன்படுத்துகிறது, அதன்படி வகைகள் முன்மொழிவுகளையும் பிரதிநிதித்துவப்படுத்தலாம் மற்றும் சொற்கள் பின்னர் ஆதாரங்களைக் குறிக்கலாம். எவ்வாறாயினும், HOTT இல், நிலையான "வகைகளாக முன்மொழிவுகள்" போலல்லாமல், ஒரு சிறப்பு பாத்திரம் 'வெறும் முன்மொழிவுகளால்' விளையாடப்படுகிறது, இது தோராயமாக பேசுகையில், அந்த வகைகள் அதிகபட்சம் ஒரு சொல்லைக் கொண்டுள்ளன, முன்மொழிவு சமத்துவம் வரை. இவை பொதுவான வகைகளை விட வழக்கமான தர்க்கரீதியான முன்மொழிவுகளைப் போன்றவை, அவை ஆதாரம்-பொருத்தமற்றவை. சமத்துவம் ஹோமோடாபி வகை கோட்பாட்டின் அடிப்படை கருத்து பாதை. HOTT இல், வகை என்பது புள்ளியில் இருந்து புள்ளி வரை அனைத்து பாதைகளின் வகையாகும். (எனவே, ஒரு புள்ளி ஒரு புள்ளிக்கு சமம் என்பதற்கான சான்று புள்ளியில் இருந்து புள்ளிக்கு செல்லும் பாதைக்கு சமம்.) எந்தவொரு புள்ளிக்கும், சமத்துவத்தின் பிரதிபலிப்பு பண்புடன் தொடர்புடைய ஒரு வகை பாதை உள்ளது. ஒரு வகை பாதையை தலைகீழாக மாற்றலாம், இது சமத்துவத்தின் சமச்சீர் பண்புடன் தொடர்புடைய வகையின் பாதையை உருவாக்குகிறது. ரெஸ்ப் வகையின் இரண்டு பாதைகள். இணைக்கப்படலாம், இது ஒரு வகை பாதையை உருவாக்குகிறது; இது சமத்துவத்தின் இடைநிலை பண்புக்கு ஒத்திருக்கிறது. மிக முக்கியமாக, ஒரு பாதை மற்றும் சில சொத்தின் ஆதாரம் கொடுக்கப்பட்டால், சொத்தின் ஆதாரத்தை வழங்குவதற்காக ஆதாரத்தை பாதையில் "கொண்டு செல்ல" முடியும். (சமமாக கூறப்பட்டால், ஒரு வகை பொருளை ஒரு வகை பொருளாக மாற்றலாம்.) இது சமத்துவத்தின் மாற்றுச் சொத்துடன் ஒத்திருக்கிறது. இங்கே, எச்ஓடிடி மற்றும் கிளாசிக்கல் கணிதத்திற்கு இடையிலான ஒரு முக்கியமான வேறுபாடு வருகிறது. கிளாசிக்கல் கணிதத்தில், இரண்டு மதிப்புகளின் சமத்துவம் நிறுவப்பட்டதும், அதன்பிறகு அவற்றுக்கிடையே எந்த வேறுபாட்டையும் பொருட்படுத்தாமல் ஒன்றுக்கொன்று மாற்றாகப் பயன்படுத்தப்படலாம். இருப்பினும், ஹோமோடாபி வகை கோட்பாட்டில், பல வெவ்வேறு பாதைகள் இருக்கலாம், மேலும் ஒரு பொருளை இரண்டு வெவ்வேறு பாதைகளில் கொண்டு செல்வது இரண்டு வெவ்வேறு முடிவுகளைத் தரும். எனவே, ஹோமோடாபி வகை கோட்பாட்டில், மாற்று பண்பைப் பயன்படுத்தும்போது, எந்த பாதை பயன்படுத்தப்படுகிறது என்பதைக் குறிப்பிடுவது அவசியம். பொதுவாக, ஒரு "முன்மொழிவு" பல வேறுபட்ட ஆதாரங்களைக் கொண்டிருக்கலாம். (எடுத்துக்காட்டாக, அனைத்து இயல் எண்களின் வகையும், ஒரு முன்மொழிவாகக் கருதப்படும்போது, ஒவ்வொரு இயல் எண்ணையும் ஆதாரமாகக் கொண்டுள்ளது.) ஒரு முன்மொழிவுக்கு ஒரே ஒரு ஆதாரம் இருந்தாலும், பாதைகளின் இடைவெளி ஏதோ ஒரு வகையில் அற்பமானதாக இருக்காது. ஒரு "வெறும் முன்மொழிவு" என்பது காலியாக இருக்கும் அல்லது ஒரு அற்பமான பாதை இடத்துடன் ஒரே ஒரு புள்ளியைக் கொண்டிருக்கும் எந்த வகையும் ஆகும். மக்கள் எழுதுகிறார்கள் என்பதை நினைவில் கொள்க, இதன் மூலம் மறைமுகமான வகையை விட்டு விடுகிறார்கள். அடையாள செயல்பாட்டைக் குறிக்கும் வகையில் இதைக் குழப்ப வேண்டாம். வகை சமநிலை இரண்டு வகைகள் மற்றும் சில பிரபஞ்சத்தைச் சேர்ந்தவை அவற்றுக்கிடையே ஒரு சமநிலை இருந்தால் சமமானவை என்று வரையறுக்கப்படுகின்றன. ஒரு சமநிலை என்பது இடது தலைகீழ் மற்றும் வலது தலைகீழ் இரண்டையும் கொண்ட ஒரு செயல்பாடாகும், அதாவது பொருத்தமாக தேர்ந்தெடுக்கப்பட்ட மற்றும் பின்வரும் வகைகள் இரண்டும் வசிக்கின்றனஃ அதாவது. இது சமத்துவ வகைகளைப் பயன்படுத்தி "இடது தலைகீழ் மற்றும் வலது தலைகீழ் இரண்டையும் கொண்டுள்ளது" என்ற பொதுவான கருத்தை வெளிப்படுத்துகிறது. மேலே உள்ள தலைகீழ் நிபந்தனைகள் செயல்பாட்டு வகைகள் மற்றும் சமத்துவ வகைகளாகும் என்பதை நினைவில் கொள்க. ஒன்று பொதுவாக செயல்பாட்டு விரிவாக்க கோட்பாட்டைக் கருதுகிறது, இது களம் மற்றும் கோடமைனில் உள்ள சமத்துவத்தைப் பயன்படுத்தி தலைகீழாக வெளிப்படுத்தும் பின்வரும் வகைகளுக்கு சமமானது என்பதை உறுதி செய்கிறது மற்றும்ஃ அதாவது. அனைத்திற்கும் மற்றும், வகையின் செயல்பாடுகள் அவை சமநிலைகள் என்பதற்கான சான்றுடன் சேர்ந்து குறிக்கப்படுகின்றன. ஒற்றுமை கோட்பாடு மேலே உள்ளபடி சமன்பாடுகளாக வரையறுக்கப்பட்ட செயல்பாடுகளைக் கொண்டிருப்பதால், சமன்பாடுகளுக்கு பாதைகளைத் திருப்ப ஒரு நியதி வழி உள்ளது என்பதை ஒருவர் காட்ட முடியும். வேறு வார்த்தைகளில் கூறுவதானால், வகையின் ஒரு செயல்பாடு உள்ளது, இது சமமான வகைகள், குறிப்பாக, சமமானவை என்பதை வெளிப்படுத்துகிறது. ஒற்றுமை கோட்பாடு இந்த செயல்பாடு ஒரு சமநிலை என்று கூறுகிறது. எனவே, நம்மிடம் "வேறு வார்த்தைகளில் கூறுவதானால், அடையாளம் என்பது சமநிலைக்கு சமம். குறிப்பாக, 'சமமான வகைகள் ஒரே மாதிரியானவை' என்று ஒருவர் கூறலாம். மார்ட்டின் ஹோட்ஸெல் எஸ்கார்டோ, ஒற்றுமையின் பண்பு மார்ட்டின்-லோஃப் வகை கோட்பாட்டிலிருந்து (எம். எல். டி. டி) சுயாதீனமாக உள்ளது என்பதைக் காட்டியுள்ளார். கணினி ஆதார உதவியாளர்களுக்கான கணித சான்றுகளை கணினி நிரலாக்க மொழியில் மொழிபெயர்க்க HOTT அனுமதிக்கிறது என்று வழக்குரைஞர்களை நிரூபிக்கும் பயன்பாடுகள் தேற்றம் கூறுகிறது. இந்த அணுகுமுறை கடினமான ஆதாரங்களை கணினிகள் சரிபார்க்கும் திறனை அதிகரிக்கிறது என்று அவர்கள் வாதிடுகின்றனர். இருப்பினும், இந்த கூற்றுக்கள் உலகளவில் ஏற்றுக்கொள்ளப்படவில்லை மற்றும் பல ஆராய்ச்சி முயற்சிகள் மற்றும் ஆதார உதவியாளர்கள் ஹோட்டைப் பயன்படுத்துவதில்லை. லாஜிக்கல்-கணித முன்மொழிவுகளின் சமத்துவத்தை ஹோமோடாபி கோட்பாட்டுடன் தொடர்புபடுத்தும் ஒற்றுமை கோட்பாட்டை ஹோட் ஏற்றுக்கொள்கிறது. "a = b" போன்ற சமன்பாடு என்பது இரண்டு வெவ்வேறு குறியீடுகள் ஒரே மதிப்பைக் கொண்ட ஒரு கணித முன்மொழிவு ஆகும். ஹோமோடாபி வகை கோட்பாட்டில், குறியீடுகளின் மதிப்புகளைக் குறிக்கும் இரண்டு வடிவங்களும் இடவியல் ரீதியாக சமமானவை என்று அர்த்தம். இந்த சமநிலை உறவுகள், கோட்பாட்டு ஆய்வுகளுக்கான ETH ஜூரிச் இன்ஸ்டிடியூட் இயக்குனர் ஜியோவானி ஃபெல்டெர் வாதிடுகிறார், ஹோமோடாபி கோட்பாட்டில் சிறப்பாக வடிவமைக்கப்படலாம், ஏனெனில் இது மிகவும் விரிவானதுஃ ஹோமோடோபி கோட்பாடு ஏன் "a சமம் b" என்பதை மட்டுமல்ல, இதை எவ்வாறு பெறுவது என்பதையும் விளக்குகிறது. தொகுப்புக் கோட்பாட்டில், இந்தத் தகவல் கூடுதலாக வரையறுக்கப்பட வேண்டும், இது, வக்கீல்கள் வாதிடுகிறார்கள், கணித முன்மொழிவுகளை நிரலாக்க மொழிகளில் மொழிபெயர்ப்பது மிகவும் கடினம். கணினி நிரலாக்கம் 2015 ஆம் ஆண்டு நிலவரப்படி, ஹோமோடாபி வகை கோட்பாட்டில் ஒற்றுமை கோட்பாட்டின் கணக்கீட்டு நடத்தையை மாதிரியாக்கவும் முறையாக பகுப்பாய்வு செய்யவும் தீவிர ஆராய்ச்சி பணிகள் நடந்து கொண்டிருந்தன. கியூபிகல் வகை கோட்பாடு என்பது ஹோமோடாபி வகை கோட்பாட்டிற்கு கணக்கீட்டு உள்ளடக்கத்தை வழங்குவதற்கான ஒரு முயற்சியாகும். இருப்பினும், அரை-எளிமையான வகைகள் போன்ற சில பொருட்களை துல்லியமான சமத்துவம் பற்றிய சில கருத்துக்களைக் குறிப்பிடாமல் கட்டமைக்க முடியாது என்று நம்பப்படுகிறது. எனவே, பல்வேறு இரண்டு நிலை வகை கோட்பாடுகள் உருவாக்கப்பட்டுள்ளன, அவை அவற்றின் வகைகளை நார் வகைகளாகப் பிரிக்கின்றன, அவை பாதைகளை மதிக்கின்றன, மற்றும் நார் அல்லாத வகைகள், அவை இல்லை. கார்ட்டீசியன் கியூபிகல் கம்ப்யூடேஷனல் வகை கோட்பாடு என்பது முதல் இரண்டு நிலை வகை கோட்பாடாகும், இது ஹோமோடாபி வகை கோட்பாட்டிற்கு முழு கணக்கீட்டு விளக்கத்தை வழங்குகிறது. மேலும் காண்க கட்டுமானங்களின் கால்குலஸ் கறி-ஹோவர்ட் கடிதப் புலனுணர்வு வகைக் கோட்பாடு ஹோமோடோபி கருதுகோள் யூனிவலன்ட் ஃபவுண்டேஷன்ஸ் குறிப்புகள் குறிப்புகள் நூலியல் (இந்த கட்டுரையில் மேற்கோள் காட்டப்பட்ட கிட்ஹப் பதிப்பு). PDF ஆக இருக்கும். போஸ்ட்ஸ்கிரிப்ட் போல. டேவிட் கார்ஃபீல்ட் (2020), மாடல் ஹோமோடோபி வகை கோட்பாடுஃ தத்துவத்திற்கான புதிய தர்க்கத்தின் வாய்ப்பு, ஆக்ஸ்போர்டு யுனிவர்சிட்டி பிரஸ். எக்பர்ட் ரிஜ்கே (2022), ஹோமோடோபி வகை கோட்பாட்டின் அறிமுகம்,. அறிமுக பாடப்புத்தகம். வெளிப்புற இணைப்புகள் விக்கி விளாடிமிர் வோவோட்ஸ்கியின் வலைப்பக்கத்தில் ஸ்டீவ் அவோடியின் சமத்துவமற்ற அடித்தளங்கள் ஹோமோடோபி வகை கோட்பாடு மற்றும் கணிதத்தின் சமத்துவமற்ற அடித்தளங்கள் குறித்த வலைப்பக்கம் "ஆக்கபூர்வமான வகை கோட்பாடு மற்றும் ஹோமோடோபி"-முறைப்படுத்தப்பட்ட கணிதத்தின் மேம்பட்ட ஆய்வு நூலகங்களுக்கான நிறுவனத்தில் ஸ்டீவ் அவோடியின் வீடியோ சொற்பொழிவு (இப்போது யூனிமாத்தில் ஒருங்கிணைக்கப்பட்டுள்ளது, அங்கு மேலும் வளர்ச்சி நடைபெறுகிறது) கணித வகை கோட்பாட்டின் அடித்தளங்கள் ஹோமோடோபி கோட்பாடு முறையான முறைகள் வீடியோ கிளிப்களைக் கொண்ட கட்டுரைகள்