Исправление quasimoto, 27.06.13 18:36 (текущая версия) :
https://en.wikipedia.org/wiki/Intuitionistic_type_theory#.CE.A3-types
Исходная версия quasimoto, 27.06.13 18:36:
Ссылка выше.