What exactly is "large elimination"?

Question

I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example:

impredicative polymorphism + excluded middle + large elimination => false

While I have an intuitive understanding of what it means, I wasn't been able to find or construct a more formal definition of what precisely is "large elimination".

In my understanding, large elimination is when a term t : T is eliminated (destructed) to get a value of type D, where D depends on the value of t.

For example, if vec_bool : nat -> Type is a type constructor for the boolean list of a fixed size with data constructors

nil  : vec_bool 0
cons : forall n:nat, bool -> vec_bool n -> vec_bool (S n)

the following recursive definition performs a large elimination on n:

Fixpoint construct_false_list (n:nat) : vec_bool n :=
   match n with
   | 0      => nil
   | Succ m => cons m false (construct_false_list m)
   end.

Is my understanding correct, or am I missing something?

Answer 1

You are incorrect about the definition of large elimination: it refers to the ability to build values of type $\mathrm{Type}$ by eliminating an inductive value. The canonical example:

bool_to_type : bool -> Type := fun b =>
     match b with
         | true => Unit
         | false => Empty

Where Unit and Empty are inductive types with 1 and 0 constructors, respectively. Notably, this allows you to prove the proposition $0 \not= 1$, which cannot be proven without this ability.

As noted in another answer (https://cstheory.stackexchange.com/a/21878/3984) a good resource that explains this is the following github repo: https://github.com/FStarLang/FStar/issues/360

Answer 2

Here is another attempt to illustrate large elimination. Consider the two following two ways to define a type: as an inductive or by induction.

For instance, here are two definitions of a vector with size n.

data vec (A: Type): nat -> Type where
  nil  : Unit        → vec A 0
  cons : A × vec A n → vec A (S n)

vs

vec (A: Type): nat → Type
vec A 0     = Unit
vec A (S n) = A × vec A n

Both definitions define a type vec : Type → nat → Type.

The recursive definition requires large elimination because we pattern matched on a value (a nat) to define a type. The inductive definition did not require large elimination.

But note that not all functions from something to type require large elimination, for example the identity type:

ID : Type → Type
ID A = A

The identity type is defined as a function, but it only has a single definition and no elimination (case distinction), therefore this definition does not require large elimination.

---

(There are some differences between these two styles of defining a type. To avoid infinite loops and thereby inconsistency, inductive definitions are in general checked to conform to strict positivity, while recursive type definitions are generally checked to conform to structural recursion. This means there are a few types that you can define only as an inductive and not by induction (for example arbitrary length lists violate structural recursion, as there is nothing to pattern match and recurse on); and a few types that you can define only by induction and not as an inductive (for example the denotation type used in normalisation by evaluation violates strict-positivity).)