نظریه نوع هوموتوپی به‌عنوان زبان بنیادی

شرح دقیق مسئله

این پژوهش به توسعه و کاربرد نظریه نوع هوموتوپی (HoTT) به‌عنوان زبانی بنیادی برای ریاضیات می‌پردازد: اهداف پژوهش 1. صورت‌بندی دقیق اصل یکتایی و پیامدهای آن برای معادل‌بودن ایزومورف‌ها 2. توسعه و کاربرد انواع استقرایی بالاتر برای تعریف ساختارهای توپولوژیک 3. بررسی ارتباط میان HoTT و نظریه رسته‌های (∞,1) 4. ساخت مدل‌های سازگار برای HoTT و تحلیل استقلال اصول موضوعه 5. پیاده‌سازی سیستم‌های اثبات خودکار بر پایه HoTT 6. کشف روابط جدید بین هندسه، توپولوژی، و منطق از طریق لنز HoTT 7. بررسی پدیده‌های ریاضی مانند همبندی، هم‌ارزی هوموتوپی و ناوردایی هوموتوپی از دیدگاه نوع‌شناختی اهمیت و کاربرد این پژوهش دارای اهمیت بنیادی و کاربردی است: 1. ارائه بنیانی متحد برای ریاضیات که هم توصیفی و هم محاسباتی باشد 2. از بین بردن شکاف بین ریاضیات “کاغذ و قلمی” و ریاضیات رسمی‌شده کامپیوتری 3. تقویت ارتباط بین نظریه دسته‌ها، توپولوژی و نظریه نوع 4. توسعه سیستم‌های برنامه‌نویسی وابسته به نوع پیشرفته با کاربرد در نرم‌افزارهای مطمئن 5. امکان اثبات خودکار قضایای پیچیده با کمک اثبات‌یارها 6. رفع برخی تناقضات فلسفی در مبانی ریاضیات 7. کاربرد در علوم کامپیوتر نظری، هندسه محاسباتی و هوش مصنوعی منابع مرجع 1. The Univalent Foundations Program. (2013). “Homotopy Type Theory: Univalent Foundations of Mathematics.” Institute for Advanced Study. 2. Awodey, S. (2010). “Type Theory and Homotopy.” In P. Dybjer et al. (Eds.), “Epistemology versus Ontology” (pp. 183-201). Springer. 3. Shulman, M. (2018). “Homotopy Type Theory: A synthetic approach to higher equalities.” In “Categories for the Working Philosopher” (pp. 77-102). Oxford University Press. 4. Coquand, T. (2018). “A survey of constructive presheaf models of univalent type theory.” Math. Proc. Cambridge Philos. Soc. 5. Licata, D. R., & Brunerie, G. (2015). “A Cubical Approach to Synthetic Homotopy Theory.” LICS '15, pp. 92-103. 6. Hottinger, C. (2021). “Cubical Methods in Homotopy Type Theory and Univalent Foundations.” Springer. 7. Rijke, E. (2022). “Introduction to Homotopy Type Theory.” Cambridge University Press. 8. Angiuli, C., Brunerie, G., Coquand, T., Favonia, R. H., Harper, R., & Licata, D. R. (2019). “Cartesian Cubical Computational Type Theory.” Journal of Functional Programming, 31, e22.