إزالة التكرار في المجموعات الناتجة في نظرية الأنماط الهوماسية

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