کد مقاله کد نشریه سال انتشار مقاله انگلیسی ترجمه فارسی نسخه تمام متن
4661567 1344843 2016 12 صفحه PDF ندارد دانلود رایگان
عنوان انگلیسی مقاله
The intrinsic topology of Martin-Löf universes
ترجمه فارسی عنوان
توپولوژی ذاتی جهان های مارتین ـ لوف
کلمات کلیدی
نظریه نوع مارتین لوف؛ جهان؛ توپولوژی. قضیه رایس
03B15; 03F50; 03C90; 03D65Martin-Löf type theory; Universe; Topology; Rice's Theorem
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

A construction by Hofmann and Streicher gives an interpretation of a type-theoretic universe U in any Grothendieck topos, assuming a Grothendieck universe in set theory. Voevodsky asked what space U is interpreted as in Johnstone's topological topos. We show that its topological reflection is indiscrete. We also offer a model-independent, intrinsic or synthetic, description of the topology of the universe: It is a theorem of type theory that the universe is sequentially indiscrete, in the sense that any sequence of types converges to any desired type, up to equivalence. As a corollary we derive Rice's Theorem for the universe: it cannot have any non-trivial, decidable, extensional property, unless WLPO, the weak limited principle of omniscience, holds.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 167, Issue 9, September 2016, Pages 794–805
نویسندگان
, ,