4 ms·
Late reply, but telescopes seem to be based on a similar thought: (http://www.nuprl.org/documents/Constable/Automath-35years.pdf http://www.nuprl.org/documents
by mafm 8y ago
Late reply, but telescopes seem to be based on a similar thought:
(http://www.nuprl.org/documents/Constable/Automath-35years.pdf http://www.nuprl.org/documents/Constable/Automath-35years.pd...)
RECENT RESULTS IN TYPE THEORY AND THEIR RELATIONSHIP TO AUTOMATH, ROBERT L. CONSTABLE