The Dependent Calculus of Indistinguishability (DCOI) uses dependency tracking to identify irrelevant arguments and uses indistinguishability during type conversion to enable proof irrelevance, supporting run-time and compile-time irrelevance with the same uniform mechanism. DCOI also internalizes reasoning about indistinguishability through the use of a propositional equality type indexed by an observer level. As DCOI is a pure type system, prior work establishes only its syntactic type safety, justifying its use as the basis for a programming language with dependent types. However, it was not clear whether any instance of this system would be suitable for use as a type theory for theorem proving. Here, we identify a suitable instance DCOI ω , which has an infinite predicative universe hierarchy. We show that DCOI ω is logically consistent, normalizing, and that type conversion is decidable. We have mechanized all results using the Coq proof assistant.

A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type axiom. In this work, we argue that a universe hierarchy is not the only option for universes in type theory. Taking inspiration from Leivant’s Stratified System F, we introduce Stratified Type Theory (), where rather than stratifying universes by levels, we stratify typing judgements and restrict the domain of dependent functions to strictly lower levels. Even with type-in-type, this restriction suffices to enforce consistency. In , we consider a number of extensions beyond just stratified dependent functions. First, the subsystem employs McBride’s crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where global definitions with concrete levels can be displaced uniformly to any higher level. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full includes a separate nondependent function type with a floating domain whose level matches that of the overall function type. Finally, we have implemented a prototype type checker for extended with datatypes and inference for level and displacement annotations, along with a small core library. We have proven to be consistent and to be type safe, but consistency of the full remains an open problem, largely due to the interaction between floating functions and cumulativity of judgements. Nevertheless, we believe to be consistent, and as evidence have verified the ill-typedness of some well-known type-theoretic paradoxes using our implementation.

In type systems with dependency tracking, programmers can assign an ordered set of levels to computations and prevent information flow from high-level computations to the low-level ones. The key notion in such systems is indistinguishability : a definition of program equivalence that takes into account the parts of the program that an observer may depend on. In this paper, we investigate the use of dependency tracking in the context of dependently-typed languages. We present the Dependent Calculus of Indistinguishability (DCOI), a system that adopts indistinguishability as the definition of equality used by the type checker. DCOI also internalizes that relation as an observer-indexed propositional equality type, so that programmers may reason about indistinguishability within the language. Our design generalizes and extends prior systems that combine dependency tracking with dependent types and is the first to support conversion and propositional equality at arbitrary observer levels. We have proven type soundness and noninterference theorems for DCOI and have developed a prototype implementation of its type checker.

We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.

Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.

We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky’s univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.