Are uniqueness rules converse to introduction rules?
Uniqueness is not converse to introduction. Uniqueness rules in type theory are
components of isomorphisms. If a type former is specified with an isomorphism, then

Constructors form one map
Eliminators form the inverse map
β-rules express elim ∘ con = id
η-rules (uniqueness) express con ∘ elim = id

For example, function types are given as Tm Γ (Π A B) ≃ Tm (Γ, A) B.

lam : Tm (Γ, A) B → Tm Γ (Π A B)
app : Tm Γ (Π A B) → Tm (Γ, A) B

For Σ types, we have that internal Σ is isomorphic to metatheoretic Σ.

pair  : Σ(t : Tm Γ A) × (Tm Γ (B[t])) → Tm Γ (Σ A B)
proj  : Tm Γ (Σ A B) → Σ(t : Tm Γ A) × (Tm Γ (B[t]))

In extensional type theory, the identity type is specified to be isomorphic to
metatheoretic equality:

refl    : t = u → Tm Γ (Id t u)
reflect : Tm Γ (Id t u) → t = u

Here reflect is equality reflection. If the metatheory has UIP, the object
theory inherits it via the β and η rules (omitted above). If the
metatheory does not have UIP, the object theory also does not have it!
So UIP is not like η-rules for other negative type formers. UIP is something
that we get if assume UIP in the metatheory and try to weaken the above rules
just enough to get decidable definitional equality.
In intensional TT, Id is specified differently, since in that case we do
not think of Id as a negative type (a terminal algebra, specified by an
isomorphism), but as a positive type (initial algebra).
Can we define terms of positive types with isomorphisms? What about sum types:

inj  : Tm Γ A + Tm Γ B → Tm Γ (A + B)
elim : Tm Γ (A + B) → Tm Γ A + Tm Γ B

elim is unfortunately not feasible in a constructive and proof-relevant
way. If we have a variable x : A + B in the context, we cannot decide whether
A is provable or B is provable. This only works in the empty context, where
everything computes to inj1 or inj2.
In other words, the problem is that positive types are categorically defined by mapping out (like (A + B) → C ≃ (A → B) × (A → C)), but in type theory, terms always map from the context into the type former.