It's tempting to think that one can define univalence without universes, but I don't think this rule makes sense:
The
elimination rule says that given a judgment 'A type' in context Gamma, a
judgment 'B type' in context Gamma, a judgment 'C(p) type' in the
context 'Gamma, p : A = B', and a judgment 't:C(refl_A)' in the context
'Gamma', one could form the conclusion 'J(t, p): C(p)' in the context
'Gamma'
In the ordinary Id-elimination
rule, the motive C has to be defined in the context of two *variable*
elements of the type and an equality between them, not two *specific*
elements. In particular, if A and B are specific types, then it doesn't
make sense to substitute refl_A for p in C, because you can't
substitute A for B. You can only substitute for a variable.
I
think in order to do something like this, you have to augment type
theory by some kind of "polymorphism" that will allow you to hypothesize
a "type variable" in the context.