Related papers: Yet another cubical type theory, but via a semanti…

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…

This paper proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the…

This paper presents a type theory in which it is possible to directly manipulate $n$-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways…

We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we…

The category of Cartesian cubical sets is introduced and endowed with a Quillen model structure using ideas coming from recent constructions of cubical systems of univalent type theory.

We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-L\"{o}f type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory:…

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…

We construct a model of type theory enjoying parametricity from an arbitrary one. A type in the new model is a semi-cubical type in the old one, illustrating the correspondence between parametricity and cubes. Our construction works not…

The goal of this article is to emphasize the role of cubical sets in enriched categories theory and infinity-categories theory. We show in particular that categories enriched in cubical sets provide a convenient way to describe many…

Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly…

We define a variety of notions of cubical sets, based on sites organized using substructural algebraic theories presenting PRO(P)s or Lawvere theories. We prove that all our sites are test categories in the sense of Grothendieck, meaning…

Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of constructive type theory with axioms governing…

This article is the first in a series of articles that explain the formalization of a constructive model of cubical type theory in Nuprl. In this document we discuss only the parts of the formalization that do not depend on the choice of…

This note informally describes a way to build certain cubical n-categories by iterating a process of taking models of certain finite limits theories. We base this discussion on a construction of "double bicategories" as bicategories…

The singular cubical homology theory for the category of quivers or digraphs can be constructed similarly to the classical singular homology theory for topological spaces. The case of digraphs and quivers differs from the topological case…

We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection…

We provide a treatment of isomorphism within a set-theoretic formulation of dependent type theory. Type expressions are assigned their natural set-theoretic compositional meaning. Types are divided into small and large types --- sets and…

This paper gives a uniform-theoretic refinement of classical homotopy theory. Both cubical sets (with connections) and uniform spaces admit classes of weak equivalences, special cases of classical weak equivalences, appropriate for 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…

We propose applying the categorical compositional scheme of [6] to conceptual space models of cognition. In order to do this we introduce the category of convex relations as a new setting for categorical compositional semantics, emphasizing…