Last year Bob Harper wrote a blog post about the failure of "Church's Law" in Extensional Type Theory[1]. However his statement of the law looks to me more like an internal version of the statement "all functions are computable" and I am not surprised that this turns out to be false.

To falsify the law I would have imagined that it would be necessary to set up two general internal models of computation, both of which we believe cannot be extended further whilst retaining their "algorithmic" character, and then proceed to show, internally, that these models of computation are distinct.

Is the issue here just two different interpretations of what "Church's Law" should mean internally, or is there really something deeper going on that I don't understand?

[1] http://existentialtype.wordpress.com/2012/08/09/churchs-law/