RECENT RESULTS IN TYPE THEORY AND THEIR RELATIONSHIP TO AUTOMATH

unofficial copies [PDF]

by Robert L. Constable

Published: Fairouz Kamareddine (eds.),
Thirty Five Years of Automating Mathematics 1–11.
© 2003, Kluwer Academic Publishers. Printed in the Netherlands.

About

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.