相关论文: Martin-Lof identity types in the C-systems defined…

We present some first steps in the more general setting of the interpretation of dependent type theory in Ludics. The framework is the following: a (Martin-Lof) type A is represented by a behaviour (which corresponds to a formula) in such a…

Connections between homotopy theory and type theory have recently attracted a lot of attention, with Voevodsky's univalent foundations and the interpretation of Martin-Lof's identity types in Quillen model categories as some of the…

We construct a univalent universe in the sense of Voevodsky in some suitable model categories for homotopy types (obtained from Grothendieck's theory of test categories). In practice, this means for instance that, appart from the homotopy…

A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are…

In this article the author endows the functor category [B(C2),Gpd] with the structure of a type-theoretic fibration category with a universe using the projective fibrations. It offers a new model of Martin-L\"of type theory with dependent…

For Martin-Lof type theory with a hierarchy U(0): U(1): U(2): ... of univalent universes, we show that U(n) is not an n-type. Our construction also solves the problem of finding a type that strictly has some high truncation level without…

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to…

In this article the author endows the functor category [B(Z2),Gpd] with the structure of a type-theoretic fibration category with a univalent universe using the so-called injective model structure. It gives us a new model of Martin-L\"of…

This is a major update of the previous version. The methods of the paper are now fully constructive and the style is "formalization ready" with the emphasis on the possibility of formalization both in type theory and in constructive set…

In Feferman's work, explicit mathematics and theories of generalized inductive definitions play a central role. One objective of this article is to describe the connections with Martin-Lof type theory and constructive Zermelo-Fraenkel set…

This is the fourth in a series of papers extending Martin-L\"of's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type systems supporting a general schema of…

This is the second in a series of papers extending Martin-L\"{o}f's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I,…

A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are…

This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice…

A new approach to the semantics of identity types in intensional Martin-L\"of type theory is proposed, assuming only a category with finite limits and an interval. The specification of \emph{extensional} identity types in the original…

We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes…

This paper presents preliminary work on a general system for integrating dependent types into substructural type systems such as linear logic and linear type theory. Prior work on this front has generally managed to deliver type systems…

In this paper we construct new categorical models for the identity types of Martin-L\"of type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren, which has…

Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based…

We present a construction of W-types in the setoid model of extensional Martin-L\"of type theory using dependent W-types in the underlying intensional theory. More precisely, we prove that the internal category of setoids has initial…