<p>The basic idea is clearest when you think about things in terms of Tarski-style universes. There, you have a data type of <em>codes</em>, and an interpretation function which maps codes to <em>types</em>. In this case, it is obvious that you can discriminate on type codes, even though this is a much more questionable operation on types. For example, <span class="math-container">$\mathbb{N} \to 0$</span> and <span class="math-container">$\mathbb{R} \to 0$</span> are equal as sets, which means that injectivity of type constructors is obviously false — <span class="math-container">$\mathbb{R} \neq \mathbb{N}$</span>!</p>
<pre><code>-- A Tarski-style universe in Agda
—-
-- Declarations.
data TypeCode : Set
El : TypeCode → Set

-- Definitions.
data TypeCode where
  nat : TypeCode
  pi  : (a : TypeCode) (b : El a → TypeCode) → TypeCode

El nat      = Nat
El (pi a b) = (x : El a) → El (b x)
</code></pre>
<p>A definition very similar to this Agda code is pretty typical when building PER models of type theory — the main difference is just that everything is valued in PERs.</p>
<p>Distinguishing type codes and types is not “normal mathematics&quot;, which is a strike against it, but on the other hand, the stricter, more decidable, equality on type codes can make various forms of automation easier to implement.</p>
<p>Which is better? It’s unclear! As Edwin Brady says, we don’t know how to do dependent types wrong yet.</p>

CC BY-SA 4.0
2021-05-22T19:47:44.847Z
I beg to differ about "pretty typical when building PER models of type theory". Yes, NuPRL does this sort of thing, but in general realizability models have universes that are not inductive. In any case, an inductively defined universe is no universe in the sense usually understood by type theorirsts and mathematicians, it's just some syntax for types.
Andrej Bauer
CC BY-SA 4.0
2021-05-23T03:31:59.677Z
@AndrejBauer well, if you have induction-recursion, you're not in such bad shape, as long as you stay nice and predicative.
cody
CC BY-SA 4.0
2021-05-23T06:31:41.803Z
@AndrejBauer How do you model the injectivity of pi-types in judgemental equality without something like codes lurking in a dark corner somewhere?
Neel Krishnaswami
CC BY-SA 4.0
2021-05-23T12:11:37.973Z
$\Pi$-types are injective? Didn't you give a counter-example in your answer? To answer more seriously: *codes* for $\Pi$-types are injective, but to suppose that the $\Pi$-type constructions themselves are injective is a very serious commitment that may only be warrented in very specific situation. I certainly wouldn't recommend it as a general principle.
Andrej Bauer
CC BY-SA 4.0
2021-05-24T16:16:24.360Z
Another note: Mahlo universes cannot consistently have inductive eliminators (this is mentioned in some Anton Setzer papers). So for instance, even if Agda's universes were Tarski style, it wouldn't be consistent to have an induction principle for their codes, because they're closed under induction-recursion.
Dan Doel
CC BY-SA 4.0
2021-05-25T05:49:34.583Z
@AndrejBauer The judgemental equality for a type theory certainly treats pi-types as injective, so when you are showing that it is decidable I see no way to avoid putting something morally equivalent to codes into the model construction. Or am I misunderstanding your point somehow?
Neel Krishnaswami
CC BY-SA 4.0
2021-05-25T06:01:40.660Z
Which standard rule of type theory shows that $\Pi$ is injective?
Andrej Bauer
CC BY-SA 4.0
2021-05-22T17:28:35.173Z
2021-05-22T17:28:35.173Z
Neel Krishnaswami
<p>Pattern matching on <span class="math-container">$\cal U$</span> is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove that?).</p>
<p>I wonder how this feature work in the underlying model of type theories and how do they affect programming in dependent type systems. It seems that <span class="math-container">$\cal U$</span> will then become an inductive type, and formation rules are turned into introduction rules...</p>

<pl.programming-languages><type-theory><dependent-type>
What are the pros and cons for type cases in dependent type theories?
ice1000
# What are the pros and cons for type cases in dependent type theories?

(Asked by: username_0 on 2021-05-22)

Pattern matching on $\cal U$ is allowed in XTT and Idris2 (for unerased types), and that implies the injectivity of type constructors (that's just my intuition, though -- I also wonder how do I prove that?).

I wonder how this feature work in the underlying model of type theories and how do they affect programming in dependent type systems. It seems that $\cal U$ will then become an inductive type, and formation rules are turned into introduction rules...

**Tags:** pl.programming-languages, type-theory, dependent-type


---

## 1 answers

### Answer by username_1 on 2021-05-22. Score: 6 | Accepted answer

The basic idea is clearest when you think about things in terms of Tarski-style universes. There, you have a data type of codes, and an interpretation function which maps codes to types. In this case, it is obvious that you can discriminate on type codes, even though this is a much more questionable operation on types. For example, $\mathbb{N} \to 0$ and $\mathbb{R} \to 0$ are equal as sets, which means that injectivity of type constructors is obviously false — $\mathbb{R} \neq \mathbb{N}$!
-- A Tarski-style universe in Agda
—-
-- Declarations.
data TypeCode : Set
El : TypeCode → Set

-- Definitions.
data TypeCode where
  nat : TypeCode
  pi  : (a : TypeCode) (b : El a → TypeCode) → TypeCode

El nat      = Nat
El (pi a b) = (x : El a) → El (b x)

A definition very similar to this Agda code is pretty typical when building PER models of type theory — the main difference is just that everything is valued in PERs.
Distinguishing type codes and types is not “normal mathematics", which is a strike against it, but on the other hand, the stricter, more decidable, equality on type codes can make various forms of automation easier to implement.
Which is better? It’s unclear! As Edwin Brady says, we don’t know how to do dependent types wrong yet.

> **Comments:**
> **username_2**: I beg to differ about "pretty typical when building PER models of type theory". Yes, NuPRL does this sort of thing, but in general realizability models have universes that are not inductive. In any case, an inductively defined universe is no universe in the sense usually understood by type theorirsts and mathematicians, it's just some syntax for types.  
> **username_3**: @AndrejBauer well, if you have induction-recursion, you're not in such bad shape, as long as you stay nice and predicative.  
> **username_1**: @AndrejBauer How do you model the injectivity of pi-types in judgemental equality without something like codes lurking in a dark corner somewhere?  
> **username_2**: $\Pi$-types are injective? Didn't you give a counter-example in your answer? To answer more seriously: *codes* for $\Pi$-types are injective, but to suppose that the $\Pi$-type constructions themselves are injective is a very serious commitment that may only be warrented in very specific situation. I certainly wouldn't recommend it as a general principle.  
> **username_4**: Another note: Mahlo universes cannot consistently have inductive eliminators (this is mentioned in some Anton Setzer papers). So for instance, even if Agda's universes were Tarski style, it wouldn't be consistent to have an induction principle for their codes, because they're closed under induction-recursion.  
> **username_1**: @AndrejBauer The judgemental equality for a type theory certainly treats pi-types as injective, so when you are showing that it is decidable I see no way to avoid putting something morally equivalent to codes into the model construction. Or am I misunderstanding your point somehow?  
> **username_2**: Which standard rule of type theory shows that $\Pi$ is injective?  

---

