几天前在Reddit Haskell上看到的评论：
A tautology is a tautology, is a tautology.
But: A tautology is a tautology, is a tautology, is not a tautology. More of an observation. And: “A tautology is a tautology, is a tautology, is not a tautology. More of an observation.” is also an observation. Which in turn is an observation.
“重言式是重言式”是个重言式。
“‘重言式是重言式’是个重言式”，不是重言式，是个观察。
上面那一句也是个观察…这样继续去都是观察。
后面还有人说这是Homotopy Type Theory的基础，也有人说 Intuitionistic Type Theory就够了～～