Universes

Stream: lean4

[Calvin Lee]

Can I use a type with two different universes in the same declaration?
e.g. if I have def foo {m : Type u -> Type v} can I use m with two different universes in the same formula?

[Kyle Miller]

If they're different m's, then yes. You can even be explicit with universes if needed. Here's setting u=0 and v=1: foo.{0, 1}. This notation works with universe variables, too.

[Floris van Doorn]

In the definition of foo you cannot use m with a different universe level: you only have one m that has type Type u -> Type v, and u and v are fixed in the definition of foo.
After you have declared foo you can use it with u and v instantiated however you want.

[Calvin Lee]

Is there any way to make a tuple of items in two different universes? e.g. could I have def foo {m : Type u -> Type v} {a : Type u} ... : Option (m a, a) because I'm trying to do something like this and getting some type errors

[Kyle Miller]

(deleted)

[Mario Carneiro]

I think you want Option (m a × a)

[Mario Carneiro]

and this should work even if m a and a are in different universes

[Floris van Doorn]

If you have a pair, you can just take a product.
If you need a sequence with n elements, this gets inconvenient, but it is possible with Ulift.

[Kind Bubble]

I want my definition of category to depend on a choice of universe or something like that. Here's what I've got going right now:

notation "("  x  ":"  X  ")" "↦" F => (fun (x : X) => F)
notation "Σ" "(" X ":" A ")" ":" F => Σ' (X : A), F
notation "Π" "(" X ":" A ")" ":" F => forall (X : A), F
notation "*" => Unit.unit
notation "⊛" => Unit
notation x "==" y => Σ(_:x=y):⊛

def Cat :=
Σ(Obj:Type 1):
Σ(Hom:Π(_:Obj):Π(_:Obj):(Type 1)):
Σ(Id:Π(X:Obj):(Hom X X)):
Σ(Comp:Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(_:Hom X Y):Π(_:Hom Y Z):(Hom X Z)):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Comp X Y Y) f (Id Y) == f):
Σ(_:Π(X:Obj):Π(Y:Obj):Π(f:Hom X Y):(Comp X X Y) (Id X) f == f):
Σ(_:Π(W:Obj):Π(X:Obj):Π(Y:Obj):Π(Z:Obj):Π(f:Hom W X):Π(g:Hom X Y):Π(h:Hom Y Z):(Comp W X Z) f (Comp X Y Z g h) == Comp W Y Z (Comp W X Y f g) h):
⊛

As you can see, Cat is a 7-tuple. I hope my notation isn't too purist.

But I would like to switch Type 1 for something more general. How would I make it depend on a universe?

[Adam Topaz]

What happens if you replace the 1s with _? Or with universe parameters?

[Adam Topaz]

Also, what's the reason for introducing these notations?

[Kind Bubble]

Adam Topaz said:

What happens if you replace the 1s with _? Or with universe parameters?

I don't know about this yet. How does that work? And what is the most general option?

[Adam Topaz]

An underscore will be an unspecified universe parameter, making your definition universe polymorphic.

[Kind Bubble]

Adam Topaz said:

An underscore will be an unspecified universe parameter, making your definition universe polymorphic.

ok this is good.

[Kind Bubble]

Kind Bubble said:

Adam Topaz said:

An underscore will be an unspecified universe parameter, making your definition universe polymorphic.

ok this is good.

And this will work for any universe now? Is the underscore the most general option?

[Adam Topaz]

An underscore will be (essentially) equivalent to introducing arbitrary universe variables and replacing the 1s with those variables.

[Adam Topaz]

If you want to specify the universe parameters in a certain order, which can be useful sometimes (particularly in category theory!!) then you should introduce and use those variables explicitly

[Kind Bubble]

Adam Topaz said:

An underscore will be (essentially) equivalent to introducing arbitrary universe variables and replacing the 1s with those variables.

Ok thanks for your help. This is good.

[James Gallicchio]

You can also explicitly introduce universes with the def Cat.{u,v} := ... syntax, using u and v as levels like Type u and Type v. The main advantage of doing so is that the _ might be filled in with concrete universe levels (if something constrains them to a concrete level), whereas the explicit universes will raise a type error if accidentally constrained somehow.