Ответ 1
В Coq все имеет тип. Type не является исключением: если вы спросите Coq с помощью команды Check, он скажет вам, что его тип... Type!
Собственно, это немного ложь. Если вы запросите более подробную информацию, выпустив директиву Set Printing Universes., Coq сообщит вам, что Type не совпадает с первым, а "более крупным". Формально каждый Type имеет связанный с ним индекс, называемый его уровнем юниверса. Этот индекс не отображается при печати выражений обычно. Таким образом, правильный ответ на этот вопрос состоит в том, что Type_i имеет тип Type_j для любого индекса j > i. Это необходимо для обеспечения согласованности теории Кок: если бы существовало только одно Type, можно было бы показать противоречие, как и в случае теории противоречия в теории множеств, если предположить, что существует множество всех множеств.
Чтобы упростить работу с индексами типа, Coq дает вам некоторую гибкость: ни один тип не имеет фиксированного индекса, связанного с ним. Вместо этого Coq генерирует одну новую индексную переменную каждый раз, когда вы пишете Type, и отслеживает внутренние ограничения, чтобы гарантировать, что они могут быть созданы с конкретными значениями, которые удовлетворяют ограничениям, требуемым теорией.
Сообщение об ошибке, которое вы видели, означает, что решатель ограничений Coq для уровней юниверсов говорит, что не может быть решения для системы ограничений, которую вы просили. Проблема в том, что forall в определении nat определяется количественно над Type_i, но логика Coq вынуждает nat быть самим типом Type_j, с j > i. С другой стороны, для приложения n nat требуется j <= i, что приводит к невыполнимому набору ограничений индекса.