言霊による誤解・違和感・抵抗感

• 命題は型である。← そんなわけないだろ。
• 命題は型の一種である。
• [間違い] 命題はデータ型の一種である。
• 命題とデータ型は違う。が、命題は型の一種である。
• 命題は広義の型の一種である。
• 命題は広義の型の一種であり、データ型も広義の型の一種である。
• 命題は命題の型宇宙に居て、データ型はレベル0の型宇宙に居る。