1
$\begingroup$

I am wondering if there is any known relationship between these 2 concepts in intensional MLTT as formulated here.

Does $Internal\ parametricity \implies ECT$ hold? For forumlation of ECT see https://en.wikipedia.org/wiki/Church%27s_thesis_(constructive_mathematics), also I am wondering about the internal version of it. In particular the formulation as stated in this paper in the form compatible with univalence axiom.

This question is motivated by the results in Parametricity and excluded middle, which shows that failures of parametricity are related to axioms without computational content such as Law of excluded middle and that ECT also implies failure of Law of excluded middle.

By internal parametricity I mean the internalization of this concept ala A computational interpretation of parametricity.

I am quite sure that the opposite direction, doesn't hold. Let me outline my reasons for this for a function $f:\forall a.a \rightarrow a$, then if internal parametricity fails for this type, $ECT$ might still hold, i.e. if $f$ analyses type of its argument and acts as $\neg$ only for bools and $id$ everywhere else, all functions should still be computable and thus $ECT$ can still be admissible.

$\endgroup$
  • $\begingroup$ Can someone explain to me the reason for the downvote, so I can improve the question? $\endgroup$ – Nift Dec 3 '19 at 10:18
  • 4
    $\begingroup$ I've not voted, but maybe explain what you mean by "extended Church's thesis", since the inattentive reader is probably assuming you mean a variant of the Church-Turing thesis. I guess you are referring to this. Maybe also sketch / give reference for iMLTT and internal parametricity, so that your question looks polished. $\endgroup$ – Martin Berger Dec 3 '19 at 11:10
  • 1
    $\begingroup$ Take care not to mix external and internal versions of ECT. The external one says that every definable function is computable. The internal one says that the statement "all functions are computable" is provable (or that a certain type is inhabited). $\endgroup$ – Andrej Bauer Dec 4 '19 at 9:37
4
$\begingroup$

Internal parametricity does not entail any version of extended Church's thesis. To see this, consider a presheaf model of internal parametricity, for example this one, and observe that in any presheaf model of type theory the extended Church's thesis fails (both the internal and the external one) because the object $\mathbb{N}^\mathbb{N}$ has uncountably many global points.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.