27 citations · 102 across the 13 of their papers we have counts for
13 papers
Setoids in Intensional Type Theory
Andrew M. Pitts
We show that a certain notion of displayed setoid (family of setoids) in intensional type theory can be used to give a semantics for extensional type theory with universes (ETU). S…
Well-Scoped Locally Nameless Representation of Syntax
Andrew M. Pitts
When using interactive theorem provers based on dependent type theory to define and reason about languages involving binding constructs, we advocate the use of a well-scoped versio…
Constructing Initial Algebras Using Inflationary Iteration
Andrew M. Pitts, S. C. Steenkamp
An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new vers…
Quotients, inductive types, and quotient inductive types
Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp
This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for ind…
Constructing Infinitary Quotient-Inductive Types
Marcelo Fiore, Andrew M. Pitts, S. C. Steenkamp
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 infinitar…
Typal Heterogeneous Equality Types
Andrew M. Pitts
The usual homogeneous form of equality type in Martin-Löf Type Theory contains identifications between elements of the same type. By contrast, the heterogeneous form of equality co…
Modal Dependent Type Theory and Dependent Right Adjoints
Lars Birkedal, Ranald Clouston, Bassel Mannaa +3
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked typ…
Models of Type Theory Based on Moore Paths
Ian Orton, Andrew M. Pitts
This paper introduces a new family of models of intensional Martin-Löf type theory. We use constructive ordered algebra in toposes. Identity types in the models are given by a noti…
Internal Universes in Models of Homotopy Type Theory
Daniel R. Licata, Ian Orton, Andrew M. Pitts +1
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 u…
Decomposing the Univalence Axiom
Ian Orton, Andrew M. Pitts
This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first p…
Axioms for Modelling Cubical Type Theory in a Topos
Ian Orton, Andrew M. Pitts
The homotopical approach to intensional type theory views proofs of equality as paths. We explore what is required of an object in a topos to give such a path-based model of ty…
An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets
Andrew M. Pitts
Staton has shown that there is an equivalence between the category of presheaves on (the opposite of) finite sets and partial bijections and the category of nominal restriction set…
Generative Unbinding of Names
Andrew M. Pitts, Mark R. Shinwell
This paper is concerned with the form of typed name binding used by the FreshML family of languages. Its characteristic feature is that a name binding is represented by an abstract…