# What exactly is “large elimination”?

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?

• section 3 of github.com/jdolson/hott-notes/blob/pdfs/pdfs/notes_week5.pdf may help. There are also videos for the entire class if you want to dig in. – user833970 Mar 7 '18 at 16:25
• "a term t : T is eliminated (destructed) to get a value of type D, where D depends on the value of t" <- this is called "dependent elimination" – Jason Gross Mar 7 '18 at 20:29

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

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.