Assume we work in some minimalistic version of Martin-Löf type theory. Does it break consistency 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", I understand that if it could be proved, excluded middle would not be admissible.

More generally, can we assume this form of Yoneda reduction for $F : \mathcal{U} \to \mathcal{U}$ without breaking consistency? $$ \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 and later by Escardó relating the J-elimination rule and the Yoneda lemma.

Assume we work in some minimalistic version of Martin-Löf type theory. Does it break consistency 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", I understand that if it could be proved, excluded middle would not be consistent.

More generally, can we assume this form of Yoneda reduction for $F : \mathcal{U} \to \mathcal{U}$ without breaking consistency? $$ \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 and later by Escardó relating the J-elimination rule and the Yoneda lemma.

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", 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 and later by Escardó relating the J-elimination rule and the Yoneda lemma.

Assume we work in some minimalistic version of Martin-Löf type theory. Does it break consistency 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", I understand that if it could be proved, excluded middle would not be admissible.

More generally, can we assume this form of Yoneda reduction for $F : \mathcal{U} \to \mathcal{U}$ without breaking consistency? $$ \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 and later by Escardó relating the J-elimination rule and the Yoneda lemma.