unofficial copies [PDF], [PS]

by Robert L. Constable

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

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.