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 depends on the value of
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
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?