# 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? Commented Jan 16, 2020 at 14:23
• Oh, that's totally true. Thank you. Commented Jan 16, 2020 at 15:54

$$\prod_{X : \mathcal{U}} (X \to X) \cong 1$$ is consistent. It follows from parametricity and function extensionality. Usual parametric models also support function extensionality. The simplest one which suffices would be the Fam model where every closed type is a set together with a family of sets over it, functions are predicate-preserving functions and the universe is the set of sets together with the family which maps each $$A : \mathsf{Set}$$ to $$A \to \mathsf{Set}$$. Here's a reference for a model which also works for our purpose but which is more complicated than necessary.
$$(\prod_{X : \mathcal{U}} (A \to X) \to FX) \cong FA$$ is provably false in plain MLTT. Let $$F\,X := X \to \bot$$ and $$A := \bot$$. Now the statement simplifies to $$(\prod_{X : \mathcal{U}} X \to \bot) \cong \top$$, which is evidently false. Same for coYoneda. Pick $$A := \top$$ and $$F$$ as before, and coYoneda simplifies to $$(\sum_{X : \mathcal{U}} X \to \bot) \cong \bot$$. The problem is that $$F$$ is just an $$\mathcal{U}\to \mathcal{U}$$ function, and not a functor with respect to functions-as-morphisms in $$\mathcal{U}$$.
• Presheaves over $\cdot \to \cdot$ doesn't quite work. It is true that for every closed term $\vdash M : \Pi_{X : U} X \to X$ in type theory, $\Pi_{X : U} M X = 1_X$ holds in the model, but this is weaker than the internal statement $\Pi_{M : \prod_{X : U} X \to X} M X = 1_X$. E.g. the internal statement implies the law of excluded middle is false, but the double negation of LEM does hold in presheaves over $\cdot \to \cdot$.
• I don't know enough about parametric models to say how they compare with the Hofmann-Streicher presheaf interpretation of extensional type theory in presheaves. The universe you described for $\mathsf{Fam}$ looks like it works out the same as the Streicher universe in $\mathsf{Set}^\to$. I would have guessed that exponentials were the same as well.