Internal Parametricity for Cubical Type Theory

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 call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.

The Scott model of PCF in univalent type theory

We develop the Scott model of the programming language PCF in univalent type theory. Moreover, we work constructively and predicatively. To account for the non-termination in PCF, we use the lifting monad (also known as the partial map classifier monad) from topos theory, which has been extended to univalent type theory by Escardó and Knapp. Our results show that lifting is a viable approach to partiality in univalent type theory. Moreover, we show that the Scott model can be constructed in a predicative and constructive setting. Other approaches to partiality either require some form of choice or quotient inductive-inductive types. We show that one can do without these extensions.

Cubical Agda: A dependently typed programming language with univalence and higher inductive types

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 (HITs). 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 HITs. These new primitives allow the direct definition of function and propositional extensionality as well as quotient types, all with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. The adoption of cubical type theory extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.

Indexed type theories

In this paper, we define indexed type theories which are related to indexed (∞-)categories in the same way as (homotopy) type theories are related to (∞-)categories. We define several standard constructions for such theories including finite (co)limits, arbitrary (co)products, exponents, object classifiers, and orthogonal factorization systems. We also prove that these constructions are equivalent to their type theoretic counterparts such as Σ-types, unit types, identity types, finite higher inductive types, Π-types, univalent universes, and higher modalities.

Constructing Infinitary Quotient-Inductive Types

This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel’s size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.