Homotopy type theory
ગાણિતિક તર્કશાસ્ત્ર અને કોમ્પ્યુટર વિજ્ઞાનમાં, હોમોટૉપી પ્રકાર સિદ્ધાંત (એચઓટીટી) એ અંતર્જ્ઞાનવાદી પ્રકાર સિદ્ધાંતના વિકાસની વિવિધ રેખાઓનો ઉલ્લેખ કરે છે, જે પદાર્થો તરીકે પ્રકારોના અર્થઘટન પર આધારિત છે, જેના પર (અમૂર્ત) હોમોટૉપી સિદ્ધાંતનો અંતર્જ્ઞાન લાગુ થાય છે. આમાં, કાર્યની અન્ય રેખાઓ વચ્ચે, આવા પ્રકારનાં સિદ્ધાંતો માટે સમસ્થાનિક અને ઉચ્ચ-શ્રેણીના નમૂનાઓનું નિર્માણ; અમૂર્ત સમસ્થાનિક સિદ્ધાંત અને ઉચ્ચ શ્રેણી સિદ્ધાંત માટે તર્ક (અથવા આંતરિક ભાષા) તરીકે પ્રકાર સિદ્ધાંતનો ઉપયોગ; પ્રકાર-સૈદ્ધાંતિક પાયામાં ગણિતનો વિકાસ (અગાઉ અસ્તિત્વમાં રહેલા ગણિત અને નવા ગણિત કે જે સમસ્થાનિક પ્રકારો શક્ય બનાવે છે તે બંને સહિત); અને કમ્પ્યુટર પ્રૂફ સહાયકોમાં આમાંના દરેકનું ઔપચારિકરણ સામેલ છે. હોમોટૉપી પ્રકાર સિદ્ધાંત તરીકે ઓળખાતા કાર્ય અને અવિભાજ્ય પાયો પ્રોજેક્ટ વચ્ચે એક મોટો ઓવરલેપ છે. જો કે બંનેમાંથી કોઈનું ચોક્કસ વર્ણન કરવામાં આવ્યું નથી, અને શબ્દોનો ઉપયોગ કેટલીકવાર એકબીજાના બદલે કરવામાં આવે છે, ઉપયોગની પસંદગી પણ કેટલીકવાર દૃષ્ટિકોણ અને ભારમાં તફાવતોને અનુરૂપ હોય છે. જેમ કે, આ લેખ આ ક્ષેત્રના તમામ સંશોધકોના મંતવ્યોને સમાન રીતે રજૂ કરી શકશે નહીં. જ્યારે ક્ષેત્ર ઝડપી પ્રવાહમાં હોય ત્યારે આ પ્રકારની પરિવર્તનશીલતા અનિવાર્ય હોય છે. ઇતિહાસ ગ્રુપોઇડ મોડેલ એક સમયે આ વિચાર કે સઘન પ્રકાર સિદ્ધાંતમાં તેમના ઓળખ પ્રકારો સાથે પ્રકારોને ગ્રુપોઇડ્સ તરીકે ગણી શકાય તે ગાણિતિક લોકકથાઓ હતી. તે સૌપ્રથમ માર્ટિન હોફમેન અને થોમસ સ્ટ્રીચરના 1994 ના પેપરમાં અર્થપૂર્ણ રીતે ચોક્કસ બનાવવામાં આવ્યું હતું, જેને "ગ્રુપોઇડ મોડેલ ઓળખ સાબિતીની વિશિષ્ટતાને રદિયો આપે છે" કહેવાય છે, જેમાં તેઓએ દર્શાવ્યું હતું કે સઘન પ્રકાર સિદ્ધાંત ગ્રુપોઇડ્સની શ્રેણીમાં એક મોડેલ ધરાવે છે. આ પ્રકાર સિદ્ધાંતનું પ્રથમ સાચું "હોમોટોપિકલ" મોડેલ હતું, જોકે માત્ર "1-પરિમાણીય" (સમૂહોની શ્રેણીમાં પરંપરાગત મોડેલો હોમોટોપિકલ રીતે 0-પરિમાણીય છે). તેમના અનુવર્તી કાગળે હોમોટૉપી પ્રકાર સિદ્ધાંતમાં ઘણા પછીના વિકાસની આગાહી કરી. દાખલા તરીકે, તેઓએ નોંધ્યું હતું કે ગ્રૂપોઇડ મોડેલ એક નિયમને સંતોષે છે જેને તેઓ "બ્રહ્માંડ વિસ્તરણ" કહે છે, જે દસ વર્ષ પછી વ્લાદિમીર વોવોડસ્કીએ પ્રસ્તાવિત કરેલા 1-પ્રકારનાં સમાનતાના સ્વયંસિદ્ધ પર પ્રતિબંધ સિવાય બીજું કંઈ નથી. (1-પ્રકારો માટેનો સ્વયંસિદ્ધ સિદ્ધાંત ઘડવા માટે નોંધપાત્ર રીતે સરળ છે, જો કે, "સમાનતા" ની સુસંગત કલ્પનાની જરૂર નથી.) તેઓએ "સમરૂપતા સાથેની શ્રેણીઓને સમાનતા તરીકે" પણ વ્યાખ્યાયિત કરી અને અનુમાન લગાવ્યું કે ઉચ્ચ-પરિમાણીય ગ્રૂપોઇડ્સનો ઉપયોગ કરતા મોડેલમાં, આવી શ્રેણીઓ માટે "સમાનતા સમાનતા છે" હશે; આ પછીથી બેનેડિક્ટ અહ્રેન્સ, ક્રિઝિસ્તોફ કપુલ્કિન અને માઇકલ શુલમેન દ્વારા સાબિત કરવામાં આવ્યું હતું. પ્રારંભિક ઇતિહાસઃ નમૂનાની શ્રેણીઓ અને ઉચ્ચ જૂથો સઘન પ્રકાર સિદ્ધાંતના પ્રથમ ઉચ્ચ-પરિમાણીય નમૂનાઓનું નિર્માણ સ્ટીવ ઓવોડી અને તેમના વિદ્યાર્થી માઈકલ વોરેન દ્વારા 2005માં ક્વિલન નમૂનાની શ્રેણીઓનો ઉપયોગ કરીને કરવામાં આવ્યું હતું. આ પરિણામો સૌપ્રથમ એફ. એમ. સી. એસ. 2006 પરિષદમાં જાહેરમાં રજૂ કરવામાં આવ્યા હતા, જેમાં વોરેને "હોમોટોપી મોડલ્સ ઓફ ઇન્ટેન્સિઓનલ ટાઇપ થિયરી" શીર્ષક ધરાવતું પ્રવચન આપ્યું હતું, જે તેમના થીસીસ પ્રોસ્પેક્ટસ તરીકે પણ કામ કરતું હતું (શોધ નિબંધ સમિતિમાં એવોડે, નિકોલા ગેમ્બિનો અને એલેક્સ સિમ્પસન હાજર હતા). સારાંશ વોરેનના થીસીસ પ્રોસ્પેક્ટસ એબ્સ્ટ્રેક્ટમાં સમાયેલ છે. 2006 માં ઉપ્સાલા યુનિવર્સિટી ખાતે ઓળખના પ્રકારો વિશેની અનુગામી વર્કશોપમાં સઘન પ્રકાર સિદ્ધાંત અને ફેક્ટરાઇઝેશન સિસ્ટમ્સ વચ્ચેના સંબંધ વિશે બે ચર્ચાઓ થઈ હતીઃ એક રિચાર્ડ ગાર્નર દ્વારા, "પ્રકાર સિદ્ધાંત માટે ફેક્ટરાઇઝેશન સિસ્ટમ્સ", અને એક માઇકલ વોરેન દ્વારા, "મોડેલ કેટેગરીઝ અને સઘન ઓળખ પ્રકારો". સ્ટીવ ઓવોડી, "ઉચ્ચ-પરિમાણીય શ્રેણીઓનો પ્રકાર સિદ્ધાંત", અને થોમસ સ્ટ્રીચર, "ઓળખના પ્રકારો વિરુદ્ધ નબળા ઓમેગા-જૂથોઃ કેટલાક વિચારો, કેટલીક સમસ્યાઓ" દ્વારા વાતચીતમાં સંબંધિત વિચારોની ચર્ચા કરવામાં આવી હતી. તે જ પરિષદમાં બેન્નો વાન ડેન બર્ગે "નબળા ઒મેગા-વર્ગોના પ્રકારો" શીર્ષક ધરાવતું પ્રવચન આપ્યું હતું, જેમાં તેમણે એવા વિચારોની રૂપરેખા આપી હતી જે પાછળથી રિચાર્ડ ગાર્નર સાથે સંયુક્ત પેપરનો વિષય બન્યા હતા. ઉચ્ચ પરિમાણીય નમૂનાઓની તમામ પ્રારંભિક રચનાઓએ આશ્રિત પ્રકાર સિદ્ધાંતના નમૂનાઓની લાક્ષણિક સુસંગતતાની સમસ્યાનો સામનો કરવો પડ્યો હતો અને વિવિધ ઉકેલો વિકસાવવામાં આવ્યા હતા. આવો એક 2009માં વોવોડસ્કી દ્વારા, બીજો 2010માં વેન ડેન બર્ગ અને ગાર્નર દ્વારા આપવામાં આવ્યો હતો. વોવોડસ્કીના બાંધકામ પર આધારિત એક સામાન્ય ઉકેલ આખરે લુમ્સડેન અને વોરેન દ્વારા 2014માં આપવામાં આવ્યો હતો. 2007માં PSSL86 ખાતે ઓવોડીએ "હોમોટોપી પ્રકાર સિદ્ધાંત" શીર્ષક ધરાવતું પ્રવચન આપ્યું હતું (તે શબ્દનો આ પ્રથમ જાહેર ઉપયોગ હતો, જે ઓવોડે દ્વારા રચવામાં આવ્યો હતો). એવોડે અને વોરેને તેમના પરિણામોનો સારાંશ "ઓળખના પ્રકારોના હોમોટોપી સૈદ્ધાંતિક નમૂનાઓ" પેપરમાં આપ્યો હતો, જે 2007માં આર્ક્સિવ પ્રીપ્રિન્ટ સર્વર પર પોસ્ટ કરવામાં આવ્યો હતો અને 2009માં પ્રકાશિત થયો હતો; વધુ વિગતવાર સંસ્કરણ 2008માં વોરેનના થીસીસ "રચનાત્મક પ્રકાર સિદ્ધાંતના હોમોટોપી સૈદ્ધાંતિક પાસાઓ" માં દેખાયું હતું. લગભગ તે જ સમયે, વ્લાદિમીર વોવોડસ્કી ગણિતના વ્યવહારુ ઔપચારિકરણ માટે ભાષાની શોધના સંદર્ભમાં સ્વતંત્ર રીતે પ્રકાર સિદ્ધાંતની તપાસ કરી રહ્યા હતા. સપ્ટેમ્બર 2006માં તેમણે ટાઇપ્સ મેઇલિંગ લિસ્ટમાં "હોમોટૉપી લેમ્બડા કેલ્ક્યુલસ પર એક ખૂબ જ ટૂંકી નોંધ" પોસ્ટ કરી હતી, જેમાં આશ્રિત ઉત્પાદનો, સરવાળો અને બ્રહ્માંડ સાથે પ્રકાર સિદ્ધાંતની રૂપરેખા અને કાન સરળ સમૂહોમાં આ પ્રકારના સિદ્ધાંતના નમૂનાનું સ્કેચ કરવામાં આવ્યું હતું. તેની શરૂઆત "હોમોટૉપી λ-કેલ્ક્યુલસ એ એક કાલ્પનિક (આ ક્ષણે) પ્રકારની પ્રણાલી છે" એમ કહીને થઈ હતી અને તેનો અંત "આ ક્ષણે મેં ઉપર જે કહ્યું તેમાંથી મોટાભાગનું અનુમાનના સ્તરે છે. હોમોટૉપી શ્રેણીમાં ટી. એસ. ના મોડેલની વ્યાખ્યા પણ બિન-તુચ્છ છે, જે 2009 સુધી ઉકેલાયા ન હતા તેવા જટિલ સુસંગતતા મુદ્દાઓનો ઉલ્લેખ કરે છે. આ નોંધમાં "સમાનતાના પ્રકારો" ની વાક્યરચનાત્મક વ્યાખ્યાનો સમાવેશ થતો હતો, જેનો મોડલમાં પાથ-સ્પેસ દ્વારા અર્થઘટન કરવામાં આવ્યો હોવાનો દાવો કરવામાં આવ્યો હતો, પરંતુ ઓળખના પ્રકારો માટે પર માર્ટિન-લોફના નિયમોને ધ્યાનમાં લીધા નહોતા. તેણે બ્રહ્માંડને કદ ઉપરાંત હોમોટૉપી પરિમાણ દ્વારા પણ સ્તરીકૃત કર્યું હતું, જે વિચાર પાછળથી મોટાભાગે નકારી કાઢવામાં આવ્યો હતો. વાક્યરચના બાજુએ, બેન્નો વાન ડેન બર્ગે 2006 માં અનુમાન લગાવ્યું હતું કે સઘન પ્રકાર સિદ્ધાંતમાં એક પ્રકારનાં ઓળખ પ્રકારોના ટાવરમાં ω-શ્રેણીનું માળખું હોવું જોઈએ, અને ખરેખર ω-જૂથ હોવું જોઈએ, માઇકલ બેટનિનના "ગોળાકાર, બીજગણિત" અર્થમાં. આ પાછળથી વેન ડેન બર્ગ અને ગાર્નર દ્વારા પેપરમાં સ્વતંત્ર રીતે સાબિત કરવામાં આવ્યું હતું "પ્રકારો નબળા ઓમેગા-ગ્રૂપોઇડ્સ છે" (પ્રકાશિત 2008), અને પીટર લુમ્સડેન દ્વારા પેપરમાં "વીક ω-કેટેગરીઝ ફ્રોમ ઇન્ટેન્શનલ ટાઇપ થિયરી" (પ્રકાશિત 2009) અને તેમના 2010 પીએચ. ડી. થીસીસ "હાયર કેટેગરીઝ ફ્રોમ ટાઇપ થિયરીઝ" ના ભાગ રૂપે. અવિભાજ્ય સ્વયંસિદ્ધ, કૃત્રિમ હોમોટોપી સિદ્ધાંત અને ઉચ્ચ પ્રેરક પ્રકારો અવિભાજ્ય તંતુઓની વિભાવના 2006ની શરૂઆતમાં વોવોડસ્કી દ્વારા રજૂ કરવામાં આવી હતી. જો કે, માર્ટિન-લોફ પ્રકાર સિદ્ધાંતની તમામ પ્રસ્તુતિઓના આગ્રહને કારણે કે ઓળખના પ્રકારો, ખાલી સંદર્ભમાં, માત્ર પ્રતિબિંબીત હોઈ શકે છે, વોવોડસ્કીએ 2009 સુધી માન્યતા આપી ન હતી કે આ ઓળખના પ્રકારોનો ઉપયોગ અવિભાજ્ય બ્રહ્માંડ સાથે સંયોજનમાં થઈ શકે છે. ખાસ કરીને, વર્તમાન માર્ટિન-લોફ પ્રકાર સિદ્ધાંતમાં સ્વયંસિદ્ધ સૂત્ર ઉમેરીને સમાનતા રજૂ કરી શકાય તેવો વિચાર 2009 માં જ દેખાયો હતો. 2009માં પણ, વોવોડસ્કીએ કાન સંકુલમાં પ્રકાર સિદ્ધાંતના નમૂનાની વધુ વિગતો પર કામ કર્યું હતું અને અવલોકન કર્યું હતું કે સાર્વત્રિક કાન તંતુના અસ્તિત્વનો ઉપયોગ પ્રકાર સિદ્ધાંતના શ્રેણીબદ્ધ નમૂનાઓ માટે સુસંગતતા સમસ્યાઓને ઉકેલવા માટે થઈ શકે છે. તેમણે એ. કે. બોસફિલ્ડના વિચારનો ઉપયોગ કરીને એ પણ સાબિત કર્યું કે આ સાર્વત્રિક તંતુ અસમાન હતુંઃ તંતુઓ વચ્ચે જોડી મુજબની સમસ્થાનિક સમાનતાનું સંકળાયેલ તંતુ આધારના પાથ-સ્પેસ તંતુને સમકક્ષ છે. એક સ્વયંસિદ્ધ શબ્દ તરીકે એકરૂપતાને ઘડવા માટે વોવોડસ્કીએ વાક્યરચનામાં "સમાનતાઓ" ને વ્યાખ્યાયિત કરવાનો એક માર્ગ શોધી કાઢ્યો જેમાં મહત્વપૂર્ણ ગુણધર્મ હતો કે "f એક સમાનતા છે" નિવેદનનું પ્રતિનિધિત્વ કરતો પ્રકાર (કાર્ય વિસ્તરણની ધારણા હેઠળ) (-1)-સંકોચાયેલો હતો (એટલે કે. જો વસવાટ કરો છો તો કરારક્ષમ). આનાથી તેઓ હોફમેન અને સ્ટ્રીચરની "બ્રહ્માંડની વ્યાપકતા" ને ઉચ્ચ પરિમાણોમાં સામાન્ય બનાવતા એકરૂપતાનું વાક્યરચનાત્મક નિવેદન આપી શક્યા. તેઓ પ્રૂફ આસિસ્ટન્ટ કોકમાં નોંધપાત્ર માત્રામાં "સિન્થેટિક હોમોટૉપી થિયરી" વિકસાવવાનું શરૂ કરવા માટે સમાનતા અને સંકોચનક્ષમતાની આ વ્યાખ્યાઓનો ઉપયોગ કરવામાં પણ સક્ષમ હતા; આ પછીથી "ફાઉન્ડેશન્સ" અને આખરે "યુનિમેથ" તરીકે ઓળખાતા પુસ્તકાલયનો આધાર બન્યો. વિવિધ થ્રેડ્સનું એકીકરણ ફેબ્રુઆરી 2010માં કાર્નેગી મેલોન યુનિવર્સિટી ખાતે અનૌપચારિક બેઠક સાથે શરૂ થયું હતું, જ્યાં વોવોડ્સ્કીએ કાન સંકુલમાં તેમનું મોડેલ અને તેમનો કોક કોડ ઓવોડી, વોરેન, લુમ્સડેન, રોબર્ટ હાર્પર, ડેન લિકાટા, માઇકલ શુલમેન અને અન્ય સહિતના જૂથ સમક્ષ રજૂ કર્યો હતો. આ બેઠકમાં (વોરેન, લુમ્સડેન, લિકાટા અને શુલમેન દ્વારા) સાબિતીની રૂપરેખા રજૂ કરવામાં આવી હતી કે દરેક હોમોટૉપી સમાનતા એક સમાનતા છે (વોવોડસ્કીના સારા સુસંગત અર્થમાં), જે સંલગ્ન સમાનતાઓમાં સમાનતા સુધારવાના શ્રેણી સિદ્ધાંતના વિચાર પર આધારિત છે. ત્યારબાદ ટૂંક સમયમાં, વોવોડસ્કીએ સાબિત કર્યું કે સમાનતાનો સ્વયંસિદ્ધ અર્થ કાર્ય વિસ્તરણ સૂચવે છે. આગામી નિર્ણાયક ઘટના માર્ચ 2011 માં ઓબેરવોલ્ફચની મેથેમેટિકલ રિસર્ચ ઇન્સ્ટિટ્યૂટ ખાતે સ્ટીવ ઓવોડી, રિચાર્ડ ગાર્નર, પર માર્ટિન-લોફ અને વ્લાદિમીર વોવોડસ્કી દ્વારા આયોજિત એક નાની વર્કશોપ હતી, જેનું શીર્ષક "રચનાત્મક પ્રકાર સિદ્ધાંતનું હોમોટૉપી અર્થઘટન" હતું. આ વર્કશોપ માટે કોક ટ્યુટોરિયલના ભાગરૂપે, આન્દ્રેજ બાઉરએ વોવોડસ્કીના વિચારોના આધારે એક નાની કોક લાઇબ્રેરી લખી હતી (પરંતુ વાસ્તવમાં તેના કોઈ પણ કોડનો ઉપયોગ કર્યો ન હતો); આ આખરે "હોટીટી" કોક લાઇબ્રેરીના પ્રથમ સંસ્કરણનું કર્નલ બની ગયું હતું (માઇકલ શુલમેન દ્વારા બાદમાં પ્રથમ કમિટ નોંધે છે કે "વિકાસ એન્ડ્રેજ બાઉરની ફાઇલો પર આધારિત છે, જેમાં વ્લાદિમીર વોવોડસ્કીની ફાઇલોમાંથી લેવામાં આવેલા ઘણા વિચારો છે"). લુમ્સડેઇન, શુલમેન, બાઉર અને વોરેનને કારણે ઓબેરવોલ્ફેક મીટિંગમાંથી બહાર આવવાની સૌથી મહત્વપૂર્ણ બાબતોમાંનો એક ઉચ્ચ પ્રેરક પ્રકારોનો મૂળભૂત વિચાર હતો. સહભાગીઓએ મહત્વપૂર્ણ ખુલ્લા પ્રશ્નોની યાદી પણ તૈયાર કરી હતી, જેમ કે શું સમાનતાનો સ્વયંસિદ્ધ સિદ્ધાંત માન્યતાને સંતોષે છે (હજુ પણ ખુલ્લો છે, જોકે કેટલાક વિશેષ કેસો હકારાત્મક રીતે ઉકેલવામાં આવ્યા છે), શું સમાનતાનો સ્વયંસિદ્ધ સિદ્ધાંત બિન-માનક નમૂનાઓ ધરાવે છે (ત્યારથી શુલમેન દ્વારા હકારાત્મક જવાબ આપવામાં આવ્યો છે), અને (અર્ધ) સરળ પ્રકારોને કેવી રીતે વ્યાખ્યાયિત કરવા (હજુ પણ એમ. એલ. ટી. ટી. માં ખુલ્લા છે, જો કે તે વોવોડસ્કીની હોમોટોપી પ્રકાર પ્રણાલી (એચ. ટી. એસ.) માં કરી શકાય છે, જે બે સમાનતાના પ્રકારો સાથેનો એક પ્રકાર સિદ્ધાંત છે). ઓબેરવોલ્ફચ વર્કશોપ પછી તરત જ, હોમોટોપી ટાઇપ થિયરી વેબસાઇટ અને બ્લોગની સ્થાપના કરવામાં આવી હતી, અને તે નામ હેઠળ આ વિષય લોકપ્રિય બનવાનું શરૂ થયું હતું. આ સમયગાળા દરમિયાન કેટલીક મહત્વપૂર્ણ પ્રગતિનો ખ્યાલ બ્લોગના ઇતિહાસમાંથી મેળવી શકાય છે. સમાનતાવાળા પાયા શબ્દસમૂહ "સમાનતાવાળા પાયા" બધા દ્વારા હોમોટોપી પ્રકાર સિદ્ધાંત સાથે નજીકથી સંબંધિત હોવા માટે સંમત છે, પરંતુ દરેક વ્યક્તિ તેનો સમાન રીતે ઉપયોગ કરતા નથી. તેનો મૂળ ઉપયોગ વ્લાદિમીર વોવોડસ્કી દ્વારા ગણિત માટે પાયાની પ્રણાલીની તેમની દ્રષ્ટિનો સંદર્ભ આપવા માટે કરવામાં આવ્યો હતો જેમાં મૂળભૂત પદાર્થો સમસ્થાનિક પ્રકારો છે, જે § સમાનતાના સિદ્ધાંતને સંતોષતા પ્રકાર સિદ્ધાંત પર આધારિત છે, અને કમ્પ્યુટર પ્રૂફ સહાયકમાં ઔપચારિક છે. જેમ જેમ વોવોડસ્કીનું કાર્ય હોમોટૉપી પ્રકાર સિદ્ધાંત પર કામ કરતા અન્ય સંશોધકોના સમુદાય સાથે સંકલિત થયું તેમ, "અવિભાજ્ય પાયો" નો ઉપયોગ કેટલીકવાર "હોમોટૉપી પ્રકાર સિદ્ધાંત" સાથે એકબીજાના બદલે કરવામાં આવતો હતો, અને અન્ય સમયે માત્ર પાયાની પ્રણાલી તરીકે તેનો ઉપયોગ કરવા માટે કરવામાં આવતો હતો (ઉદાહરણ તરીકે, મોડેલ-શ્રેણીબદ્ધ સિમેન્ટિક્સ અથવા કોમ્પ્યુટેશનલ મેટાથિયરીનો અભ્યાસ સિવાય). દાખલા તરીકે, આઇએએસ વિશેષ વર્ષના વિષયને સત્તાવાર રીતે "સમાન પાયા" તરીકે આપવામાં આવ્યો હતો, જો કે ત્યાં કરવામાં આવેલું ઘણું કામ પાયા ઉપરાંત શબ્દાર્થ અને મેટાથિયરી પર કેન્દ્રિત હતું. આઈ. એ. એસ. કાર્યક્રમમાં સહભાગીઓ દ્વારા તૈયાર કરવામાં આવેલા પુસ્તકનું શીર્ષક "હોમોટોપી ટાઇપ થિયરીઃ યુનિવેલેન્ટ ફાઉન્ડેશન્સ ઓફ મેથેમેટિક્સ" હતું; જોકે આ ક્યાં તો ઉપયોગનો સંદર્ભ આપી શકે છે, કારણ કે પુસ્તકમાં માત્ર એચઓટીટીને ગાણિતિક પાયો તરીકે ચર્ચા કરવામાં આવી છે. ઇન્સ્ટિટ્યૂટ ફોર એડવાન્સ્ડ સ્ટડીના સંશોધકોએ ગણિતના અસમાન પાયા પર વિશેષ વર્ષ "ગણિતના અસમાન પાયા પર વિશેષ વર્ષ" નું આયોજન કર્યું હતું. આ વિશેષ વર્ષ ટોપોલોજી, કોમ્પ્યુટર વિજ્ઞાન, શ્રેણી સિદ્ધાંત અને ગાણિતિક તર્કશાસ્ત્રના સંશોધકોને એક સાથે લાવ્યું હતું. આ કાર્યક્રમનું આયોજન સ્ટીવ ઓવોડી, થિએરી કોક્વાંડ અને વ્લાદિમીર વોવોડસ્કી દ્વારા કરવામાં આવ્યું હતું. કાર્યક્રમ દરમિયાન પીટર એક્ઝેલ, જે સહભાગીઓમાંના એક હતા, તેમણે એક કાર્યકારી જૂથની શરૂઆત કરી હતી જેણે ટાઇપ થિયરીને અનૌપચારિક રીતે પરંતુ સખત રીતે કેવી રીતે કરવી તેની તપાસ કરી હતી, જે સેટ થિયરી કરતા સામાન્ય ગણિતશાસ્ત્રીઓ જેવી શૈલીમાં છે. પ્રારંભિક પ્રયોગો પછી તે સ્પષ્ટ થઈ ગયું કે આ માત્ર શક્ય જ નહોતું પણ અત્યંત ફાયદાકારક હતું, અને એક પુસ્તક (કહેવાતા એચઓટીટી બુક) લખી શકાય છે અને લખવું જોઈએ. પ્રોજેક્ટના અન્ય ઘણા સહભાગીઓ પછી તકનીકી સહાય, લેખન, પ્રૂફ રીડિંગ અને વિચારો રજૂ કરીને આ પ્રયાસમાં જોડાયા. ગણિતના લખાણ માટે અસામાન્ય રીતે, તે સહયોગથી વિકસાવવામાં આવ્યું હતું અને GitHub પર ખુલ્લામાં, ક્રિએટિવ કોમન્સ લાઇસન્સ હેઠળ પ્રકાશિત કરવામાં આવ્યું છે જે લોકોને પુસ્તકના પોતાના સંસ્કરણને ફોર્ક કરવાની મંજૂરી આપે છે, અને તે પ્રિન્ટમાં ખરીદી શકાય છે અને મફત ડાઉનલોડ કરી શકાય છે. વધુ સામાન્ય રીતે, આ વિશેષ વર્ષ સમગ્ર વિષયના વિકાસ માટે ઉત્પ્રેરક હતું; સૌથી વધુ દૃશ્યમાન પરિણામ હોવા છતાં, એચઓટીટી બુક માત્ર એક જ હતું. વિશેષ વર્ષમાં સત્તાવાર સહભાગીઓ પીટર એસ્ઝેલ બેનેડિક્ટ અહ્રેન્સ થોર્સ્ટન અલ્ટેન્કિર્ચ સ્ટીવ ઓવોડે બ્રુનો બારાસ એન્ડ્રેજ બાઉર યવેસ બેર્ટોટ માર્ક બેઝેમ થિએરી કોક્વાંડ એરિક ફિન્સ્ટર ડેનિયલ ગ્રેસન હ્યુગો હર્બેલિન એન્ડ્રે જોયલ ડેન લિકાટા પીટર લુમ્સડેન એસિયા મહબોબી પર માર્ટિન-લોફ સર્ગેઈ મેલિખોવ અલ્વારો પેલાયો એન્ડ્રુ પોલોનસ્કી માઇકલ શુલમેન મેથ્યુ સોઝેઉ બાસિટર્સ બેનો વાન ડેન બર્ગ વ્લાદિમીર વોવોડસ્કી માઈકલ વોરેન નોઆમ ઝીલબર્ગર એસીએમ કમ્પ્યુટિંગ સમીક્ષાઓએ આ પુસ્તકને "મેથેમેટિક્સ ઓફ કમ્પ્યુટિંગ" શ્રેણીમાં 2013ના નોંધપાત્ર પ્રકાશન તરીકે સૂચિબદ્ધ કર્યું. મુખ્ય વિભાવનાઓ "પ્રપોઝિશન એઝ ટાઇપ્સ" એચઓટીટી પ્રકાર સિદ્ધાંતના "પ્રપોઝિશન એઝ ટાઇપ્સ" અર્થઘટનના સુધારેલા સંસ્કરણનો ઉપયોગ કરે છે, જે અનુસાર પ્રકારો પણ પ્રપોઝિશનનું પ્રતિનિધિત્વ કરી શકે છે અને શરતો પછી સાબિતીનું પ્રતિનિધિત્વ કરી શકે છે. જોકે, એચ. ઓ. ટી. ટી. માં, પ્રમાણભૂત "પ્રકારો તરીકે દરખાસ્તો" થી વિપરીત, 'માત્ર દરખાસ્તો' દ્વારા વિશેષ ભૂમિકા ભજવવામાં આવે છે, જે, આશરે કહીએ તો, તે પ્રકારો છે જે પ્રસ્તાવાત્મક સમાનતા સુધી મહત્તમ એક શબ્દ ધરાવે છે. આ સામાન્ય પ્રકારો કરતાં વધુ પરંપરાગત તાર્કિક દરખાસ્તો જેવા છે, જેમાં તેઓ સાબિતી-અપ્રસ્તુત છે. સમાનતા હોમોટૉપી પ્રકાર સિદ્ધાંતનો મૂળભૂત ખ્યાલ એ માર્ગ છે. એચઓટીટીમાં, પ્રકાર એ બિંદુથી બિંદુ સુધીના તમામ રસ્તાઓનો પ્રકાર છે. (તેથી, એક બિંદુ એક બિંદુ બરાબર છે તેનો પુરાવો એ બિંદુથી બિંદુ સુધીનો માર્ગ સમાન છે.) કોઈપણ બિંદુ માટે, સમાનતાના પ્રતિબિંબીત ગુણધર્મને અનુરૂપ પ્રકારનો એક માર્ગ અસ્તિત્વમાં છે. પ્રકારનો માર્ગ ઊંધો કરી શકાય છે, જે સમાનતાના સમપ્રમાણ ગુણધર્મને અનુરૂપ પ્રકારનો માર્ગ બનાવે છે. રેસ્પ પ્રકારનાં બે માર્ગો. તેને સંયોજિત કરી શકાય છે, જે પ્રકારનો માર્ગ બનાવે છે; આ સમાનતાના સંક્રમક ગુણધર્મને અનુરૂપ છે. સૌથી અગત્યનું, માર્ગ અને અમુક મિલકતનો પુરાવો આપવામાં આવે તો, મિલકતનો પુરાવો આપવા માટે સાબિતીને રસ્તામાં "પરિવહન" કરી શકાય છે. (સમાન રીતે કહીએ તો, પ્રકારની વસ્તુને પ્રકારની વસ્તુમાં ફેરવી શકાય છે.) આ સમાનતાની અવેજી મિલકતને અનુરૂપ છે. અહીં, એચઓટીટી અને શાસ્ત્રીય ગણિત વચ્ચેનો એક મહત્વપૂર્ણ તફાવત આવે છે. શાસ્ત્રીય ગણિતમાં, એકવાર બે મૂલ્યોની સમાનતા સ્થાપિત થઈ ગઈ છે, અને તે પછી તેમની વચ્ચેના કોઈપણ તફાવતને ધ્યાનમાં લીધા વિના, એકબીજાના બદલે તેનો ઉપયોગ કરી શકાય છે. હોમોટૉપી પ્રકાર સિદ્ધાંતમાં, જો કે, બહુવિધ જુદા જુદા માર્ગો હોઈ શકે છે, અને બે જુદા જુદા માર્ગો પર ઑબ્જેક્ટનું પરિવહન બે અલગ અલગ પરિણામો આપશે. તેથી, હોમોટૉપી પ્રકાર સિદ્ધાંતમાં, અવેજી ગુણધર્મ લાગુ કરતી વખતે, કયા માર્ગનો ઉપયોગ કરવામાં આવી રહ્યો છે તે જણાવવું જરૂરી છે. સામાન્ય રીતે, "દરખાસ્ત" માં બહુવિધ પુરાવા હોઈ શકે છે. (ઉદાહરણ તરીકે, તમામ પ્રાકૃતિક સંખ્યાઓનો પ્રકાર, જ્યારે દરખાસ્ત તરીકે ગણવામાં આવે છે, ત્યારે પુરાવા તરીકે દરેક પ્રાકૃતિક સંખ્યા હોય છે.) જો દરખાસ્તમાં માત્ર એક જ પુરાવો હોય, તો પણ માર્ગની જગ્યા કોઈક રીતે બિન-તુચ્છ હોઈ શકે છે. "માત્ર દરખાસ્ત" એ કોઈપણ પ્રકાર છે જે ક્યાં તો ખાલી છે, અથવા તુચ્છ પાથ સ્પેસ સાથે માત્ર એક જ બિંદુ ધરાવે છે. નોંધ લો કે લોકો માટે લખે છે, જેથી ગર્ભિત પ્રકાર છોડી દે છે. તેની સાથે મૂંઝવણ ન કરો, જે ઓળખ કાર્યને સૂચવે છે. પ્રકાર સમાનતા બે પ્રકારો અને કેટલાક બ્રહ્માંડ સાથે જોડાયેલા હોય તો તેમની વચ્ચે સમાનતા અસ્તિત્વમાં હોય તો તેને સમકક્ષ તરીકે વ્યાખ્યાયિત કરવામાં આવે છે. સમાનતા એ એક એવું વિધેય છે જેમાં ડાબી બાજુએ ઊલટું અને જમણી બાજુએ ઊલટું બંને હોય છે, એ અર્થમાં કે યોગ્ય રીતે પસંદ કરવા માટે અને નીચેના પ્રકારો બંને વસવાટ કરે છેઃ એટલે કે. આ સમાનતાના પ્રકારોનો ઉપયોગ કરીને "ડાબી બાજુ અને જમણી બાજુ બંને વિરુદ્ધ છે" ની સામાન્ય કલ્પનાને વ્યક્ત કરે છે. નોંધ લો કે ઉપરની ઇન્વર્ટિબિલિટી શરતો ફંક્શન પ્રકારો અને માં સમાનતા પ્રકારો છે. એક સામાન્ય રીતે કાર્ય વિસ્તરણ સ્વયંસિદ્ધ ધારણ કરે છે, જે સુનિશ્ચિત કરે છે કે આ નીચેના પ્રકારોની સમકક્ષ છે જે ડોમેન અને કોડોમેન પર સમાનતાનો ઉપયોગ કરીને વ્યુત્ક્રમતા વ્યક્ત કરે છે અનેઃ એટલે કે. બધા માટે અને, પ્રકારનાં કાર્યો એકસાથે પુરાવા સાથે સૂચવવામાં આવે છે કે તેઓ સમાનતાઓ છે. અવિભાજ્ય સ્વયંસિદ્ધ એવા કાર્યોને વ્યાખ્યાયિત કર્યા પછી કે જે ઉપરની જેમ સમાનતાઓ છે, તે બતાવી શકે છે કે સમાનતા તરફનો માર્ગ ફેરવવાની એક પ્રમાણભૂત રીત છે. બીજા શબ્દોમાં કહીએ તો, પ્રકારનું એક કાર્ય છે જે વ્યક્ત કરે છે કે જે પ્રકારો સમાન છે, ખાસ કરીને, તે પણ સમકક્ષ છે. સમાનતા સ્વયંસિદ્ધ જણાવે છે કે આ કાર્ય પોતે એક સમાનતા છે. તેથી, આપણી પાસે "બીજા શબ્દોમાં કહીએ તો, ઓળખ એ સમાનતાની સમકક્ષ છે. ખાસ કરીને, કોઈ એવું કહી શકે છે કે 'સમકક્ષ પ્રકારો સમાન છે'. માર્ટિન હોટ્ઝેલ એસ્કાર્ડોએ દર્શાવ્યું છે કે સમાનતાનો ગુણધર્મ માર્ટિન-લોફ પ્રકાર સિદ્ધાંત (એમએલટીટી) થી સ્વતંત્ર છે. એપ્લિકેશન્સ સિદ્ધાંતો વકીલો દાવો કરે છે કે HOTT ગાણિતિક સાબિતીઓને કોમ્પ્યુટર પ્રૂફ સહાયકો માટે કોમ્પ્યુટર પ્રોગ્રામિંગ ભાષામાં પહેલાં કરતાં વધુ સરળતાથી અનુવાદિત કરવાની મંજૂરી આપે છે. તેઓ દલીલ કરે છે કે આ અભિગમ કમ્પ્યુટર માટે મુશ્કેલ પુરાવા તપાસવાની ક્ષમતામાં વધારો કરે છે. જો કે, આ દાવાઓ સાર્વત્રિક રીતે સ્વીકારવામાં આવતા નથી અને ઘણા સંશોધન પ્રયાસો અને પુરાવા સહાયકો એચઓટીટીનો ઉપયોગ કરતા નથી. એચઓટીટી એકરૂપતાના સિદ્ધાંતને અપનાવે છે, જે લોજિકલ-ગાણિતિક દરખાસ્તોની સમાનતાને હોમોટૉપી સિદ્ધાંત સાથે સંબંધિત કરે છે. "a = b" જેવા સમીકરણ એ એક ગાણિતિક દરખાસ્ત છે જેમાં બે અલગ અલગ પ્રતીકોનું મૂલ્ય સમાન હોય છે. હોમોટૉપી પ્રકાર સિદ્ધાંતમાં, આનો અર્થ એ થાય છે કે પ્રતીકોના મૂલ્યોનું પ્રતિનિધિત્વ કરતા બે આકારો ટોપોલોજીકલ રીતે સમકક્ષ છે. આ સમાનતા સંબંધો, ETH ઝુરિચ ઇન્સ્ટિટ્યૂટ ફોર થિયોરેટિકલ સ્ટડીઝના ડિરેક્ટર જીઓવાન્ની ફેલ્ડર દલીલ કરે છે કે, હોમોટોપી થિયરીમાં વધુ સારી રીતે ઘડવામાં આવી શકે છે કારણ કે તે વધુ વ્યાપક છેઃ હોમોટોપી થિયરી માત્ર "a બરાબર b" જ કેમ નથી પણ આ કેવી રીતે મેળવવું તે પણ સમજાવે છે. સમૂહ સિદ્ધાંતમાં, આ માહિતીને વધુમાં વ્યાખ્યાયિત કરવી પડશે, જે હિમાયતીઓ દલીલ કરે છે કે, પ્રોગ્રામિંગ ભાષાઓમાં ગાણિતિક દરખાસ્તોના અનુવાદને વધુ મુશ્કેલ બનાવે છે. કોમ્પ્યુટર પ્રોગ્રામિંગ 2015 સુધીમાં, હોમોટોપી પ્રકાર સિદ્ધાંતમાં એકરૂપતાના સ્વયંસિદ્ધના કોમ્પ્યુટેશનલ વર્તનનું મોડેલ અને ઔપચારિક રીતે વિશ્લેષણ કરવા માટે તીવ્ર સંશોધન કાર્ય ચાલી રહ્યું હતું. ક્યુબિકલ પ્રકાર સિદ્ધાંત એ હોમોટૉપી પ્રકાર સિદ્ધાંતને કોમ્પ્યુટેશનલ સામગ્રી આપવાનો એક પ્રયાસ છે. જો કે, એવું માનવામાં આવે છે કે અમુક વસ્તુઓ, જેમ કે અર્ધ-સરળ પ્રકારો, ચોક્કસ સમાનતાની કેટલીક કલ્પનાના સંદર્ભ વિના બનાવી શકાતા નથી. તેથી, વિવિધ બે-સ્તરના પ્રકારનાં સિદ્ધાંતો વિકસાવવામાં આવ્યા છે જે તેમના પ્રકારોને તંતુમય પ્રકારોમાં વિભાજિત કરે છે, જે માર્ગને માન આપે છે અને બિન-તંતુમય પ્રકારો, જે નથી કરતા. કાર્ટેશિયન ક્યુબિકલ કોમ્પ્યુટેશનલ પ્રકારનો સિદ્ધાંત એ પ્રથમ બે-સ્તરનો પ્રકારનો સિદ્ધાંત છે જે હોમોટૉપી પ્રકાર સિદ્ધાંતને સંપૂર્ણ કોમ્પ્યુટેશનલ અર્થઘટન આપે છે. આ પણ જુઓ બાંધકામોની ગણતરી કરી-હોવર્ડ પત્રવ્યવહાર અંતઃપ્રેરણાત્મક પ્રકાર સિદ્ધાંત હોમોટોપી પૂર્વધારણા યુનિવેલેન્ટ ફાઉન્ડેશન્સ નોટ્સ રેફરન્સ ગ્રંથસૂચિ (આ લેખમાં ટાંકવામાં આવેલ ગિટહબ સંસ્કરણ). પીડીએફ તરીકે. પોસ્ટસ્ક્રિપ્ટ તરીકે. ડેવિડ કોર્ફીલ્ડ (2020), મોડલ હોમોટોપી ટાઇપ થિયરીઃ ધ પ્રોસ્પેક્ટ ઓફ એ ન્યૂ લોજિક ફોર ફિલોસોફી, ઓક્સફર્ડ યુનિવર્સિટી પ્રેસ. એગબર્ટ રિજકે (2022), હોમોટોપી પ્રકાર સિદ્ધાંતનો પરિચય,. પરિચયાત્મક પાઠ્યપુસ્તક. બાહ્ય કડીઓ અનોખો પાયો વિકિ વ્લાદિમીર વોવોડસ્કીનું વેબપેજ અનોખો પાયો સ્ટીવ ઓવોડી દ્વારા હોમોટોપી પ્રકાર સિદ્ધાંત અને ગણિતના અનોખો પાયો "રચનાત્મક પ્રકાર સિદ્ધાંત અને હોમોટોપી"-ઇન્સ્ટિટ્યૂટ ફોર એડવાન્સ્ડ સ્ટડી લાઇબ્રેરીઝ ઓફ ફોર્મલાઇઝ્ડ મેથેમેટિક્સ ખાતે સ્ટીવ ઓવોડી દ્વારા વિડિયો વ્યાખ્યાન (હવે યુનિમેથમાં સંકલિત છે, જ્યાં વધુ વિકાસ થાય છે) ગણિતનો પાયો પ્રકાર સિદ્ધાંત ઔપચારિક પદ્ધતિઓ વિડિયો ક્લિપ્સ ધરાવતા લેખો