Post #1846832
2026-04-28 06:33 UTC
@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.
Replies (1)
-
@mevenlennonbertrand@lipn.info 2026-04-28 06:39
@jonmsterling @jpoiret @carloangiuli Whoop my bad I got mixed up. Indeed the "reasonable' version you need for synthetic computability is compatible. A quoting operation properly integrated in the type theory is a pretty funny thing, and that one contradicts funext, but it's arguably even more niche than CT.