На самом деле, подход CoC более выразителен - он допускает произвольную непредсказуемую количественную оценку. Например, тип ∀ а .а → аМожно создать экземпляр a \ to a для себя ( ∀ а .a → a ) → ( ∀ a .а → а ) , что невозможно при иерархии юниверсов.
Причина, по которой он не используется широко, заключается в том, что непредсказуемое количественное определение несовместимо с классической логикой. Если у вас это есть, вы не можете дать модель теории типов, в которой типы интерпретируются как множества наивным способом - см. Знаменитую статью Джона Рейнольдса « Неимметричный по множеству» .
Поскольку многие люди хотят использовать теорию типов как способ проверки обычных математических доказательств, они, как правило, не испытывают энтузиазма по поводу теоретико-типичных особенностей, которые несовместимы с обычными основами. На самом деле, Coq изначально поддерживала непредсказуемость, но они неуклонно отказывались от нее.