The internal languages of univalent categories

ملخص تقني: اللغات الداخلية للفئات الموحدة (Univalent Categories)

بيان المشكلة
تؤسس نظريات اللغة الداخلية في المنطق الفئوي (Categorical Logic) تكافؤاً بين القواعد (Syntax - نظريات النوع) والدلالات (Semantics - النماذج الفئوية). وتعد نتيجة كليرامبو وديبير [CD14] نتيجة محورية صححت نظرية سيلي الأصلية [See84]، حيث أثبتت وجود تكافؤ ثنائي (Biequivalence) بين الفئة الثنائية للفئات محلياً مغلقة كارتيزياً (LCCCs) والفئة الثنائية للفئات الديمقراطية ذات العائلات (CwFs) التي تدعم أنواع الهوية الامتدادية (Extensional Identity Types)، وأنواع $\Sigma$، وأنواع $\Pi$.

ومع ذلك، فقد صيغت هذه النتيجة ضمن أسس نظرية المجموعات. وفي الأسس الموحدة (Univalent Foundations - نظرية النوع المتجانس/هوموتوبي)، يواجه المفهوم القياسي لـ CwF عقبة جوهرية: فبديهية الوحدة (Univalence Axiom) تقتضي أن نوع المجموعات ليس مجموعة في حد ذاته (بل هو 1-type). وبناءً عليه، فإن الشرط الذي تفرضه CwFs بأن مجموعة الأنواع في سياق ما يجب أن تكون "مجموعة" (Set) يُنتهك بواسطة فئة المجموعات الموحدة. علاوة على ذلك، فإن التمييز بين البنية "المختارة" (مثل الـ split fibrations) والبنية "الموجودة" (مثل الحدود حتى التماثل/Isomorphism) يخلق مشكلات في التماسك (Coherence) في أسس نظرية المجموعات، مما يستلزم استخدام بديهية الاختيار أو إجراءات التصلب (Strictification). أما في الأسس الموحدة، حيث التماثل يقتضي التطابق، فإن هذه التمايزات تتلاشى، لكن إطار عمل CwFs الحالي لا يمكن تطبيقه مباشرة.

المنهجية
يطور البحث إطاراً جديداً للدلالات الفئوية ضمن الأسس الموحدة، باستخدام الفئات الموحدة (Univalent Categories) وفئات الاستيعاب (Comprehension Categories) بدلاً من CwFs.

1. الفئات الموحدة: يعمل المؤلف على فئات يكون فيها نوع الهوية للكائنات مكافئاً لنوع التماثلات (Adjoint Equivalences). يسمح هذا بمعاملة التماثلات المرافقة كأنها هويات، مما يبسط البراهين المتعلقة بالحفاظ على البنية (مثل الأسس) ويلغي الحاجة إلى بديهية الاختيار لاختيار الحدود.
2. فئات الاستيعاب: لنمذجة الأنواع المعتمدة دون اشتراط أن تشكل الأنواع "مجموعة"، يتبنى البحث فئات استيعاب (تعتمد على الـ fibrations والـ displayed categories). تتكون فئة الاستيعاب من فئة قاعدة للسياقات، وفئة معروضة (Displayed Category) للأنواع، وتقطيع (Cleaving - يوفر عملية الاستبدال)، ودالة استيعاب. ويحصر المؤلف اهتمامه في فئات الاستيعاب الكاملة الموحدة، حيث تكون كل من الفئة القاعدة والفئة المعروضة موحدة.
3. الفئات الثنائية المعروضة (Displayed Bicategories): يعتمد بناء الفئات الثنائية للنماذج بشكل كبير على الفئات الثنائية المعروضة [AFM+21]. يسمح هذا النهج التركيبي ببناء فئات ثنائية معقدة (مثل LCCCs أو التوبوسات مع الأكوان) عبر طبقات من الخصائص (مثل الحدود النهائية، أنواع $\Pi$، الأكوان) فوق فئات ثنائية أساسية أبسط. تسهل هذه الوحدوية (Modularity) إثبات أن الفئات الثنائية الناتجة هي نفسها موحدة.
4. الخصائص المحلية: لتوسيع النتائج من الفئات ذات الحدود النهائية إلى الهياكل الأكثر تعقيداً مثل التوبوسات، يكيف البحث مفهوم الخصائص المحلية لـ "مايتي" [Mai05]. الخاصية المحلية هي شرط على الفئات يكون مغلقاً تحت عملية التقطيع (Slicing). يقوم المؤلف بصياغة ذلك ضمن إطار الفئات الثنائية المعروضة لتوسيع التكافؤات الثنائية من الحالة الأساسية (الحدود النهائية) إلى فئات متنوعة من التوبوسات.
5. إعادة الفهرسة والأكوان: لمعالجة الأكوان، يستخدم البحث إعادة فهرسة الفئات الثنائية المعروضة. تسمح هذه التقنية بنقل التكافؤ الثنائي من فئة أساسية إلى فئة معروضة فوقها، مما يتيح تعريف الأكوان المغلقة تحت صانعات أنواع محددة (مثل $\Sigma$، $\Pi$، الأعداد الطبيعية) دون اشتراط قوانين استقرار صارمة، بل الاستقرار حتى التماثل (الذي يصبح تطابقاً في الفئات الموحدة).

