In intensional Martin-Löf type theory we can prove the metatheorem that two closed terms are propositionally equal iff they are judgmentally equal.

Is there a non-empty model of homotopy type theory where this metatheorem holds?

  • 1
    $\begingroup$ You have many basic questions about homotopy type theory and type theory in general, which I think might be answered more quickly at the HoTT Zulip. Are you a member there? I am not saying that you shouldn't be asking the questions here, but over there you have dozens of people doing HoTT, whereas here you will quickly exhaust the energy of the few HoTT experts who answer HoTT-related questions. $\endgroup$ Mar 19 at 16:29
  • $\begingroup$ The boring answer is yes: just start from the syntactic model and quotient it by propositional equality. But perhaps you meant a certain kind of model where equality is easy to decide? $\endgroup$
    – Jesper
    Mar 19 at 16:30
  • 2
    $\begingroup$ P. S. You have not accepted any answers so far (clicked on the "check" next to an answer), which makes it unclear as to whether you are generally dissatisfied with our answers, or you just don't know that it's good manners to accept answers that you are happy with. $\endgroup$ Mar 19 at 16:31
  • $\begingroup$ @Jesper: How do you know that model is non-trivial? $\endgroup$ Mar 19 at 16:32
  • 1
    $\begingroup$ It's not obvious to me how that would work, either, since there are closed terms of the universe where 'propositional' equality is not a proposition in the homotopy sense. For instance, there are multiple distinct paths between each of $2 + 2$, $2 × 2$ and $2 → 2$. So what does 'quotienting' do in situataions like that? $\endgroup$
    – Dan Doel
    Mar 19 at 19:53

Your Answer

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