Issue #186

Stream: Equational

[Cody Roux]

The issue https://github.com/teorth/equational_theories/issues/186 apparently proving two very similar statements to be equivalent, up to universes. I think I might be able to handle this, but I just want to understand:

1. Do we even need this theorem?
2. What's the difference between G : Type and G : Type*? I thought that Type introduced a (single) fresh variable and Type* just did it for each variable in the telescope. Are these two things equivalent already?

[Terence Tao]

It was inspired by @Franklin Pezzuti Dyer 's comment at equational#36 , perhaps he can weigh in more on what the precise issue was?

[Daniel Weber]

Type is Type 0, while Type* is a type of any universe, so they are different

[Cody Roux]

Oh? Yea ok I can totally prove it then, though I feel like I'll need the excluded middle. I already used choice though, so...

[Franklin Pezzuti Dyer]

I didn't have a more precise issue other than just not knowing what Type* meant (and having trouble finding relevant Lean docs), and noticing that the treatment of universes across files was sometimes inconsistent.

[Cody Roux]

It's a fun exercise, at least, though of course the much harder Lowenheim-Skolem theorem in full generality is already in Mathlib (both directions, I think? Maybe just the upper one...)

[Cody Roux]

But I also should generalize the completeness theorem

[Andrés Goens]

is there any example so far where we actually need a higher universe than 0?

[Terence Tao]

One could imagine for some reason wanting to work with a magma associated to a large category, e.g., Type with the operation × is a magma. Of course the Lowenheim-Skolem (together with this simpler counterpart) tells us that we never actually need to use models this large, but one could imagine that it is sometimes convenient. (In model theory it is sometimes convenient to work with extremely saturated models constructed using large cardinals in order to get some nice symmetry and completeness properties. I doubt we will ever need this level of sophistication for our current project, but it is theoretically possible.)

[Cody Roux]

I'll prove it this weekend if I can. Seems fun

[Cody Roux]

Wait no, it's not fun at all :(

[Cody Roux]

I'm in universe hell, I'm gong to have to give up on this one... We can call in some reinforcements if we actually need the extra flexibility.