المساهمات الرئيسية
يقدم البحث أربع مساهمات رئيسية:

1. النظرية المناظرة لـ "كليرامبو-ديبير": يبني المؤلف تكافؤاً ثنائياً بين الفئة الثنائية لـ الفئات الموحدة ذات الحدود النهائية والفئة الثنائية لـ فئات الاستيعاب الديمقراطية النهائية (DFL) الموحدة. يثبت هذا أن اللغة الداخلية للفئات الموحدة ذات الحدود النهائية هي نظرية مارتن-لوف للأنواع الامتدادية مع الوحدة، والضرب الثنائي، وأنواع $\Sigma$.
2. التوسيع إلى الفئات محلياً مغلقة كارتيزياً (LCCCs): يتم توسيع التكافؤ الثنائي ليشمل الفئات الموحدة محلياً مغلقة كارتيزياً وفئات الاستيعب (DFL) التي تدعم أنواع $\Pi$. وهذا يؤكد أن اللغة الداخلية لـ LCCCs الموحدة هي نظرية مارتن-لوف للأنواع الامتدادية مع أنواع $\Pi$.
3. التوسيع إلى التوبوسات والأكوان: يتم تعميم المنهج على فئات متنوعة من التوبوسات (Pretoposes، $\Pi$-pretoposes، التوبوسات الأولية، والتوبوسات ذات كائن الأعداد الطبيعية) باستخدام الخصائص المحلية. علاوة على ذلك، يعرّف المؤلف الأكوان في هذه الفئات بحيث تكون مغلقة تحت صانعات الأنواع (الأعداد الطبيعية، مصنف الكائنات الجزئية، تغيير حجم القضايا، أنواع $\Sigma$، وأنواع $\Pi$)، مما يثبت وجود تكافؤ ثنائي للتوبوسات الأولية مع كون.
4. التحقق الصوري (Formalization): تمت صياغة جميع البناءات والبراهين في مساعد الإثبات Rocq باستخدام مكتبة UniMath، مما يضمن الصحة ويوفر مرجعاً يمكن التحقق منه آلياً للنظرية.

النتائج
يثبت البحث أنه بالنسبة لفئات متنوعة من الفئات الموحدة، يوجد تكافؤ ثنائي مع الفئات المقابلة من فئات الاستيعب الموحدة. وتحديداً:

• الحدود النهائية: الفئات الموحدة ذات الحدود النهائية $\simeq$ فئات الاستيعب (DFL) التي تدعم (الوحدة، الضرب، المساوي، $\Sigma$).
• LCCC: الفئات الموحدة محلياً مغلقة كارتيزياً $\simeq$ فئات الاستيعب (DFL) التي تدعم أنواع $\Pi$.
• التوبوسات: التوبوسات الأولية الموحدة (مع أو بدون NNO) $\simeq$ فئات الاستيعب (DFL) ذات الخصائص المحلية المقابلة (مثل مصنفات الكائنات الجزئية، المجموعات المنفصلة، الحصص).
• الأكوان: التوبوسات الأولية الموحدة مع كون مغلق تحت صانعات أنواع محددة $\simeq$ فئات الاستيعب (DFL) مع كون يحقق شروط الإغلاق المقابلة.

يوضح البحث أنه في الأسس الموحدة، اللغة الداخلية لهذه الهياكل الفئوية هي نظرية مارتن-لوف للأنواع الامتدادية. إن استخدام الفئات الموحدة يبسط النظرية عبر إزالة الحاجة إلى الـ split fibrations، كما تُحل مشكلات التماسك التي تعاني منها النماذج القائمة على نظرية المجموعات (حيث يجب أن يكون الاستبدال صارماً) لأن التماثلات تصبح تطابقات.

الأهمية والادعاءات
يزعم البحث أن تطويره يوفر منظوراً جديداً لدلالات نظرية الأنواع المعتمدة. فمن خلال استخدام الفئات الموحدة، يتجنب المؤلف الأعباء التقنية للـ split fibrations وبديهية الاختيار، والتي تعد ضرورية في أسس نظرية المجموعات لضمان الصحة. إن مبادئ هوية البنية المتأصلة في الأسس الموحدة تسمح بمعاملة أكثر طبيعية للهياكل الفئوية حيث تُحدد الكائنات بالتماثل بدلاً من التطابق الصارم.

يصرح المؤلف صراحة بأنه لا يبني القواعد (Syntax) أو النموذج الأولي في هذا العمل؛ بل يركز على الجانب الفئوي من نظرية اللغة الداخلية (التكافؤ بين النماذج). ويشير إلى أنه بينما تعتبر فئات الاستيعاب مناسبة للأسس الموحدة، فإن الهياكل الأخرى مثل CwFs ليست كذلك بسبب قيد "المجموعة" المفروض على الأنواع. يضع البحث نفسه كخطوة تأسيسية، تاركاً تطوير قواعد مناسبة (مثل قواعد الـ groupoid) وتفسيرها كعمل مستقبلي. تكمن الأهمية في إرساء مراسلة متينة ومحققة آلياً بين الهياكل الفئوية الموحدة ونظريات الأنواع، مما يثبت أن الأسس الموحدة تدعم طبيعياً هذه النظريات الداخلية دون العيوب الموجودة في الصياغات السابقة القائمة على نظرية المجموعات.