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

<pre><code>bool_to_type : bool -&gt; Type := fun b =&gt;
     match b with
         | true =&gt; Unit
         | false =&gt; Empty
</code></pre>

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

<p>As noted in another answer (<a href="https://cstheory.stackexchange.com/a/21878/3984">https://cstheory.stackexchange.com/a/21878/3984</a>) a good resource that explains this is the following github repo: <a href="https://github.com/FStarLang/FStar/issues/360" rel="noreferrer">https://github.com/FStarLang/FStar/issues/360</a></p>

CC BY-SA 3.0
2018-03-07T16:56:48.450Z
2018-03-07T19:16:58.717Z
2018-03-07T19:16:58.717Z
cody
<p>Here is another attempt to illustrate large elimination. Consider the two following two ways to define a type: <em>as an inductive</em> or <em>by induction</em>.</p>
<p>For instance, here are two definitions of a vector with size n.</p>
<pre><code>data vec (A: Type): nat -&gt; Type where
  nil  : Unit        → vec A 0
  cons : A × vec A n → vec A (S n)
</code></pre>
<p>vs</p>
<pre><code>vec (A: Type): nat → Type
vec A 0     = Unit
vec A (S n) = A × vec A n
</code></pre>
<p>Both definitions define a type
<code>vec : Type → nat → Type</code>.</p>
<p>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.</p>
<p>But note that not all functions from something to type require large elimination, for example the identity type:</p>
<pre><code>ID : Type → Type
ID A = A
</code></pre>
<p>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.</p>
<hr />
<p>(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).)</p>

CC BY-SA 4.0
2022-11-15T22:44:22.657Z
2022-11-15T22:44:22.657Z
drcicero
<p>I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example: </p>

<blockquote>
  <p>impredicative polymorphism + excluded middle + large elimination => false</p>
</blockquote>

<p>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".</p>

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

<p>For example, if <code>vec_bool : nat -&gt; Type</code> is a type constructor for the boolean list of a fixed size with data constructors</p>

<pre><code>nil  : vec_bool 0
cons : forall n:nat, bool -&gt; vec_bool n -&gt; vec_bool (S n)
</code></pre>

<p>the following recursive definition performs a large elimination on <code>n</code>:</p>

<pre><code>Fixpoint construct_false_list (n:nat) : vec_bool n :=
   match n with
   | 0      =&gt; nil
   | Succ m =&gt; cons m false (construct_false_list m)
   end.
</code></pre>

<p>Is my understanding correct, or am I missing something?</p>

CC BY-SA 3.0
2018-03-07T16:25:18.130Z
section 3 of https://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
CC BY-SA 3.0
2018-03-07T20:29:54.943Z
"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
<type-theory><coq>
What exactly is "large elimination"?
deniss
# What exactly is "large elimination"?

(Asked by: username_0 on 2018-03-07)

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?

**Tags:** type-theory, coq

> **Comments:**
> **username_1**: section 3 of https://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.  
> **username_2**: "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"  

---

## 2 answers

### Answer by username_3 on 2018-03-07. Score: 11 | Accepted answer

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 by username_4 on 2022-11-15. Score: 4

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


---

