Пример ложного предложения при допущении Тип: Тип

В теории типов, если кто-то позволяет типу быть членом самого себя, это делает теорию несостоятельной. Я понимаю это по аналогии с парадоксом Рассела в теории множеств, но предпочел бы, чтобы это было сделано в теории типов. Есть короткий пример аналога в теории типов?

Соответствующая литература следующая:

Тьерри Кокванд Новый парадокс в теории типов (ссылка) . Он описывает свой парадокс в системе, которая несколько слабее, чем

Type : Type

Но это можно легко перенести на вышесказанное. Основная идея заключается в доказательстве Рейнольдса того, что в теории множеств не существует моделей системы F. Это происходит путем построения начальной алгебры вида:

$$A\simeq (A \rightarrow \mathrm{2}) \rightarrow \mathrm{2}$$

Где - это множество из 2 элементов, получающее противоречие с помощью аргумента мощности. Coquand показывает$\mathrm{2}$

1. Вы можете провести это рассуждение в приведенной выше теории типов
2. В этой теории есть модель системы F. Это приводит к противоречию.

Вторая статья написана Антониусом Хюркенсом и озаглавлена «Упрощение парадокса Жирара» (ссылка) . Доказательство включает построение «типа всех обоснованных типов». Я должен признать, что общая идея кажется ясной, но детали довольно дьявольские.

Боюсь, что в нет простого, легко понятного противоречия . Однако полученные из противоречия контрольные термины относительно просты: для их определения достаточно нескольких строк.$\mathrm{Type} : \mathrm{Type}$

Александр Микель в своей дипломной работе показал, что можно построить модель наивной теории множеств в этих несовместных системах типов, используя точечную графовую интерпретацию множеств. Затем он может просто применить парадокс Рассела напрямую. К сожалению, построение модели требует немного работы, и диссертация на французском языке.