اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدModels of Type Theory Based on Moore Paths
92
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
This paper introduces a new family of models of intensional Martin-Lof type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a notion of Moore path. By considering a particular gros topos, we show that there is such a model that is non-truncated, i.e. contains non-trivial structure at all dimensions. In other words, in this model a type in a nested sequence of identity types can contain more than one element, no matter how great the degree of nesting. Although inspired by existing non-truncated models of type theory based on simplicial and cubical sets, the notion of model presented here is notable for avoiding any form of Kan filling condition in the semantics of types.
قيم البحث
اقرأ أيضاً
We begin by recalling the essentially global character of universes in various models of homotopy type theory, which prevents a straightforward axiomatization of their properties using the internal language of the presheaf toposes from which these mo
del are constructed. We get around this problem by extending the internal language with a modal operator for expressing properties of global elements. In this setting we show how to construct a universe that classifies the Cohen-Coquand-Huber-Mortberg (CCHM) notion of fibration from their cubical sets model, starting from the assumption that the interval is tiny - a property that the interval in cubical sets does indeed have. This leads to an elementary axiomatization of that and related models of homotopy type theory within what we call crisp type theory.
In this paper, we make a substantial step towards an encoding of Cubical Type Theory (CTT) in the Dedukti logical framework. Type-checking CTT expressions features a decision procedure in a de Morgan algebra that so far could not be expressed by the
rewrite rules of Dedukti. As an alternative, 2 Layer Type Theories are variants of Martin-Lof Type Theory where all or part of the definitional equality can be represented in terms of a so-called external equality. We propose to split the encoding by giving an encoding of 2 Layer Type Theories (2LTT) in Dedukti, and a partial encoding of CTT in 2LTT.
We exhibit a computational type theory which combines the higher-dimensional structure of cartesian cubical type theory with the internal parametricity primitives of parametric type theory, drawing out the similarities and distinctions between the tw
o along the way. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic types, including functions between higher inductive types, and we show by example how relativity can be used to characterize the relational interpretation of inductive types.
Nakanos later modality can be used to specify and define recursive functions which are causal or synchronous; in concert with a notion of clock variable, it is possible to also capture the broader class of productive (co)programs. Until now, it has b
een difficult to combine these constructs with dependent types in a way that preserves the operational meaning of type theory and admits a hierarchy of universes. We present an operational account of guarded dependent type theory with clocks called Guarded Computational Type Theory, featuring a novel clock intersection connective that enjoys the clock irrelevance principle, as well as a predicative hierarchy of universes which does not require any indexing in clock contexts. Guarded Computational Type Theory is simultaneously a programming language with a rich specification logic, as well as a computational metalanguage that can be used to develop semantics of other languages and logics.
This paper improves the treatment of equality in guarded dependent type theory (GDTT), by combining it with cubical type theory (CTT). GDTT is an extensional type theory with guarded recursive types, which are useful for building models of program lo
gics, and for programming and reasoning with coinductive types. We wish to implement GDTT with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. CTT is a variation of Martin-Lof type theory in which the identity type is replaced by abstract paths between terms. CTT provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory (GCTT), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of CTT as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that CTT can be given semantics in presheaves on the product of the cube category and a small category with an initial object. We then show that the category of presheaves on the product of the cube category and omega provides semantics for GCTT.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
