کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
4662956 | 1345214 | 2014 | 5 صفحه PDF | دانلود رایگان |
عنوان انگلیسی مقاله ISI
A model of type theory in simplicial sets: A brief introduction to Voevodsky's homotopy type theory
ترجمه فارسی عنوان
یک مدل از تئوری نوع در مجموعه های ساده: یک مقدمه کوتاه برای نظریه نوع هموتوپی Voevodsky
دانلود مقاله + سفارش ترجمه
دانلود مقاله ISI انگلیسی
رایگان برای ایرانیان
کلمات کلیدی
تئوری نوع؛ مدل های طبقه بندی شده؛ تئوری Homotopy؛ axiom univalence
موضوعات مرتبط
مهندسی و علوم پایه
ریاضیات
منطق ریاضی
چکیده انگلیسی
We describe how to interpret constructive type theory in the topos of simplicial sets where types appear as Kan complexes and families of types as Kan fibrations. Since Kan complexes may be understood as weak higher-dimensional groupoids this model generalizes and extends the (ordinary) groupoid model which was introduced by M. Hofmann and the author about 20 years ago. Finally, we discuss Voevodsky's Univalence Axiom which has been shown to hold in this model. This axiom roughly states that isomorphic types are equal. The type theoretic notion of isomorphism provided by this model coincides with homotopy equivalence of Kan complexes. For this reason it has become common to refer to it as Homotopy Type Theory.
ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Journal of Applied Logic - Volume 12, Issue 1, March 2014, Pages 45–49
Journal: Journal of Applied Logic - Volume 12, Issue 1, March 2014, Pages 45–49
نویسندگان
T. Streicher,