@mevenlennonbertrand@lipn.info
Post #1846831
2026-04-28 06:28 UTC
@jonmsterling @jpoiret @carloangiuli Church Thesis, for synthetic computability theory. This is by now a well-installed topic, if maybe a bit niche, and imho a much more elegant way to formalise computability theory that all the other alternatives.
Now I'm not saying that you should abandon funext in your standard mathematical life just to stay compatible with CT. But there is at least one non-hypothetical application for negating it.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-28 06:33
@mevenlennonbertrand @jpoiret @carloangiuli But church’s thesis is, if stated correctly, obviously compatible with funext. So I would say this example is a non example. This is not a “non-hypothetical application” but rather a “hypothetical non-application”. Church’s thesis holds in the Effective Topos. There are also other interesting words where versions of church’s thesis holds. All of them are models of ETT or HoTT, depending on how you set things up. Church’s thesis is actually a fantastic motivation for the use of function extensionality.