Return to Answer

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

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

$\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, or equivalently the presheaf model over the category $\cdot \to \cdot$. 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}$.

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

$\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, or equivalently the presheaf model over the category $\cdot \to \cdot$. 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 that statement simplifies to $\left(\prod_{X : \mathcal{U}} X \to \bot\right) \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}$.

$\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, or equivalently the presheaf model over the category $\cdot \to \cdot$. 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}$.