7
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ I think "admissible" is the wrong word here. You probably mean consistent? $\endgroup$
    – Max New
    Commented Jan 16, 2020 at 14:23
  • 1
    $\begingroup$ Oh, that's totally true. Thank you. $\endgroup$
    – Mario
    Commented Jan 16, 2020 at 15:54

1 Answer 1

Reset to default
8
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ 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$. $\endgroup$
    – aws
    Commented Feb 21, 2020 at 17:01
  • 1
    $\begingroup$ @aws I'll believe that, edited. Are functions and universes the crucial difference in the presheaf version? $\endgroup$
    – András Kovács
    Commented Feb 21, 2020 at 18:20
  • $\begingroup$ 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. $\endgroup$
    – aws
    Commented Feb 21, 2020 at 21:59

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .