Are uniqueness rules converse to introduction rules? I've seen many people connecting introduction rules and elimination rules, saying that they're dual notion. Indeed, like in the categorical model, these rules are symmetric morphisms. However, if we think of the introduction rules as 'theorems' (in the sense of CHK-correspondence), the uniqueness rules seem to fit better as a 'converse' of the introduction theorems. Am I right?
My reason: it's because the uniqueness rules take the return type of the introduction rules as input, while the elimination rules take the return value of the formation rule as input.
Examples (as AB asked):

Product type

Intro: given $a:A,b:B$ an instance of $A \times B$ can be uniquely constructed
Unique: given an instance of $A \times B$, it is uniquely constructed by some $a:A,b:B$
Elim (I'm just using the non-dependent version to make it simple): providing a function $A \to B \to C$, we could feed it with an instance of $A \times B$ and we could obtain an instance of $C$


Identity type a la Martin-Löf

Intro: given $x:A$ an instance of $\sum_{x:A}{x=_A x}$ can be uniquely constructed
Unique: given an instance of $\sum_{y:A}{x=_A y}$ must be uniquely constructed from some $x:A$
Elim: omitted



I'm asking to look for criticisms on my pov.
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.