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.

$\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$ Commented Jan 16, 2020 at 15:54

1 Answer 1

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.