What I am writing up now looks approximately as follows:
It is a type system or, to be more precise, a family of type systems parametrized by pairs (UC, FV) where UC is a “universe context” and FV a sequence of formal type variables. The type systems of this family corresponding to sensible UC (which is a well defined and decidable property) and empty FV have univalent model.
It has three classes of expressions - u-level expressions (corresponding to universe levels), T-expressions (corresponding to types) and o-expressions (corresponding to objects of types).
It has universes, dependent products, unit type, dependent sums, empty type, pairwise disjoint unions, generalized W-types (corresponding to parametrized containers) and identity types. It has resizing rules.
It has unique typing. More precisely for a given context G and a given o-term o there is an easily computable T-term \tau_G(o) which is the type of o in G.
It is expected to have canonicity for disjoint unions and generalized W-types.
It has stronger definitional equality than most other intensional type systems. In particular, it has eta-rule for all type constructors listed above other than the identity types.
This makes definitional equality to be context dependent and undecidable. Therefore sentences (sequents) can not be internally represented syntactically (i.e. as sequences of terms) because it is impossible to mechanically verify derivability in such presentation.
This is approximately where I am now - thinking about the way to represent sentences (theorems, proofs) in a way which would allow for mechanical verification of derivability. At the moment I am considering the possibility to represent sentences directly by their derivation trees.
Since definitional equality is context dependent and undecidable anyway one can play with many ideas related to making it even stronger e.g. by adding functional extensionality. I think that canonicity can still be preserved, at least for natural numbers, because in the presence of eta-rule for nat propositional equality in nat implies definitional equality.
Vladimir.