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, 2020 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, 2020 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, 2020 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, 2020 at 22:12
  • 1
    $\begingroup$ Just kind of squeezing a type between UIP and full Univalence... $\endgroup$
    – cody
    Mar 30, 2020 at 23:31


Your Answer

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

Browse other questions tagged or ask your own question.