<p>AFAIK, <strong>dependent elimination</strong> was introduced by Coquand in '92, under the name &quot;dependent pattern matching&quot;, in the paper <a href="https://wonks.github.io/type-theory-reading-group/papers/proc92-coquand.pdf" rel="nofollow noreferrer">Pattern Matching with Dependent Types</a></p>
<p>Famously implemented in the Agda system, the main idea (and difference with, say, the default matching in Coq) is that there is additional information added in the right hand side of a case definition: say if you have</p>
<pre><code>datatype Fin : nat -&gt; Type = Zero : Fin (S 0) | Succ : forall k, Fin k -&gt; Fin (S k)

f : forall n, Fin n -&gt; nat
f _ Zero = ???
f _ (Succ f) = ???
</code></pre>
<p>Then in the first <code>???</code>, you &quot;know&quot; the equation <code>n = S 0</code> and in the second <code>???</code> you know <code>n = S k</code>, which in turn can allow you to typecheck some terms that would otherwise be ill-typed. Indeed, if there is no possible well-typed right hand side (say if you knew <code>n = 0</code>) then you wouldn't even need to write that case!</p>
<p>It turns out that to recover the entire power of this kind of pattern matching, it suffices to add the axiom K (which roughly states that every proof of <code>x = x</code> is <code>refl</code>) as described in Goguen, McBride and McKinna <a href="https://link.springer.com/chapter/10.1007/11780274_27" rel="nofollow noreferrer">Eliminating Dependent Pattern Matching</a>. Coquand had previously noticed that K is provable in the presence of dependent pattern matching, so the two are roughly equivalent (up to some computational rules).</p>
<p><strong>Large elimination</strong> is the ability to eliminate to <code>Type</code>, e.g. defining <code>f 0 = Bool</code>, <code>f (S n) = Nat -&gt; f n</code>. One can notice that this enables proving <span class="math-container">$0 \not = 1$</span>, e.g. by defining <code>f 0 = False</code> and <code>f (S _) = True</code> and doing some simple rewriting. In a system like Coq, it is otherwise impossible to prove such a simple fact! Not sure who first noticed this.</p>

CC BY-SA 4.0
2023-04-12T16:23:08.087Z
2023-04-12T16:23:08.087Z
cody
<p>I am trying to find more information (preferably an academic paper) for the concept of &quot;dependent elimination&quot;. I understand the concept itself: it means constructing a type by eliminating a term i.e. eliminating a term into the large universe of types. But I would like to know if there is some paper or thesis or dissertation or book that I could cite. I know that <a href="https://cstheory.stackexchange.com/questions/40339/what-exactly-is-large-elimination">this Stack Exchange question</a> exists but I'm not sure it is exactly citeable.</p>
<p>I've read two papers that mention this concept, but unfortunately they don't add a citation for it:</p>
<ul>
<li><p><a href="https://www.cs.nott.ac.uk/%7Epsztxa/publ/pisigma-new.pdf" rel="nofollow noreferrer">ΠΣ: Dependent Types without the Sugar</a>;</p>
</li>
<li><p><a href="https://arxiv.org/pdf/1012.4896.pdf" rel="nofollow noreferrer">MiniAgda: Integrating Sized and Dependent Types</a> (which calls the concept &quot;large elimination&quot; instead of &quot;dependent elimination&quot;).</p>
</li>
</ul>
<p>Bottom line: is there somewhere I could read more about &quot;dependent elimination&quot; that I could also cite?</p>

CC BY-SA 4.0
2023-04-05T21:41:28.490Z
As far as I know, there isn't a unified technical meaning of "dependent elimination". For *specific* type constructions one can discuss dependent vs. non-dependent eliminators, but these are done on a case-by-case basis. The non-dependent eliminators are called "recursors".
Andrej Bauer
CC BY-SA 4.0
2023-04-10T13:35:57.987Z
I was mistaken about "large elimination" and "dependent elimination" being the same thing: "large elimination" means creating a type by eliminating a term and "dependent elimination" means adding knowledge about some pattern being eliminated to the context.  I still haven't found citeable information about either of these concepts but your help made me understand them better. Thanks!
Valmir Junior
<dependent-type>
Where can I find more information about "dependent elimination"?
Valmir Junior
# Where can I find more information about "dependent elimination"?

(Asked by: username_0 on 2023-04-05)

I am trying to find more information (preferably an academic paper) for the concept of "dependent elimination". I understand the concept itself: it means constructing a type by eliminating a term i.e. eliminating a term into the large universe of types. But I would like to know if there is some paper or thesis or dissertation or book that I could cite. I know that [this Stack Exchange question](https://cstheory.stackexchange.com/questions/40339/what-exactly-is-large-elimination) exists but I'm not sure it is exactly citeable.

I've read two papers that mention this concept, but unfortunately they don't add a citation for it:

* [ΠΣ: Dependent Types without the Sugar](https://www.cs.nott.ac.uk/%7Epsztxa/publ/pisigma-new.pdf);
* [MiniAgda: Integrating Sized and Dependent Types](https://arxiv.org/pdf/1012.4896.pdf) (which calls the concept "large elimination" instead of "dependent elimination").

Bottom line: is there somewhere I could read more about "dependent elimination" that I could also cite?

**Tags:** dependent-type
> **Comments:**
> **username_1**: As far as I know, there isn't a unified technical meaning of "dependent elimination". For *specific* type constructions one can discuss dependent vs. non-dependent eliminators, but these are done on a case-by-case basis. The non-dependent eliminators are called "recursors".  
> **username_0**: I was mistaken about "large elimination" and "dependent elimination" being the same thing: "large elimination" means creating a type by eliminating a term and "dependent elimination" means adding knowledge about some pattern being eliminated to the context.  I still haven't found citeable information about either of these concepts but your help made me understand them better. Thanks!  

---

## 1 answers

### Answer by username_2 on 2023-04-12. Score: 1 | Accepted answer

AFAIK, dependent elimination was introduced by Coquand in '92, under the name "dependent pattern matching", in the paper Pattern Matching with Dependent Types
Famously implemented in the Agda system, the main idea (and difference with, say, the default matching in Coq) is that there is additional information added in the right hand side of a case definition: say if you have
datatype Fin : nat -> Type = Zero : Fin (S 0) | Succ : forall k, Fin k -> Fin (S k)

f : forall n, Fin n -> nat
f _ Zero = ???
f _ (Succ f) = ???

Then in the first ???, you "know" the equation n = S 0 and in the second ??? you know n = S k, which in turn can allow you to typecheck some terms that would otherwise be ill-typed. Indeed, if there is no possible well-typed right hand side (say if you knew n = 0) then you wouldn't even need to write that case!
It turns out that to recover the entire power of this kind of pattern matching, it suffices to add the axiom K (which roughly states that every proof of x = x is refl) as described in Goguen, McBride and McKinna Eliminating Dependent Pattern Matching. Coquand had previously noticed that K is provable in the presence of dependent pattern matching, so the two are roughly equivalent (up to some computational rules).
Large elimination is the ability to eliminate to Type, e.g. defining f 0 = Bool, f (S n) = Nat -> f n. One can notice that this enables proving $0 \not = 1$, e.g. by defining f 0 = False and f (S _) = True and doing some simple rewriting. In a system like Coq, it is otherwise impossible to prove such a simple fact! Not sure who first noticed this.


---

