Martin-Lofの 理論とそのパラドックス - あいまいな本日の私 blogMartin-Lofの1971年の論文では、循環性がその中核を占めています。彼は、この条件があるので、彼の理論は圏論と非常に相性が良い（ご存知のように、圏論では、圏全体は圏をなし、その意味で強い循環性を持ちます）と主張しています。しかし、翌年に、Girardがこの中核部分の（もしくは現代の書き方では Type: type）からパラドックス（ブラリ-フォルティのパラドックスの一般化）が導けることを証明し、彼の夢は消えました。現在では、循環的部分を削除した、厳格な可述性に基づく依存型理論（おそらく整合的だろうと思われるもの）が、Martin-Lofの体系ということになっています。 さて、Girardのパラドックスですが、文献は Girardの論文は仏文？だったはずなので、Thierry Coquandの An Analysis of Girard's Paradox (LICS 1986)をど
