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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.