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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.