# * A Type Theory with Partial Equivalence Relations as Types *

## by Abhishek Anand, Mark Bickford, Robert L. Constable, Vincent Rahli

2014

Presented at TYPES 2014: Types for Proofs and Programs, in Paris, France.

**Abstract**

A small core type language with intersection types in which a partial equivalence relation on closed terms is a type is enough to build the non-inductive types of Nuprl, including the types of dependent functions and partial functions. Using induction on natural numbers and intersection types, we build coinductive types; and using partial functions and coinductive types we build algebraic datatypes.