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.