# 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.

• 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.

• The question would be easier to understand if you included at least one concrete example. That way we can figure out what you mean more easily. – Andrej Bauer Apr 28 at 20:49
• @AndrejBauer I modified it – ice1000 Apr 29 at 11:11

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.

• Thank you. I think what I'm missing is that uniqueness rules are stronger than what I thought -- it not only states how terms are constructed, but also what they use to construct. Like you said, it also mentions elim rules. – ice1000 Apr 29 at 11:32