<p>Internal parametricity does not entail any version of extended Church's thesis. To see this, consider a presheaf model of internal parametricity, for example <a href="http://publications.lib.chalmers.se/records/fulltext/230735/local_230735.pdf" rel="noreferrer">this one</a>, 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 <span class="math-container">$\mathbb{N}^\mathbb{N}$</span> has uncountably many global points.</p>

CC BY-SA 4.0
2019-12-05T17:03:24.403Z
2019-12-05T17:03:24.403Z
Andrej Bauer
<p>I am wondering if there is any known relationship between these 2 concepts in intensional MLTT as formulated <a href="https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory" rel="nofollow noreferrer">here</a>.</p>

<p>Does <span class="math-container">$Internal\ parametricity \implies ECT$</span> hold?
For forumlation of ECT see <a href="https://en.wikipedia.org/wiki/Church%27s_thesis_(constructive_mathematics)" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Church%27s_thesis_(constructive_mathematics)</a>, also I am wondering about the internal version of it. In particular the formulation as stated in <a href="https://arxiv.org/pdf/1905.03014.pdf" rel="nofollow noreferrer">this paper</a> in the form compatible with univalence axiom.</p>

<p>This question is motivated by the results in <a href="https://www.cs.bham.ac.uk/~abb538/papers/2016-02-parametricity.pdf" rel="nofollow noreferrer">Parametricity and excluded middle</a>, 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.</p>

<p>By internal parametricity I mean the internalization of this concept ala <a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.908.7845&amp;rep=rep1&amp;type=pdf" rel="nofollow noreferrer">A computational interpretation of parametricity</a>.</p>

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

CC BY-SA 4.0
2019-12-03T10:18:43.317Z
Can someone explain to me the reason for the downvote, so I can improve the question?
Ilk
CC BY-SA 4.0
2019-12-03T11:10:48.163Z
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](https://en.wikipedia.org/wiki/Church%27s_thesis_(constructive_mathematics)#Extended_Church's_thesis). Maybe also sketch / give reference for iMLTT and internal parametricity, so that your question looks polished.
Martin Berger
CC BY-SA 4.0
2019-12-04T09:37:37.980Z
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).
Andrej Bauer
<computability><type-theory><parametricity>
Extended Church's thesis and internal parametricity
Ilk
# Extended Church's thesis and internal parametricity

(Asked by: username_0 on 2019-12-03)

I am wondering if there is any known relationship between these 2 concepts in intensional MLTT as formulated [here](https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory).

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](https://arxiv.org/pdf/1905.03014.pdf) in the form compatible with univalence axiom.

This question is motivated by the results in [Parametricity and excluded middle](https://www.cs.bham.ac.uk/~abb538/papers/2016-02-parametricity.pdf), 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](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.908.7845&rep=rep1&type=pdf).

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.

**Tags:** computability, type-theory, parametricity

> **Comments:**
> **username_0**: Can someone explain to me the reason for the downvote, so I can improve the question?  
> **username_1**: 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](https://en.wikipedia.org/wiki/Church%27s_thesis_(constructive_mathematics)#Extended_Church's_thesis). Maybe also sketch / give reference for iMLTT and internal parametricity, so that your question looks polished.  
> **username_2**: 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).  

---

## 1 answers

### Answer by username_2 on 2019-12-05. Score: 5 | Accepted answer

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](http://publications.lib.chalmers.se/records/fulltext/230735/local_230735.pdf), 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.


---

