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.