🔢 mathematics

Unbiasing symmetric monoidal categories in Lean

यह शोध पत्र Mathlib के भीतर एक Lean 4 औपचारिकीकरण (formalization) प्रस्तुत करता है जो उनके डेटा को परिमित समुच्चयों के स्पैन (spans) पर एक Cat-मानित स्यूडोफंक्टर (pseudofunctor) तक विस्तारित करके सममित मोनॉइडल श्रेणियों (symmetric monoidal categories) को निष्पक्ष बनाता है, जो उच्च-अैरिटी (higher-arity) टेंसर उत्पादों और उनकी सुसंगति (coherences) को संभालने के लिए मैक लेन के कोहेरेंस प्रमेय (Mac Lane's coherence theorem) और एक क्लेइसली बायकेटिगरी (Kleisli bicategory) एन्कोडिंग का लाभ उठाता है।

मूल लेखक: Robin Carlier

प्रकाशित 2026-03-03

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Robin Carlier

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक बहुत ही व्यस्त रसोई में एक शेफ हैं। आपके पास एक रेसिपी है जो कहती है, "सामग्री A और B को मिलाएं।" यह आसान है। लेकिन क्या होगा अगर रेसिपी कहती है, "सामग्री A, B, C, D और E को मिलाएं"?

सामान्य खाना पकाने (या सामान्य गणित) की दुनिया में, आपको आमतौर पर क्रम का पता लगाना होता है। क्या आप पहले A और B को मिलाते हैं, फिर C जोड़ते हैं? या क्या आप C और D को मिलाते हैं, फिर उस मिश्रण को A और B में डालते हैं? एक सामान्य रसोई में, भले ही अंतिम स्वाद समान हो, लेकिन प्रक्रिया के लिए क्रम मायने रखता है।

यह शोध पत्र एक नया, सुपर-स्मार्ट किचन असिस्टेंट (जिसे Lean 4 नामक कंप्यूटर भाषा में लिखा गया है) बनाने के बारे में है जो एक मौलिक नियम को समझता है: जब आप ऐसी चीजों को मिला रहे होते हैं जो पूरी तरह से सममित (symmetric) हैं, तो उन्हें करने का क्रम वास्तव में मायने नहीं रखता, जब तक कि आपके पास सही सामग्री कटोरे में आ जाए।

यहाँ सरल उपमाओं का उपयोग करके इस शोध पत्र के बड़े विचारों का विवरण दिया गया है:

1. समस्या: "पक्षपाती" (Biased) रेसिपी

पारंपरिक गणित (और Lean लाइब्रेरी के शुरुआती संस्करणों) में, एक "Symmetric Monoidal Category" एक ऐसी रेसिपी की तरह है जो केवल एक बार में दो चीजों को मिलाना जानती है।

यदि आप 5 चीजें मिलाना चाहते हैं, तो कंप्यूटर आपको इसे ((A + B) + C) + (D + E) के रूप में लिखने के लिए मजबूर करता है।
इसे यह सिद्ध करना होगा कि ((A + B) + C), (A + (B + C)) के समान है।
इसे यह सिद्ध करना होगा कि A और B को आपस में बदलने से परिणाम नहीं बदलता है।

इसे "पक्षपाती" (Biased) होना कहा जाता है। कंप्यूटर संचालन के विशिष्ट क्रम के प्रति जुनूनी है। यह एक ऐसे रोबोट शेफ की तरह है जो सलाद बनाने से इनकार कर देता है जब तक कि आप उसे ठीक से न बताएं कि पहले कौन से दो पत्तों को एक साथ मिलाना है, और फिर अगले कौन से दो को। यह काम तो करता है, लेकिन यह उबाऊ और बड़े पैमाने पर ले जाने में कठिन है।

2. समाधान: "पक्षपात रहित" (Unbiased) रसोई

लेखक एक ऐसा सिस्टम बनाना चाहते थे जहाँ कंप्यूटर "पक्षपात रहित" (unbiased) मिश्रण को समझ सके। वे चाहते थे कि हम कह सकें, "यहाँ 100 सामग्रियों की एक सूची है। बस उन सभी को एक साथ मिला दें।" कंप्यूटर को पता होना चाहिए कि आप उन्हें किसी भी तरह से समूह में बांटें, परिणाम समान ही रहेगा।

इसे करने के लिए, उन्होंने केवल रेसिपी नहीं बदली; उन्होंने उस भाषा को बदल दिया जिसे रोबोट बोलता है।

3. जादुई उपकरण: "सिमेट्रिक लिस्ट्स" (Symmetric Lists)

लेखकों ने सामग्रियों के मिश्रण को ब्रैकेट की एक लंबी श्रृंखला के रूप में नहीं, बल्कि एक "Symmetric List" के रूप में दर्शाने का तरीका बनाया।

पुराना तरीका: निर्देशों की एक लंबी, उलझी हुई स्ट्रिंग: (((A+B)+C)+D)...
नया तरीका: सामग्रियों का एक थैला जहाँ क्रम मायने नहीं रखता, लेकिन संख्या (count) मायने रखती है।

उन्होंने एक प्रसिद्ध गणितीय विचार (Mac Lane's Coherence Theorem) को एक चतुर ट्रिक का उपयोग करके सिद्ध किया: Symmetric Lists केवल Permutations (क्रमपरिवर्तन) हैं।
इसे ताश के पत्तों को फेंटने (shuffling) की तरह समझें।

यदि आपके पास [A, B, C] कार्डों की एक सूची है, तो आप उन्हें [B, A, C] प्राप्त करने के लिए फेंट सकते हैं।
लेखकों ने दिखाया कि आपकी सामग्रियों को पुनर्व्यवस्थित करने का हर संभव तरीका (हर "shuffle") एक विशिष्ट, अद्वितीय गणितीय चाल (move) के अनुरूप होता है।
उन्होंने एक कंप्यूटर मॉडल बनाया जहाँ प्रत्येक "shuffle" को एक अद्वितीय ID के साथ लेबल किया जाता है। यदि सामग्रियों को मिलाने के दो अलग-अलग रास्ते एक ही अंतिम shuffle की ओर ले जाते हैं, तो कंप्यूटर जानता है कि वे एक ही परिणाम हैं।

4. सेतु: स्पैन्स (Spans) और ब्रिज

यह शोध पत्र "Spans" की एक अवधारणा का उपयोग करता है। कल्पना कीजिए कि आपके पास दो द्वीप हैं (सेट A और सेट B)। एक "Span" एक तीसरा द्वीप (सेट C) के माध्यम से उन्हें जोड़ने वाला एक पुल है।

A से B तक जाने के लिए, आप A → C → B जाते हैं।
लेखकों ने दिखाया कि आप इन पुलों को एक सार्वभौमिक भाषा के रूप में मान सकते हैं। उन्होंने एक ऐसा सिस्टम बनाया जहाँ "सामग्रियों को मिलाना" केवल एक विशेष प्रकार का पुल पार करना है।

उन्होंने एक Pseudofunctor (एक "अनुवादक" के लिए एक फैंसी शब्द) बनाया जो मानक गणित की जटिल, पक्षपाती दुनिया को "Spans" और "Symmetric Lists" की इस स्वच्छ, पक्षपात रहित दुनिया में अनुवादित करता है।

5. यह क्यों मायने रखता है? ("मुझे इसकी परवाह क्यों करनी चाहिए?")

आप पूछ सकते हैं, "हमें एक ऐसे रोबोट शेफ की आवश्यकता क्यों है जो एक बार में 100 चीजों को मिला सके?"

जटिल सूत्र: उन्नत भौतिकी और ग्रुप थ्योरी में, ऐसे सूत्र होते हैं जिनमें हजारों पदों का योग होता है। "पुराने" तरीके के साथ ऐसा करने के लिए क्रम के बारे में हजारों छोटे चरणों को सिद्ध करने की आवश्यकता होती है। "नया" तरीका कंप्यूटर को बस यह कहने की अनुमति देता है, "इन 1,000 वस्तुओं को जोड़ें," और यह जानता है कि यह वैध है।
भविष्य के लिए तैयारी: लेखक गणित के भविष्य की तैयारी कर रहे हैं, जिसमें "Higher Categories" (वह गणित जो केवल संख्याओं के बजाय आकृतियों और स्थानों से संबंधित है) शामिल हैं। चीजों को करने का "पक्षपाती" तरीका इन उच्च आयामों में विफल हो जाता है। उन्होंने जो "पक्षपात रहित" तरीका बनाया है, वही इन जटिल, बहु-आयामी गणितीय समस्याओं तक स्केल करने का एकमात्र तरीका है।
विश्वास: इसे Lean 4 में लिखकर, उन्होंने केवल यह कहा नहीं कि यह काम करता है; उन्होंने कंप्यूटर को हर एक तार्किक चरण की जांच करने के लिए मजबूर किया। यदि उनके तर्क में कोई कमी होती, तो कंप्यूटर कोड को कंपाइल करने से मना कर देता।

निचोड़ (The Bottom Line)

यह शोध पत्र गणित को क्रम की तानाशाही से मुक्त करने के बारे में है।

लेखकों ने एक डिजिटल ढांचा बनाया जो कंप्यूटर को यह समझने की अनुमति देता है कि जब आप सममित चीजों (जैसे सलाद मिलाना या संख्याएं जोड़ना) के साथ काम कर रहे होते हैं, तो "पहले यह, फिर वह" का विशिष्ट क्रम केवल एक भ्रम है। परिणाम एक मजबूत, "पक्षपात रहित" सिस्टम है जो उन जटिल, बड़े पैमाने के गणितीय ढांचों को संभाल सकता है जो पहले कंप्यूटर के लिए विश्वसनीय रूप से संभालना बहुत कठिन था।

यह एक ऐसे कैलकुलेटर से अपग्रेड करने जैसा है जो एक बार में केवल दो संख्याएं जोड़ना जानता है, एक सुपर-कंप्यूटर में जो "संख्याओं के ढेर" की अवधारणा को समझता है और उन्हें तुरंत जोड़ सकता है, चाहे आपने उन्हें मेज पर किसी भी तरह से व्यवस्थित किया हो।

यहाँ रॉबिन कार्लियर के शोध पत्र "Unbiasing symmetric monoidal categories in Lean" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

औपचारिक गणित (विशेष रूप से Lean 4 प्रूफ़ असिस्टेंट और Mathlib लाइब्रेरी के भीतर) में, एक सममित मोनॉइडल श्रेणी (symmetric monoidal category) की मानक परिभाषा "बायस्ड" (biased) है। इसे केवल बाइनरी टेंसर उत्पादों ( $\otimes$ ), एक यूनिट ऑब्जेक्ट ($1$), और इन निम्न-आयामी (low-arity) ऑपरेशनों के लिए विशिष्ट कोहेरेंस आइसोमॉर्फिज्म (associators, unitors, और braidings) का उपयोग करके परिभाषित किया गया है।

यद्यपि यह परिभाषा न्यूनतम और निर्माण के लिए आसान है, यह उन्नत गणितीय अनुप्रयोगों के लिए महत्वपूर्ण बाधाएँ उत्पन्न करती है:

उच्च आयामी ऑपरेशंस (Higher Arity Operations): कई गणितीय संरचनाओं (जैसे, फ्री कम्यूटेटिव मोनॉइड्स, टेंसर पावर्स $x^{\otimes n}$ , या मनमाने परिमित सेटों पर योग) के लिए, $n$ वस्तुओं के टेंसर उत्पादों को परिभाषित करने के लिए एक कैनोनिकल तरीका चाहिए, जो वस्तुओं के पैरेंटेसाइजिंग (parenthesizing) या क्रम पर निर्भर न हो।
उच्च श्रेणी सिद्धांत (Higher Category Theory): $(\infty, 1)$ -श्रेणियों के सिद्धांत (जैसे, लुरी के $\infty$ -ऑपरड्स या क्रैंच के लॉवेर सिमेट्रिक मोनॉइडल कैटेगरीज) में, सममित मोनॉइडल संरचनाओं को उन स्रोतों से प्राप्त होने वाले स्यूडोफंक्टर्स (pseudofunctors) के रूप में माना जाता है जिनमें सभी परिमित सेट और उनकी सममिति (symmetries) शामिल होती हैं। Mathlib में वर्तमान "बायस्ड" परिभाषा स्वाभाविक रूप से इन उच्च-श्रेणीगत ढाँचों तक नहीं फैल पाती है।
"अनबायसिंग" अंतराल (The "Unbiasing" Gap): एक औपचारिक सेतु (bridge) का अभाव है जो एक मानक बायस्ड सममित मोनॉइडल श्रेणी को लेता है और Lean इकोसिस्टम के भीतर एक "अनबायस्ड" संस्करण (एक स्यूडोफंक्टर जो सभी परिमित टेंसर उत्पादों और उनकी कोहेरेंस को एनकोड करता है) का निर्माण करता है।

2. कार्यप्रणाली (Methodology)

लेखक Mac Lane के कोहेरेंस थ्योरम (Coherence Theorem) पर भरोसा करते हुए, Lean 4 में अनबायसिंग प्रक्रिया को औपचारिक रूप देते हैं। कार्यप्रणाली तीन चरणों में आगे बढ़ती है:

A. सिमेट्रिक लिस्ट्स के माध्यम से कोहेरेंस थ्योरम का औपचारिकीकरण

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

सिमेट्रिक लिस्ट्स ($SList$): फ्री मोनॉइडल श्रेणियों के मानक इंडक्टिव परिभाषा (जो ब्रेडिंग के साथ संघर्ष करती है) के बजाय, लेखक Piceghello के कार्य को Mathlib में अनुकूलित करते हैं। वे सिमेट्रिक लिस्ट्स की एक श्रेणी को परिभाषित करते हैं, जहाँ ऑब्जेक्ट्स तत्वों की सूचियाँ (lists) हैं और मोर्फिज्म "स्वैप्स" ( $sw_{a,b,l}$ ) द्वारा जनरेट होते हैं, जो सिमेट्रिक ग्रुप (Coxeter group relations) की नकल करने वाले संबंधों के अधीन होते हैं।
कॉक्स टर ग्रुप एनकोडिंग (Coxeter Group Encoding): एक प्रमुख तकनीकी योगदान यह है कि $SList$ में मोर्फिज्म, परम्यूटेशन्स (permutations) के साथ द्वैत रूप से सह-संबंध रखते हैं। लेखक सिमेट्रिक लिस्ट श्रेणी के जनरेटरों और कॉक्स टर ग्रुप $A_\infty$ के बीच के संबंध को औपचारिक रूप देते हैं, और यह सिद्ध करते हैं कि एक मोर्फिज्म का "वेट" (label) उसे अद्वितीय रूप से निर्धारित करता है।
तुल्यता (Equivalence): वे सिद्ध करते हैं कि एक सेट $J$ पर सिमेट्रिक लिस्ट की श्रेणी, $J$ पर फ्री सिमेट्रिक मोनॉइडल श्रेणी के तुल्य है। यह "अनबायस्ड" संरचना के लिए एक ठोस, गणना योग्य मॉडल प्रदान करता है।

B. स्पैन बाइकेटिगरीज और स्यूडोफंक्टर्स (Span Bicategories and Pseudofunctors)

अनबायस्ड श्रेणी के लिए लक्षित संरचना परिमित सेटों के स्पैन की बाइकेटिगरी के पिथ ($Pith(Span(Fin))$) से एक स्यूडोफंक्टर है।

स्पैन बाइकेटिगरीज (Span Bicategories): लेखक स्पैन की बाइकेटिगरी को औपचारिक रूप देते हैं, जहाँ 1-मोर्फिज्म स्पैन $A \leftarrow S \to B$ हैं और 2-मोर्फिज्म एपिक्स (apices) के बीच के मोर्फिज्म हैं।
पिथ-बेक-चेवल (Pith-Beck-Chevalley) सिस्टम: चूंकि अनबायसिंग में शामिल फंक्टर्स (टेंसर उत्पाद और पुलबैक) मानक अर्थों में एडजॉइंट (adjoint) नहीं हैं, इसलिए लेखक एक विशिष्ट संरचना पेश करते हैं जिसे पिथ-बेक-चेवल सिस्टम कहा जाता है। इस संरचना में दो स्यूडोफंक्टर्स (एक कोवेरिएंट और एक कॉन्ट्रावेरिएंट) और पुलबैक स्क्वॉयर्स के लिए बेस-चेंज आइसोमॉर्फिज्म का एक परिवार शामिल है।
थ्योरम 3.3: यह पेपर सिद्ध करता है कि कोई भी ऐसा सिस्टम स्पैन बाइकेटिगरी के पिथ से एक स्यूडोफंक्टर तक अद्वितीय रूप से विस्तारित होता है।

C. क्लेस्की बाइकेटिगरी और द्वैतता (The Kleisli Bicategory and Duality)

स्पैन बाइकेटिगरी को सममित मोनॉइडल श्रेणी से जोड़ने के लिए:

क्लेस्की बाइकेटिगरी ( $K_{SList}$ ): लेखक सिमेट्रिक लिस्ट्स के रिलेटिव स्यूडोमोनॉड के लिए एक क्लेस्की बाइकेटिगरी को परिभाषित करते हैं। यह सममित मोनॉइडल श्रेणियों के सार्वभौमिक सूत्रों को एनकोड करने की अनुमति देता है।
ड्युअलिटी फंकटर (Duality Functor): एक महत्वपूर्ण कदम एक ड्युअलिटी फंकटर $D_{J,K}$ का निर्माण करना है जो सिमेट्रिक लिस्ट्स के वेक्टर्स को ट्रांसपोज़ करता है। इसे एक मैट्रिक्स ट्रांसपोज़िशन के रूप में व्याख्यायित किया जाता है जहाँ "एंट्रीज़" परिमित सेट (या सिमेट्रिक लिस्ट्स) हैं।
लीनियर सिमेट्रिक लिस्ट्स (Linear Symmetric Lists): लेखक लीनियर सिमेट्रिक लिस्ट्स (बिना डुप्लिकेट तत्वों वाली लिस्ट्स) की अवधारणा पेश करते हैं। वे सिद्ध करते हैं कि लीनियर लिस्ट्स के बीच मोर्फिज्म अद्वितीय (subsingleton) होते हैं। इस गुण का उपयोग बेस-चेंज आइसोमॉर्फिज्म की कोहेरेंस जांच को स्वचालित करने के लिए किया जाता है, क्योंकि लीनियर लिस्ट्स के बीच कोई भी दो आइसोमॉर्फिज्म समान ही होने चाहिए।

3. मुख्य योगदान (Key Contributions)

मैक लेन के कोहेरेंस थ्योरम का औपचारिकीकरण: एक सेट पर फ्री सिमेट्रिक मोनॉइडल श्रेणी, सिमेट्रिक लिस्ट्स की श्रेणी के तुल्य है, यह सिद्ध करने के लिए Lean 4 में पूर्ण औपचारिकीकरण। इसमें कॉक्स टर ग्रुप वेट्स के माध्यम से परम्यूटेशन्स के साथ सिमेट्रिक लिस्ट्स के मोर्फिज्म के बीच द्वैत संबंध का एक नवीन प्रमाण शामिल है।
अनबायसिंग निर्माण (Unbiasing Construction): किसी भी सममित मोनॉइडल श्रेणी $\mathcal{C}$ से $Cat $तक एक स्यूडोफंक्टर$ \mathcal{C}^\otimes: Pith(Span(Fin)) \to Cat $का निर्माण। यह फंकटर एक परिमित सेट$ J $को उत्पाद श्रेणी$ \mathcal{C}^J$ में मैप करता है और एक स्पैन को फाइबरों पर टेंसर उत्पादों की गणना करने वाले फंकटर के रूप में मैप करता है।
पिथ-बेक-चेवल सिस्टम: स्पैन बाइकेटिगरीज के पिथ से स्यूडोफंक्टर्स उत्पन्न करने के लिए एक नए संरचनात्मक उपकरण (थ्योरम 3.3) की परिभाषा और औपचारिकीकरण, क्योंकि मानक एडजॉन्शन्स आवश्यक तरीके से पिथ तक लिफ्ट नहीं होते हैं।
मैट्रिक्स जैसी गणनाएँ: कोहेरेंस डायग्रामों के सत्यापन को सरल बनाने के लिए मल्टीसेट अंकगणित और "लीनियर" लिस्ट्स का उपयोग। कोहेरेंस जांच को मल्टीसेट्स के गुणों (जहाँ सिमेट्री ग्रुप द्वारा डुप्लिकेट्स को संभाला जाता है) में बदलकर, लेखक जटिल प्रूफ दायित्वों को निपटाने के लिए Lean के ऑटोमेशन टैक्टिक्स (simp, subsingleton) का लाभ उठाते हैं।

4. मुख्य परिणाम (Main Results)

थ्योरम 1.1 (अनबायसिंग): किसी भी सममित मोनॉइडल श्रेणी $\mathcal{C}$ के लिए, परिमित सेटों की स्पैन बाइकेटिगरी के पिथ से $Cat $तक एक स्यूडोफंक्टर मौजूद है जो मनमाने परिमित परिवारों के टेंसर उत्पाद को एनकोड करता है। यह$ \mathcal{C} $को एक लॉवेर सिमेट्रिक मोनॉइडल$ (\infty, 1)$-श्रेणी के रूप में साकार करता है।
थ्योरम 1.3 (कोहेरेंस): एक सेट $J$ पर फ्री सिमेट्रिक मोनॉइडल श्रेणी, सिमेट्रिक लिस्ट्स की श्रेणी (जिसे $Core(Fin/J)$ के रूप में औपचारिक रूप दिया गया है) के तुल्य है।
कोरोलरी 2.9: सिमेट्रिक लिस्ट की श्रेणी में मोर्फिज्म का सटीक लक्षण वर्णन, जो इंडेक्स के बियोजेक्शन (bijections) के रूप में है जो अंतर्निहित तत्वों का सम्मान करते हैं, जिससे बीजगणितीय संरचना और परम्यूटेशन्स के बीच संबंध स्थापित होता है।

5. महत्व (Significance)

मैथलिब (Mathlib): यह कार्य सममित मोनॉइडल श्रेणियों के अनबायसिंग के पहले मशीनीकृत प्रमाण (mechanized proof) के रूप में कार्य करता है। यह Mathlib में उन्नत बीजगणितीय संरचनाओं, जैसे फ्री कम्यूटेटिव मोनॉइड ऑब्जेक्ट्स और सिमेट्रिक टेंसर पावर्स ( $x^{\otimes n}$ ) को औपचारिक रूप देने के लिए आवश्यक आधार तैयार करता है।
हायर कैटेगरी तक सेतु: यह निर्माण शास्त्रीय सममित मोनॉइडल श्रेणियों की परिभाषा को आधुनिक $(\infty, 1)$ -श्रेणीगत परिप्रेक्ष्य (विशेष रूप से क्रैंच के लॉवेर दृष्टिकोण) के साथ संरेखित करता है। यह उच्च श्रेणी सिद्धांत को Mathlib में एकीकृत करने के लिए एक पूर्व शर्त है, क्योंकि यह साधारण श्रेणियों को उनके उच्च-श्रेणीगत समकक्षों के रूप में पुनर्व्याख्या करने की अनुमति देता है।
प्रूफ इंजीनियरिंग: यह पेपर सावधानीपूर्वक डेफिनिशनल इक्वैलिटीज (definitional equalities) का उपयोग करके और कोहेरेंस प्रूफ के लिए subsingleton टैक्टिक का लाभ उठाकर "DTT Hell" (डिपेंडेंट टाइप थ्योरी की कठिनाइयाँ) को संभालने की परिष्कृत तकनीकों का प्रदर्शन करता है। यह जटिल स्यूडो-अलजेब्रिक संरचनाओं को औपचारिक रूप देने के लिए एक ब्लूप्रिंट के रूप में कार्य करता है।

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