大変眠いので、入手文献名を記すのみに止めます。 Jan Smith “An Interpretation of Martin-Löf's Type Theory in a Type-Free Theory of Propositions,” in: The Journal of Symbolic Logic, vol. 49, no. 3, 1984 おやすみなさい。