# Is $\prod_{X : \mathcal{U}} (X \to X) \cong 1$ consistent with type theory?

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.

• I think "admissible" is the wrong word here. You probably mean consistent? – Max New Jan 16 at 14:23
• Oh, that's totally true. Thank you. – Mario Román Jan 16 at 15:54