The internal languages of univalent categories

तकनीकी सारांश: यूनिलिएंट श्रेणियों की आंतरिक भाषाएँ

समस्या विवरण
कैटेगोरिकल लॉजिक में आंतरिक भाषा प्रमेय (internal language theorems) टाइप थ्योरी (syntax) और कैटेगोरिकल मॉडल (semantics) के बीच एक तुल्यता स्थापित करते हैं। क्लेरैम्बोल्ट और डाइब्जर [CD14] द्वारा एक महत्वपूर्ण परिणाम ने सीली के मूल प्रमेय [See84] को सुधारा, जिससे स्थानीय रूप से कार्टेशियन क्लोज्ड कैटेगरीज (LCCCs) के बिकेटिगरी और एक्सटेंशनल आइडेंटिटी टाइप्स, $\Sigma$-टाइप्स, और $\Pi$-टाइप्स का समर्थन करने वाली डेमोक्रेटिक कैटेगरीज विद फॅमिलीज़ (CwFs) के बीच एक बी-इक्विवेलेंस (biequivalence) स्थापित की।

हालाँकि, यह परिणाम सेट-थ्योरेटिक फाउंडेशन्स के भीतर तैयार किया गया था। यूनिलिएंट फाउंडेशन्स (होमोटॉपी टाइप थ्योरी) में, CwF की मानक धारणा एक मौलिक बाधा का सामना करती है: यूनिलिएंट एक्सिओम यह निहित करता है कि सेट्स का प्रकार स्वयं एक सेट नहीं है (यह एक 1-टाइप है)। फलस्वरूप, CwFs में यह आवश्यकता कि कॉन्टेक्स्ट में टाइप्स का संग्रह एक सेट हो, उल्लंघन हो जाती है। इसके अतिरिक्त, "चुनी गई" संरचना (जैसे, स्प्लिट फाइब्रेशंस) और "अस्तित्व वाली" संरचना (जैसे, आइसोमॉर्फिज्म तक लिमिट्स) के बीच का अंतर कोहेरेंस संबंधी मुद्दे पैदा करता है, जिसके लिए चॉइस के एक्सिओम या स्ट्रिक्टिफिकेशन प्रक्रियाओं की आवश्यकता होती है। यूनिलिएंट फाउंडेशन्स में, जहाँ आइसोमॉर्फिज्म पहचान (identity) को दर्शाता है, ये अंतर समाप्त हो जाते हैं, लेकिन CwFs का मौजूदा ढांचा सीधे तौर पर लागू करने योग्य नहीं है।

कार्यप्रणाली
यह शोध पत्र यूनिलिएंट फाउंडेशन्स के भीतर कैटेगोरिकल सेमैंटिक्स के लिए एक नया ढांचा विकसित करता है, जिसमें CwFs के बजाय यूनिलिएंट कैटेगरीज और कंप्रिहेन्शन कैटेगरीज का उपयोग किया जाता है।

1. यूनिलिएंट कैटेगरीज: लेखक उन श्रेणियों के साथ कार्य करते हैं जहाँ ऑब्जेक्ट्स का आइडेंटिटी टाइप आइसोमॉर्फिज्म (एडजॉइंट इक्विवेलेंस) के समकक्ष होता है। यह एडजॉइंट इक्क्विवेलेंस को आइडेंटिटी के रूप में उपचारित करने की अनुमति देता है, जिससे संरचना के संरक्षण (जैसे, एक्सपोनेन्शियल्स) के संबंध में प्रमाणों को सरल बनाया जा सकता है और लिमिट्स को चुनने के लिए चॉइस के एक्सिओम की आवश्यकता को समाप्त किया जा सकता है।
2. कंप्रिहेन्शन कैटेगरीज: यह सुनिश्चित करने के लिए कि टाइप्स को सेट बनाने की आवश्यकता न हो, शोध पत्र कंप्रिहेन्शन कैटेगरीज (फाइब्रेशंस और डिस्प्लेड कैटेगरीज पर आधारित) को अपनाता है। एक कंप्रिहेन्शन कैटेगरी में कॉन्टेक्स्ट्स की एक बेस कैटेगरी, टाइप्स की एक डिस्प्लेड कैटेगरी, एक क्लीविंग (प्रतिस्थापन प्रदान करने के लिए), और एक कंप्रिहेन्शन फंकटर होता है। लेखक अपना ध्यान यूनिलिएंट फुल कंप्रिहेन्शन कैटेगरीज पर केंद्रित करते हैं, जहाँ बेस और डिस्प्लेड कैटेगरी दोनों यूनिलिएंट होते हैं।
3. डिस्प्लेड बिकेटिगरीज: मॉडल्स की बिकेटिगरीज का निर्माण डिस्प्लेड बिकेटिगरीज [AFM+21] पर अत्यधिक निर्भर है। यह मॉड्यूलर दृष्टिकोण लेखक को सरल बेस बिकेटिगरीज पर गुणों (जैसे, फाइनाइट लिमिट्स, $\Pi$-टाइप्स, यूनिवर्स) की परतें चढ़ाकर जटिल बिकेटिगरीज (जैसे, LCCCs या टोपोस) बनाने की अनुमति देता है। यह मॉड्यूलरिटी यह सिद्ध करने में सुविधा प्रदान करती है कि परिणामी बिकेटिगरीज स्वयं यूनिलिएंट हैं।
4. लोकल प्रॉपर्टीज: श्रेणियों से अधिक जटिल संरचनाओं जैसे टोपोस तक परिणामों का विस्तार करने के लिए, यह पत्र माईटी के लोकल प्रॉपर्टीज [Mai05] के विचार को अनुकूलित करता है। लोकल प्रॉपर्टी एक कैटेगरी पर आधारित स्थिति है जो स्लाइसिंग के तहत बंद होती है। लेखक इसे बेस केस (फाइनाइट लिमिट्स) से विभिन्न वर्गों के टोपोस तक बी-इक्विवेलेंस को विस्तारित करने के लिए डिस्प्लेड बिकेटिगरी फ्रेमवर्क के भीतर औपचारिक रूप देते हैं।
5. री-इंडेक्सिंग और यूनिवर्स: यूनिवर्स के उपचार के लिए, शोध पत्र डिस्प्लेड बिकेटिगरीज की री-इंडेक्सिंग का उपयोग करता है। यह तकनीक एक बेस कैटेगरी से डिस्प्लेड कैटेगरी पर बी-इक्विवेलेंस को स्थानांतरित करने की अनुमति देती है, जिससे विशिष्ट टाइप फॉर्मर्स (जैसे, $\Sigma$, $\Pi$, नेचुरल नंबर्स) के लिए बंद यूनिवर्स को परिभाषित करना संभव होता है, बिना सख्त स्टेबिलिटी लॉज की आवश्यकता के, बल्कि आइसोमॉर्फिज्म तक स्टेबिलिटी के साथ।

