# Zulip Chat Archive

## Stream: general

### Topic: large vs small elimination

#### Reid Barton (Mar 29 2019 at 21:05):

For each inductive type or structure Lean has to decide whether to generate large or small eliminators (eliminating to a type in an arbitrary universe, or only to a proposition). As I understand it, the algorithm is something like this.

- If the target universe of the inductive type is a Type (
`Sort u`

for`u >= 1`

), then always generate a large eliminator. - If the target universe is
`Prop`

, then only generate a large eliminator if there's at most one constructor and all of its fields are`Prop`

s.

However, with universe polymorphism, the target universe might be `Prop`

for some values of the universe parameters but not others. Currently Lean just rejects such definitions. That means you cannot define a structure like

universe u structure a (x : Sort u) : Sort u := (f : x)

You have to use a target universe of `Sort (max u 1)`

or similar. This causes some minor issues in #824 where we want to replace `Type`

by `Sort`

in category theory.

Would it be possible/sound for Lean to instead do the following?

- Solve for the universe variable substitutions which cause the target universe to become
`Prop = Sort 0`

, if possible. (This can be done in a simple syntax-directed way:`max u v = 0`

iff`u = 0`

and`v = 0`

;`imax u v = 0`

iff`v = 0`

;`u+1`

is never 0; etc.) - If there are such substitutions, then apply them before doing the large eliminator check for
`Prop`

s.

In the example, a large eliminator would be generated for `a`

, because when the target universe is `Prop`

, the field `f`

is also a `Prop`

.

Are there other reasons that Lean needs to know whether or not the target universe is a `Prop`

?

#### Mario Carneiro (Mar 29 2019 at 21:42):

This would obviously require a modification to lean's kernel, but I can confirm soundness against the paper proof.

#### Mario Carneiro (Mar 29 2019 at 21:43):

I think lean will accept inductive types in `Sort u`

under some circumstances; there are weird consequences in general, but it should be fine for large eliminating inductives

#### Mario Carneiro (Mar 29 2019 at 21:45):

In particular, lean seems to have no trouble with the structure you gave, if you use an inductive instead:

inductive {u} foo (α : Sort u) : Sort u | mk : α → foo

#### Reid Barton (Mar 29 2019 at 21:45):

Oh interesting

#### Reid Barton (Mar 29 2019 at 21:47):

It only generates a small eliminator, though

#### Mario Carneiro (Mar 29 2019 at 21:50):

ah yes, that's the weird consequence

#### Mario Carneiro (Mar 29 2019 at 21:51):

that's why the `structure`

won't work, of course

Last updated: Dec 20 2023 at 11:08 UTC