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.
 A: $\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}$. 
