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