<p>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</p>
<ul>
<li>Constructors form one map</li>
<li>Eliminators form the inverse map</li>
<li>β-rules express <code>elim ∘ con = id</code></li>
<li>η-rules (uniqueness) express <code>con ∘ elim = id</code></li>
</ul>
<p>For example, function types are given as <code>Tm Γ (Π A B) ≃ Tm (Γ, A) B</code>.</p>
<ul>
<li><code>lam : Tm (Γ, A) B → Tm Γ (Π A B)</code></li>
<li><code>app : Tm Γ (Π A B) → Tm (Γ, A) B</code></li>
</ul>
<p>For Σ types, we have that internal Σ is isomorphic to metatheoretic Σ.</p>
<ul>
<li><code>pair  : Σ(t : Tm Γ A) × (Tm Γ (B[t])) → Tm Γ (Σ A B)</code></li>
<li><code>proj  : Tm Γ (Σ A B) → Σ(t : Tm Γ A) × (Tm Γ (B[t]))</code></li>
</ul>
<p>In extensional type theory, the identity type is specified to be isomorphic to
metatheoretic equality:</p>
<ul>
<li><code>refl    : t = u → Tm Γ (Id t u)</code></li>
<li><code>reflect : Tm Γ (Id t u) → t = u</code></li>
</ul>
<p>Here <code>reflect</code> is equality reflection. If the metatheory has UIP, the object
theory inherits it via the <code>β</code> and <code>η</code> rules (omitted above). If the
metatheory <em>does not</em> have UIP, the object theory also does not have it!</p>
<p>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.</p>
<p>In intensional TT, <code>Id</code> is specified differently, since in that case we do
not think of <code>Id</code> as a negative type (a terminal algebra, specified by an
isomorphism), but as a positive type (initial algebra).</p>
<p>Can we define terms of positive types with isomorphisms? What about sum types:</p>
<ul>
<li><code>inj  : Tm Γ A + Tm Γ B → Tm Γ (A + B)</code></li>
<li><code>elim : Tm Γ (A + B) → Tm Γ A + Tm Γ B</code></li>
</ul>
<p><code>elim</code> is unfortunately not feasible in a constructive and proof-relevant
way. If we have a variable <code>x : A + B</code> in the context, we cannot decide whether
<code>A</code> is provable or <code>B</code> is provable. This only works in the empty context, where
everything computes to <code>inj1</code> or <code>inj2</code>.</p>
<p>In other words, the problem is that positive types are categorically defined by mapping out (like <code>(A + B) → C ≃ (A → B) × (A → C)</code>), but in type theory, terms always map from the context into the type former.</p>

CC BY-SA 4.0
2021-04-29T11:32:34.210Z
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
CC BY-SA 4.0
2021-04-29T10:35:15.210Z
2021-04-29T11:09:41.933Z
2021-04-29T11:09:41.933Z
András Kovács
<p>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 CH-correspondence), the uniqueness rules seem to fit better as a 'converse' of the introduction theorems. <em>Am I right?</em></p>
<p>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.</p>
<p>Examples (as AB asked):</p>
<ul>
<li>Product type
<ul>
<li>Intro: given <span class="math-container">$a:A,b:B$</span> an instance of <span class="math-container">$A \times B$</span> can be uniquely constructed</li>
<li>Unique: given an instance of <span class="math-container">$A \times B$</span>, it is uniquely constructed by some <span class="math-container">$a:A,b:B$</span></li>
<li>Elim (I'm just using the non-dependent version to make it simple): providing a function <span class="math-container">$A \to B \to C$</span>, we could feed it with an instance of <span class="math-container">$A \times B$</span> and we could obtain an instance of <span class="math-container">$C$</span></li>
</ul>
</li>
<li>Identity type a la Martin-Löf
<ul>
<li>Intro: given <span class="math-container">$x:A$</span> an instance of <span class="math-container">$\sum_{x:A}{x=_A x}$</span> can be uniquely constructed</li>
<li>Unique: given an instance of <span class="math-container">$\sum_{y:A}{x=_A y}$</span> must be uniquely constructed from some <span class="math-container">$x:A$</span></li>
<li>Elim: omitted</li>
</ul>
</li>
</ul>
<p>I'm asking to look for criticisms on my pov.</p>

CC BY-SA 4.0
2021-04-28T20:49:52.157Z
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
CC BY-SA 4.0
2021-04-29T11:11:25.143Z
@AndrejBauer I modified it
ice1000
<type-theory>
Are uniqueness rules converse to introduction rules?
ice1000
# Are uniqueness rules converse to introduction rules?

(Asked by: username_0 on 2021-04-28)

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

**Tags:** type-theory
> **Comments:**
> **username_1**: 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.  
> **username_0**: @AndrejBauer I modified it  

---

## 1 answers

### Answer by username_2 on 2021-04-29. Score: 7 | Accepted answer

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.

> **Comments:**
> **username_0**: 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.  

---

