کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4662955 | 1345214 | 2014 | 17 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
Modeling Martin-Löf type theory in categories
ترجمه فارسی عنوان
مدل سازی نظریه نوع Martin-Löf در دسته بندی ها
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
Grothendieck fibration؛ تئوری نوع Martin-Löf؛ نوع هویت؛ شی مسیر؛ تئوری نوع هومیوپاتی
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
چکیده انگلیسی
We present a model of Martin-Löf type theory that includes both dependent products and the identity type. It is based on the category of small categories, with cloven Grothendieck bifibrations used to model dependent types. The identity type is modeled by a path functor that seems to have independent interest from the point of view of homotopy theory. We briefly describe this modelʼs strengths and limitations.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Applied Logic - Volume 12, Issue 1, March 2014, Pages 28–44
Journal: Journal of Applied Logic - Volume 12, Issue 1, March 2014, Pages 28–44
نویسندگان
François Lamarche,