Polynomial Universes in Homotopy Type Theory

إليك ملخص تقني مفصل للورقة البحثية بعنوان "الأكوان متعددة الحدود في نظرية النوع المتصلة هوموتوبياً" (Polynomial Universes in Homotopy Type Theory) للباحثين سي. بي. أبيرلي وديفيد آي. سبيفاك.

1. بيان المشكلة

تتناول الورقة توتراً جوهرياً في الدلالات الفئوية لـ نظرية النوع المعتمدة (DTT): الصراع بين الصرامة (Strictness) والتماثل (Isomorphism).

• المشكلة: في الدلالات الفئوية القياسية (مثل فئات الـ presheaf)، تُنمذج العمليات النوعية مثل "التعويض" (substitution) باستخدام الـ pullbacks. ومع ذلك، فإن الـ pullbacks تحقق شرط بيك-تشيفالي (Beck-Chevalley) والارتباط (associativity) "حتى التماثل" فقط، بينما تتطلب بنية (DTT) أن تكون هذه العمليات صارمة في ارتباطها وتحقق هذه الشروط بشكل صارم.
• المقاربات السابقة: قدم أوودي ونيوستيد النماذج الطبيعية (Natural Models) لحل هذه المعضلة. وقد أظهرا أن "الكون" (نوع من الأنواع) يمكن نمذجته كدالة متعددة الحدود (polynomial endofunctor). ولكن، لاستيعاب التماسك عالي الأبعاد المطلوب لهذه النماذج (حيث تتحقق الهويات حتى التماثل وليس صرامة)، استلزم عملهما الانتقال خارج فئة الدوال متعددة الحدود العادية إلى ثلاثية فئات (tricategory) معقدة من الدوال متعددة الحدود.
• الفجوة: لم تكن هناك طريقة لأكسنة هذه النماذج الطبيعية بالكامل داخل الفئة العادية للدوال متعددة الحدود مع التعامل مع التماسك عالي الأبعاد اللازم، مما أدى إلى مأزق "الصرامة مقابل الهوية الضعيفة".

2. المنهجية

حل المؤلفان هذا المأزق عبر نقل الإطار التأسيسي من الـ 1-topoi (مثل المجموعات أو الـ presheaves) إلى نظرية النوع المتصلة هوموتوبياً (HoTT).

• الإطار التركيبي (Synthetic Setting): يعمل المؤلفان داخلياً ضمن لغة (Hoft) (تحديداً $\infty$-topoi)، حيث تكون الهياكل عالية الأبعاد والتماسك (coherences) متأصلة في المنطق. يسمح هذا بالبقاء داخل الفئة العادية للدوال متعددة الحدود ($\mathbf{Poly}$) مع التعبير عن التماسك عالي الأبعاد بشكل طبيعي.
• الدوال متعددة الحدود كأنواع: يمثلان كون النموذج الطبيعي $U$ كدالة متعددة الحدود $P_u$. وتُمثل الأنواع في السياق كعدسات (lenses) (مورفزمات في $\mathbf{Poly}$) داخل هذه الدالة.
• بديهية عدم التباين (Univalence Axiom): الآلية الجوهرية لتبسيط النظرية هي بديهية عدم التباين. فقد عرّفا الكون متعدد الحدود (Polynomial Universe) كدالة متعددة حدود تكون غير متباينة (univalent) (أي كائن تحت-طرفي في فئة العدسات الكارتيزية Cartesian lenses).
  • تعريف: يكون متعدد الحدود $u$ غير متباين إذا كان نوع العدسات الكارتيزية $p \to u$ لأي متعدد حدود $p$ آخر هو "مجرد قضية" (mere proposition) (أي أن أي عدستين من هذا النوع متساويتان).
  • الاستلتاج: يعني عدم التباين أن جميع مخططات العدسات الكارتيزية في $u$ تتبادل تلقائياً، وأن جميع خلايا التماسك العليا تتبادل أيضاً، دون الحاجة لتحديد بيانات تماسك لانهائية بشكل صريح.

3. المساهمات الرئيسية

أ. الأكسنة داخل $\mathbf{Poly}$

تثبت الورقة أن الدلالات الفئوية الكاملة لـ (DTT) (بما في ذلك أنواع $\Sigma$ و $\Pi$) يمكن أكسنتها بالكامل داخل فئة الدوال متعددة الحدود، بشرط أن يكون الكون غير متباين. وهذا يلغي الحاجة إلى ثلاثيات الفئات المعقدة المستخدمة في الأعمال السابقة.

ب. توصيف مولدات النوع (Type Formers)

يُوصّف المؤلفان انغلاق الكون متعدد الحدود تحت مولدات النوع عبر مورفزمات محددة في $\mathbf{Poly}$:

1. أنواع $\Sigma$ (الجموع المعتمدة): تقابل وجود عدسة كارتيزية $\mu: u \circ u \to u$ (حيث $\circ$ هي تركيب الدوال متعددة الحدود). وهذا يجعل $u$ شبه موناد كارتيزي (Cartesian pseudomonad).
2. أنواع $\Pi$ (المنتجات المعتمدة): تقابل وجود عدسة كارتيزية $\pi: u \uparrow u \to u$، حيث $\uparrow$ هو دالة محددة للتعامل مع الدوال المعتمدة.
3. أنواع الوحدة (Unit Types): تقابل وجود عدسة كارتيزية $\eta: y \to u$ (حيث $y$ هي دالة الوحدة المتطابقة).

