¿Cuál es la forma de inconsistencia de la paradoja de Girard en la teoría de tipos de Martin Lof?

Question

Soy consciente de que asignar el tipo de Tipo a Tipo (en lugar de estratificar a una jerarquía de tipos) conduce a una inconsistencia. Pero, ¿permite esta inconsistencia la construcción de un término bien tipificado sin una forma normal, o realmente permite una prueba de Falso? ¿Son estas dos preguntas equivalentes?

Answer 1

Conduce a un término bien tipificado, que no tiene forma normal, al que se le asigna el tipo Falso. Puede encontrar el término dado explícitamente en Una simplificación de la paradoja de Girard