Late reply, but telescopes seem to be based on a similar thought:

(http://www.nuprl.org/documents/Constable/Automath-35years.pd...)

RECENT RESULTS IN TYPE THEORY AND THEIR RELATIONSHIP TO AUTOMATH, ROBERT L. CONSTABLE