Warren does nonetheless propose a characterization in terms of introduction and elim rules, but it sets of red flashing klaxony alarms in my brain because it has the same introduction rule as equality: just refl. Experience has taught me repeatedly that something deeply weird is going on (not necessarily wrong, just weird) when two propositional connectives have the same intro rules but different elim rules, or vice-versa.
That being said, I'm definitely sympathetic to the goal of finding a characterization of roughly this shape. It would be awesome to have. The stuff Bob Harper and Dan Licata worked out at dimension 2 ("2-Dimensional directed dependent type theory", which is cited and linked over here) is really cool and all, but it seems to require a lot of clever and delicate axiom-inventing. It took me a lot of staring and mumbling before I believed that all of the polarities assigned in the rules for dependent product types had to be the way they were.