Assume we work in some minimalistic version of Martin-Löf type theory. Is it admissible to postulate that the function that selects the identity function has an inverse? 
$$\prod_{X : \mathcal{U}} (X \to X) \cong 1.$$
From ["Parametricity, automorphisms of the universe, and excluded middle"][1], I understand that if it could be proved, excluded middle would not be admissible.

More generally, is this form of Yoneda reduction admissible for $F : \mathcal{U} \to \mathcal{U}$?
$$
\left(\prod_{X : \mathcal{U}}  (A \to X) \to FX\right) \cong FA,
$$
Or this form of coYoneda?
$$
\left(\sum_{X : \mathcal{U}}  (X \to A) \times FX \right) \cong FA,
$$
The same question, but with paths instead of functions, points me to work by [Rijke][2] and later by [Escardó][3] relating the J-elimination rule and the Yoneda lemma.


  [1]: https://arxiv.org/abs/1701.05617
  [2]: https://homotopytypetheory.org/2012/05/02/a-type-theoretical-yoneda-lemma/
  [3]: https://www.cs.bham.ac.uk/~mhe/yoneda/yoneda.html