اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدIdempotents in intensional type theory
189
0
0.0
(
0
)
نشر من قبل
J\\\"urgen Koslowski
تاريخ النشر
2015
مجال البحث
الهندسة المعلوماتية
والبحث باللغة
English
تأليف
Michael Shulman
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We study idempotents in intensional Martin-Lof type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodskys univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct the type of fully coherent idempotents, by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.
قيم البحث
اقرأ أيضاً
We present polygraphic programs, a subclass of Albert Burronis polygraphs, as a computational model, showing how these objects can be seen as first-order functional programs. We prove that the model is Turing complete. We use polygraphic interpretati
ons, a termination proof method introduced by the second author, to characterize polygraphic programs that compute in polynomial time. We conclude with a characterization of polynomial time functions and non-deterministic polynomial time functions.
We describe categorical models of a circuit-based (quantum) functional programming language. We show that enriched categories play a crucial role. Following earlier work on QWire by Paykin et al., we consider both a simple first-order linear language
for circuits, and a more powerful host language, such that the circuit language is embedded inside the host language. Our categorical semantics for the host language is standard, and involves cartesian closed categories and monads. We interpret the circuit language not in an ordinary category, but in a category that is enriched in the host category. We show that this structure is also related to linear/non-linear models. As an extended example, we recall an earlier result that the category of W*-algebras is dcpo-enriched, and we use this model to extend the circuit language with some recursive types.
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theo
ry. This is a brief survey of work by the authors developed in detail elsewhere.
We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive models of univalence, that can then be relativized to any presheaf model
s, and these sheaf models are obtained by localisation for a left exact modality. We provide first an abstract notion of descent data which can be thought of as a higher version of the notion of prenucleus on frames, from which can be generated a nucleus (left exact modality) by transfinite iteration. We then provide several examples.
We define in the setting of homotopy type theory an H-space structure on $mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $mathbb S^3hookrightarrowmathbb S^7twoheadrightarrowmathbb S^4$, using only homotopy invariant tools.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
