Agdaメーリングリストの“If all functions (N->N)->N are continuous, then 0=1” https://lists.chalmers.se/pipermail/agda/2013/006064.html という話が面白い。ここで言っているcontinuityは、関数 N→N を a0, a1, … という自然数の無限列と考えた時に、関数 f: (N→N)→N はその引数の有限のprefixにしか依存しないという、Brouwerの直観主義数学に端を発する公理。 計算的な世界ではすごく自然なんだけれど、この公理をMartin-Löf型理論で形式化すると矛盾を導く。 原因は（よくあるパターンだけれども）Σが∃よりも強いことで、なら¬¬Σを使えばとも思うのだけれど、それは今度はどうも弱すぎるらしい。
[Agda] If all functions (N->N)->N are continuous, then 0=1.
https://lists.chalmers.se/pipermail/agda/2013/006064.html