# Rules between UIP with function extensionality and univalence

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

• 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. Mar 30 '20 at 8:15
• 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. Mar 30 '20 at 8:22
• So you are not really talking about axioms, but rather new rules. Please edit your question accordingly. Mar 30 '20 at 16:36
• 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. Mar 30 '20 at 22:12
• Just kind of squeezing a type between UIP and full Univalence...
– cody
Mar 30 '20 at 23:31