15 citations · 21 across the 6 of their papers we have counts for
11 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…