Is the type of propositional equality actually inductive in the HoTT context?

The family of a family of sentences is _==_

defined inductively with a single constructor idp : a == a

. But in the context of HoTT, it is clear that a type A == B

can contain elements other than idp

(after applying the postulated axiom of uniqueness).

• Is it correct to apply the principle of induction to type A == B
  
  ? Function definitions using induction A == B
  
  do not seem to be accurate.
• Wouldn't it be wrong to include the axiom of uniqueness as a constructor for a type A == B
  
  rather than postulate?