## Stream: general

### Topic: Universe of pi type

#### Sebastian Reichelt (Feb 08 2022 at 22:22):

I have a basic question about universes in Lean: Would any known inconsistency arise if the type of (x : α) → β x with α : Sort u and β : α → Sort v was simply Sort v instead of Sort (imax u v)?
(I guess the answer must be "yes" because otherwise imax wouldn't need to exist, but I'd like to be sure because it seems to be a blocker for something I would like to do.)

#### Yaël Dillies (Feb 08 2022 at 22:24):

Do you mean Sort (max u v)?

#### Sebastian Reichelt (Feb 08 2022 at 22:30):

No, max would be much "worse" than imax of course; there wouldn't be any universally quantified propositions then as far as I understand. You can interpret my question as asking if "universally quantified data" can be treated in the same way as universally quantified propositions, or equivalently if the "size" of a function could just be the "size" of its output. I hope there is not some obvious type-theoretic reason why it cannot work.

#### Reid Barton (Feb 08 2022 at 22:31):

It can't be because e.g. Type -> bool has to be bigger than Type, so at least in the same universe as Type.

#### Reid Barton (Feb 08 2022 at 22:33):

You need LEM to cook up this kind of example, I think without it a system like this might be consistent, but it would be anticlassical.

#### Reid Barton (Feb 08 2022 at 22:33):

(the key phrase is "impredicative universe")

#### Sebastian Reichelt (Feb 08 2022 at 22:40):

Thanks, I'll check that out.
Just curious, is the Type -> bool example problematic only in the presence of choice, via propDecidable or something? (Assuming LEM as you say.)

#### Reid Barton (Feb 08 2022 at 22:48):

I mean there are definitely systems with an impredicative universe out there, but they are unsuitable for mathematics in the strong sense of proving classically false statements, so I don't know that much about exactly what you can and can't put into such a theory.

#### Reid Barton (Feb 08 2022 at 22:49):

But computer scientists often don't care about classical mathematics (because they cannot compute LEM anyways), so they think it is reasonable. System F is one of these systems, I understand.

#### Sebastian Reichelt (Feb 08 2022 at 23:03):

Ah, now I understand, you are arguing that α → Bool is set-theoretically larger than α, right? I missed that, oops. :-)

#### Trebor Huang (Feb 09 2022 at 08:37):

if you do that, there cannot be more than two universes (in which case we get the CoC). Otherwise your system contains a subsystem named System $U^-$, where you can formulate Girards paradox.

#### Trebor Huang (Feb 09 2022 at 08:38):

(I haven't really checked all the axioms of $U^-$ because I simply can't remember them, so correct me if I'm wrong.)

#### Mario Carneiro (Feb 09 2022 at 09:16):

@Trebor Huang See docs#girard

#### Mario Carneiro (Feb 09 2022 at 09:19):

Oh shoot, since it's been moved to the archive I can't find it in the docs anymore. @Rob Lewis What are your thoughts on this? Can we add the mathlib archive to docgen?

#### Mario Carneiro (Feb 09 2022 at 09:19):

You can find it at an old version of the mathlib docs: https://cs.brown.edu/courses/cs1951x/docs/logic/girard.html

#### Yaël Dillies (Feb 09 2022 at 09:21):

Exactly the same happened to Bhavik and I yesterday :sweat_smile:

#### Yaël Dillies (Feb 09 2022 at 09:21):

And, yes, documentation for the archive would be great.

#### Eric Wieser (Feb 07 2023 at 14:46):

Mario Carneiro said:

Trebor Huang See docs#girard

https://leanprover-community.github.io/mathlib_docs_demo/girard.html