Skip to main content
PRL Project

Recent Results in Type Theory and Their Relationship to Automath

by Robert L. Constable

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

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