# * Recent Results in Type Theory and Their Relationship to Automath *

## by Robert L. Constable

2003

Thirty Five Years of Automating Mathematics, F. Kamareddine (ed.), pp. 1-11, Kluwer Academic Press

**Abstract**

The notion of a *telescope* is basic to Automath's theory structure; telescopes provide the context for theorems. A *dependent record type* is an internal version of a telescope and is used in Nuprl to define theories. This paper shows how A. Kopylov defines these record types in terms of *dependent intersections*, a new type constructor.

*Definitional equality* and *book equality* are fundamental concepts basic to Automath. In computational type theories these concepts appear in a different form, as computational equalities and as *quotient types*. Questions about these concepts have led to interesting discoveries about types and open problems. This paper presents a new formulation of quotient types by A. Nogin, and an open question about them.

**bibTex ref: Con03**

cite link