I am wondering if there are any interesting rules/judgemental equalities, denoted $A$, which satisfy the following properties:

$iMLTTfe+UA \implies \neg A$

$iMLTTfe+UIP \implies \neg A$, or more specifically Observational type theory.

$iMLTTfe+A$ is consistent and satisfies canonicity.

Where abrrevations mean:
iMLTTfe - intensional Martin-Löf type theory with function extensionality
UA - univalence axiom
UIP - uniqueness of identity proofs

  • $\begingroup$ Not really familiar with this, but is it possible to add an axiom to a theory without canonicity (e.g. $iMLTT+FunExt$) and get something with canonicity? That seems weird to me. $\endgroup$
    – SCappella
    Mar 30 '20 at 8:15
  • 2
    $\begingroup$ Ah, so you're including adding judgemental equalities and similar things, not just postulating terms of particular types (like UA, UIP and FunExt do). Ok, sounds good to me. $\endgroup$
    – SCappella
    Mar 30 '20 at 8:22
  • 1
    $\begingroup$ So you are not really talking about axioms, but rather new rules. Please edit your question accordingly. $\endgroup$ Mar 30 '20 at 16:36
  • 1
    $\begingroup$ A small optimization: since $\mathrm{UA}$ implies $\mathrm{FunExt}$, your base theory could be $\mathrm{iMLTT} + \mathrm{FunExt}$ throughout. Then you're asking for $A$ which is incompatible with univalence and with UIP, but it gives you canonicity. Hmm, I can't even think of reasonable $A$'s that are incompatible with both univalence and UIP. $\endgroup$ Mar 30 '20 at 22:12
  • 1
    $\begingroup$ Just kind of squeezing a type between UIP and full Univalence... $\endgroup$
    – cody
    Mar 30 '20 at 23:31

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.