# What are the pros and cons for type cases in dependent type theories?

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

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.

• 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. Commented May 22, 2021 at 19:47
• @AndrejBauer well, if you have induction-recursion, you're not in such bad shape, as long as you stay nice and predicative.
– cody
Commented May 23, 2021 at 3:31
• @AndrejBauer How do you model the injectivity of pi-types in judgemental equality without something like codes lurking in a dark corner somewhere? Commented May 23, 2021 at 6:31
• $\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. Commented May 23, 2021 at 12:11
• 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. Commented May 24, 2021 at 16:16