प्रमुख योगदान
यह शोध पत्र चार प्राथमिक योगदान देता है:

1. क्लेरैम्बोल्ट-डाइब्जर का यूनिलिएंट एनालॉग: लेखक यूनिलिएंट कैटेगरीज विद फाइनाइट लिमिट्स और यूनिलिएंट फुल डेमोक्रेटिक फाइनाइट लिमिट (DFL) कंप्रिहेन्शन कैटेगरीज के बीच एक बी-इक्विवेलेंस का निर्माण करते हैं। यह स्थापित करता है कि यूनिलिएंट कैटेगरीज विद फाइनाइट लिमिट्स की आंतरिक भाषा एक्सटेंशनल मार्टिन-लॉफ टाइप थ्योरी है जिसमें यूनिट, बाइनरी प्रोडक्ट, और $\Sigma$-टाइप्स शामिल हैं।
2. लोकेली कार्टेशियन क्लोज्ड कैटेगरीज तक विस्तार: बी-इक्विवेलेंस को यूनिलिएंट लोकेली कार्टेशियन क्लोज्ड कैटेगरीज और $\Pi$-टाइप्स का समर्थन करने वाली DFL कंप्रिहेन्शन कैटेगरीज तक विस्तारित किया गया है। यह पुष्टि करता है कि यूनिलिएंट LCCCs की आंतरिक भाषा $\Pi$-टाइप्स के साथ एक्सटेंशनल मार्टिन-लॉफ टाइप थ्योरी है।
3. टोपोस और यूनिवर्स तक विस्तार: स्थानीय गुणों का उपयोग करके विभिन्न वर्गों के टोपोस (प्री-टोपोस, $\Pi$-प्री-टोपोस, एलिमेंट्री टोपोस, और नेचुरल नंबर्स ऑब्जेक्ट वाले टोपोस) तक पद्धति को सामान्यीकृत किया गया है। इसके अलावा, लेखक इन श्रेणियों में यूनिवर्स को परिभाषित करते हैं जो विशिष्ट टाइप फॉर्मर्स (नेचुरल नंबर्स, सबऑब्जेक्ट क्लासिफायर, प्रोपोजिशनल रिसाइज़िंग, $\Sigma$-टाइप्स, और $\Pi$-टाइप्स) के तहत बंद हैं, जिससे एक यूनिवर्स के साथ एलिमेंट्री टोपोस के लिए एक बी-इक्विवेलेंस स्थापित होता है।
4. औपचारिकीकरण (Formalization): सभी निर्माण और प्रमाणों को यूनिक मैथ लाइब्रेरी का उपयोग करते हुए रोक (Rocq) प्रूफ असिस्टेंट में औपचारिक रूप दिया गया है, जो शुद्धता सुनिश्चित करता है और सिद्धांत के लिए एक मशीन-चेक्ड संदर्भ प्रदान करता है।

परिणाम
यह शोध पत्र सिद्ध करता है कि यूनिलिएंट कैटेगरीज के विभिन्न वर्गों के लिए, संगत यूनिलिएंट कंप्रिहेन्शन कैटेगरीज के साथ एक बी-इक्विवेलेंस मौजूद है। विशेष रूप से:

• फाइनाइट लिमिट्स: यूनिलिएंट कैटेगरीज विद फाइनाइट लिमिट्स $\simeq$ DFL कंप्रिहेन्शन कैटेगरीज (यूनिट, प्रोडक्ट, इक्वलाइज़र, $\Sigma$)।
• LCCC: यूनिलिएंट LCCCs $\simeq$ $\Pi$-टाइप्स के साथ DFL कंप्रिहेन्शन कैटेगरीज।
• टोपोस: यूनिलिएंट एलिमेंट्री टोपोस (NNO के साथ/बिना) $\simeq$ संगत स्थानीय गुणों (जैसे, सबऑब्जेक्ट क्लासिफायर, डिसजॉइंट सम्स, कोटिएंट्स) के साथ DFL कंप्रिहेन्शन कैटेगरीज।
• यूनिवर्स: विशिष्ट टाइप फॉर्मर्स के लिए बंद यूनिवर्स के साथ यूनिलिएंट एलिमेंट्री टोपोस $\simeq$ संगत क्लोजर कंडीशंस को संतुष्ट करने वाले यूनिवर्स ऑब्जेक्ट के साथ DFL कंप्रिहेन्शन कैटेगरीज।

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

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

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