ج. القانون التوزيعي للمونادات

الاختراق النظري الكبير هو الربط بين أنواع $\Pi$ والقوانين التوزيعية للمونادات (distributive laws of monads).

• تثبت الورقة أنه إذا كان الكون متعدد الحدود غير المتباين $u$ مغلقاً تحت أنواع $\Pi$، فإنه يستحث قانوناً توزيعياً للموناد $u$ على نفسه.
• تحديداً، المورفيزم $\pi: u \uparrow u \to u$ يترجم إلى قانون توزيع $\lambda: u \circ u \to u \circ u$.
• يشهد هذا القانون التوزيعي النمطي للمنتجات المعتمدة على الجموع المعتمدة:
  $$\Pi x:A. \Sigma y:B[x]. C[x,y] \simeq \Sigma f:\Pi x:A. B[x]. \Pi x:A. C[x, f(x)]$$
• والأهم من ذلك، أن بديهية عدم التباين تضمن أن مخططات التماسك المعقدة المطلوبة لقانون توزيع (والتي تتطلب عادةً بيانات لانهائية في نظرية الفئات العليا) تتبادل تلقائياً لأن المورفزمات ذات الصلة هي كارتيزية وتنتهي في كائن غير متباين.

د. الصياغة الرسمية (Formalization)

قام المؤلفون بصياغة النتائج الرئيسية، بما في ذلك تعريفات الدوال متعددة الحدود، والعدسات، وعدم التباين، وبراهين القوانين التوزيعية، في لغة Agda. وهذا يوفر تحققاً مدققاً آلياً للنظرية.

4. النتائج والأمثلة

• مبرهنة 4.1: إذا كان $u$ كون متعدد الحدود غير متباين يمتلك بنية لأنواع الوحدة و$\Sigma$، فإن المخططات التي تُعرف الموناد (قوانين الارتباط والوحدة) تتبادل تلقائياً.
• مبرهنة 4.2: إذا كان $u$ كون متعدد الحدود غير متباين يمتلك بنية لأنواع الوحدة، و$\Sigma$، و$\Pi$، فإن المخططات التي تُعرف قانوناً توزيعياً للموناد $u$ على نفسه تتبادل تلقائياً.
• الجزئية ذات الصلة بالبرهان (Proof-Relevant Partiality): توضح الورقة أن "موناد الجزئية" (الذي ينمذج الدوال الجزئية) ينشأ طبيعياً من كون غير متباين للقضايا (propositions).
• إكمال ريزك (Rezk Completion) والمجموعات المنتهية:
  • طبق المؤلفون إكمال ريزك (مفهوم من نظرية الفئات في Hoft) على موناد القائمة (List monad).
  • موناد القائمة القياسي ليس غير متباين (يفتقر إلى البنية الهوموتوبية الصحيحة للمجموعات المنتهية).
  • إكماله ريزك، Rezk(List)، يقابل كون مجموعات بيشوب المنتهية (Bishop finite sets).
  • النتيجة: بينما لا يحقق موناد القائمة القياسي المعادلات الصارمة لقانون توزيع (بسبب قيود المجموعات أحادية البعد)، فإن Rezk(List) يحقق بالفعل قانون توزيع ذاتي. وهذا يعني أن Rezk(List) هو نظير عالي الفئة للموناد التبادلي الحر، وأن تركيبه مع نفسه يشكل نظيراً عالي الفئة لموناد الحلقات التبادلية الحرة.

5. الأهمية

1. تبسيط الدلالات: تحل الورقة "مشكلة الصرامة" في دلالات (DTT) عبر إظهار أن عدم التباين يعمل كـ "محرك للتماسك". فهو يسمح للرياضيين بالعمل مع الفئة المألوفة للدوال متعددة الحدود مع استيفاء جميع شروط التماسك عالية الأبعاد ضمنياً.
2. توحيد المفاهيم: توحد الورقة مفاهيم النماذج الطبيعية، والدوال متعددة الحدود، والقوانين التوزيعية تحت مظلة (Hoft). وتكشف أن وجود أنواع $\Pi$ يكافئ بنيوياً وجود قانون توزيع للموناد المرتبط بها.
3. البنى الجبرية الجديدة: تشير الورقة إلى بنى جبرية جديدة في نظرية الفئات العليا. فعلى سبيل المثال، تحديد Rezk(List) كموناد متعدد الحدود ذي قانون توزيع ذاتي يفتح الباب لدراسة "الحلقات متعددة الحدود" في سياق الفئات العليا ($\infty$-categories)، وهي تختلف عن البناءات الكلاسيكية في نظرية المجموعات.
4. التحقق الرسمي: من خلال تقديم صياغة كاملة في Agda، تضع الورقة معياراً جديداً للدقة في التقاطع بين نظرية الفئات ونظرية النوع، مما يضمن أن حجج التماسك المعقدة تصمد أمام التحقق الآلي.

باختصار، يثبت أبيرلي وسبياك أن نظرية النوع المتصلة هوموتوبياً (Hoft) توفر البيئة التركيبية المثالية لتعريف الأكوان متعددة الحدود، حيث تعمل بديهية عدم التباين تلقائياً على فرض قوانين التماسك الصارمة المطلوبة لنظرية النوع المعتمدة، مما يبسط الدلالات الفئوية ويكشف عن روابط عميقة بين مولدات النوع والقوانين التوزيعية المونادية.