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