<p>No: strong elimination of large inductive types (SELIT) is itself inconsistent because it breaks the layering of universes by trivially allowing you to smuggle a large value in a Prop box and take it back out unscathed.</p>
<p>In <a href="https://doi.org/10.4230/LIPIcs.TYPES.2019.9" rel="noreferrer">Is Impredicativity Implicitly Implicit?</a> I proposed a restriction on SELIT which is a bit more permissive than Coq's while still enjoying consistency (I still don't have a proof for it, tho I believe I'm almost there ;-)</p>

CC BY-SA 4.0
2021-03-04T23:51:27.957Z
Are strong eliminations the same thing as large eliminations?
NJay
CC BY-SA 4.0
2021-03-05T19:35:19.310Z
@NJay: Yes.  AFAIK "strong elimination" is the more correct term, but I could never find a definitive answer on that all-too-important part of the question ;-)
Stefan
CC BY-SA 4.0
2021-03-06T09:31:41.777Z
What do you mean by "more correct", out of curiosity? Are there parts of the literature that refer to this as "strong elimination"?
NJay
CC BY-SA 4.0
2021-03-07T18:16:17.910Z
@NJay: Just a hunch, really.  I have the suspicion that the term "large elimination" is a mix-up between "large types" and "strong elimination" (a bit like some people end up mixing "higher-order functions" and "first class functions" into "higher-class functions" or "first-order functions").  I believe I've seen the term "strong elimination" used more often, at least in the context of CIC.  But I really don't know if any of this is actually true.
Stefan
CC BY-SA 4.0
2021-09-28T14:54:42.997Z
I've heard "large elimination" far more often than "strong elimination".  For instance here, https://github.com/RobertHarper/hott-notes/blob/5339576f55a4b7f5d04734370a5117491c44b1fe/notes_week5.tex#L155 with a conventional definition of large elimination, and no mention of "large elimination" in the entire notes.  this may be the sort of definition that is really sensitive to the underling language constructs.
user833970
CC BY-SA 4.0
2021-03-04T15:46:50.837Z
2021-03-04T15:46:50.837Z
Stefan
<p>It is known that <code>impredicativity + large eliminations + excluded middle</code> is inconsistent. Prop is impredicative and consistent with excluded middle, but does not allow large eliminations (except when constructing witnesses whose type lives in Prop). Set and Type(i) allow large eliminations and are consistent with excluded middle, but are predicative. If we use the <code>-impredicative-set</code> flag, then Set is impredicative, but does not allow large eliminations for large inductive types.</p>
<p>Is there a universe in Coq which is impredicative, allows large eliminations on any inductive type that lives in it, but is consistent in the absence of the axiom of excluded middle?</p>

<dependent-type><coq>
Impredicativity + large eliminations (with no excluded middle) in Coq
NJay
# Impredicativity + large eliminations (with no excluded middle) in Coq

(Asked by: username_0 on 2021-03-04)

It is known that `impredicativity + large eliminations + excluded middle` is inconsistent. Prop is impredicative and consistent with excluded middle, but does not allow large eliminations (except when constructing witnesses whose type lives in Prop). Set and Type(i) allow large eliminations and are consistent with excluded middle, but are predicative. If we use the `-impredicative-set` flag, then Set is impredicative, but does not allow large eliminations for large inductive types.

Is there a universe in Coq which is impredicative, allows large eliminations on any inductive type that lives in it, but is consistent in the absence of the axiom of excluded middle?

**Tags:** dependent-type, coq


---

## 1 answers

### Answer by username_1 on 2021-03-04. Score: 6 | Accepted answer

No: strong elimination of large inductive types (SELIT) is itself inconsistent because it breaks the layering of universes by trivially allowing you to smuggle a large value in a Prop box and take it back out unscathed.

In [Is Impredicativity Implicitly Implicit?](https://doi.org/10.4230/LIPIcs.TYPES.2019.9) I proposed a restriction on SELIT which is a bit more permissive than Coq's while still enjoying consistency (I still don't have a proof for it, tho I believe I'm almost there ;-)

> **Comments:**
> **username_0**: Are strong eliminations the same thing as large eliminations?  
> **username_1**: @username_0: Yes.  AFAIK "strong elimination" is the more correct term, but I could never find a definitive answer on that all-too-important part of the question ;-)  
> **username_0**: What do you mean by "more correct", out of curiosity? Are there parts of the literature that refer to this as "strong elimination"?  
> **username_1**: @username_0: Just a hunch, really.  I have the suspicion that the term "large elimination" is a mix-up between "large types" and "strong elimination" (a bit like some people end up mixing "higher-order functions" and "first class functions" into "higher-class functions" or "first-order functions").  I believe I've seen the term "strong elimination" used more often, at least in the context of CIC.  But I really don't know if any of this is actually true.  
> **username_2**: I've heard "large elimination" far more often than "strong elimination".  For instance here, https://github.com/RobertHarper/hott-notes/blob/5339576f55a4b7f5d04734370a5117491c44b1fe/notes_week5.tex#L155 with a conventional definition of large elimination, and no mention of "large elimination" in the entire notes.  this may be the sort of definition that is really sensitive to the underling language constructs.  

---

