Define something that varies over all types

Stream: new members

[Aatman Supkar]

How do I write something down that varies over literally all types? For example, x : <Syntax> such that x can vary over any type at all. Strictly speaking I don't think I need such an x in my work, but it did make me curious as to how one would go about doing that.

[Julian Berman]

Are you asking about variable {T : Type} (x : T)?

[Julian Berman]

(Specifically that says "let T be a type that we say nothing else about, and x is a term of type T.")

[Aatman Supkar]

Is that what it says? Does it not mean that T is a term of type Type?

[Aaron Liu]

Types Terms of type Type are types

[Julian Berman]

Terms (a typo I'm sure)

[Aaron Liu]

Examples: Nat, List Nat, Real, and Localization ((nonZeroDivisors Int).map (Int.castRingHom (Zsqrtd (-3)))) all have type Type.

[Aatman Supkar]

So Type u where u is a universe is not a type? What about propositions, which have type Prop? I've always understood them to be types, whose terms are proofs of the propositions...

[Riccardo Brasca]

There is a difference between being "a type", with lowercase t, and Type.

[Riccardo Brasca]

Being "a type" is not a super formal notion, we usually say that T is a type if T has terms, so t : T makes sense.

[Riccardo Brasca]

Very often this means that T : Type, but now always. Note that in Lean (practically) everything is a term, so (practically) everything has its own type, but not everything is a type. For example the term 2 is not a type.

[Riccardo Brasca]

The subtle question is what is the type of the term Type, but depending on what you are interested in you can safely ignore this question at the beginning.

[Edward van de Meent]

i guess in that sense, writing down something which varies over all "types" rather than Types would amount to something like {T : Sort u} as a parameter

[Riccardo Brasca]

One can quantify over all T : Type without any problem. What cannot be done is quantify over all universes.

[Aaron Liu]

You can do a sort of restricted quantification with universe polymorphism, but it's not quite the same.

[Aatman Supkar]

Riccardo Brasca said:

The subtle question is what is the type of the term Type, but depending on what you are interested in you can safely ignore this question at the beginning.

Is it correct to guess from this that while Type as a term also has its type Type 1, I can't create terms of type Type 1 other than Type?

[Riccardo Brasca]

Why not?

inductive SuperNat : Type 8 where
  | Superzero : SuperNat
  | Supersucc : SuperNat → SuperNat

is an example of a type of type Type 8 (that is basically a copy of the natural numbers).

[Riccardo Brasca]

More concretely, Type → Type has type Type 1

[Aatman Supkar]

Aaron Liu said:

You can do a sort of restricted quantification with universe polymorphism, but it's not quite the same.

Okay, I take it as a no to my original question.

Might I ask, in that case, when trying to define something that works for every 'reasonable' input, what do I let my input vary over? Type u with a universe u declaration or something?

[Aaron Liu]

Yes

[Riccardo Brasca]

We can give a better answer if you have a precise question. If you are thinking about universal properties this is something not completely trivial to solve for example.

[Aaron Liu]

Aatman Supkar said:

Might I ask, in that case, when trying to define something that works for every 'reasonable' input, what do I let my input vary over? Type u with a universe u declaration or something?

It would be better if you were to give an example.

[Aatman Supkar]

Nothing in mind, in particular. This question was born out of pure curiosity, not much with a particular goal in mind. I'd imagine that people want to make algebraic structures like rings over their favourite type, though. What do they do?

[Aaron Liu]

You can look at the source code for docs#Ring.

[Aaron Liu]

Ring is

universe u v
-- 91 lines omitted
/-- A `Ring` is a `Semiring` with negation making it an additive group. -/
class Ring (R : Type u) extends Semiring R, AddCommGroup R, AddGroupWithOne R

[Riccardo Brasca]

What happens here is that Lean actually creates a family of classes, Ring.{u}, one for each universe u. This is not exactly the same as having one class that allows the universe to vary, but in practice it works like that.

[Jireh Loreaux]

Riccardo Brasca said:

Being "a type" is not a super formal notion

Is it not? I would have said: t is a type if t : Type u for some universe u. No?

[Riccardo Brasca]

I say that T is a type if T has terms, so 1+1=2 is a type for me (so Sort u rather than Type u is probably a formal translation of what I have in mind for "being a type")

[Riccardo Brasca]

By "not a super formal notion" I mean that we cannot write in Lean T is a type

[Edward van de Meent]

is Empty a type then? :upside_down:

[Riccardo Brasca]

Ahahah, well spotted. T is a type if I can write t : T.

[Riccardo Brasca]

Like variable (t : False).

[Jireh Loreaux]

Lean agrees that our definitions coincide :wink:

variable {t : Sort u} {x : t}

Although, for newcomers both of our definitions might be confusing due to docs#CoeSort, as this works, but more is happening than is visible from the source.

import Mathlib.Data.Set.Basic

variable {t : Type u} (s : Set t)

#check (s : Type u)

variable (x : s)

[Matt Diamond]

maybe worth noting that you can also do Type* and have Lean do the universe polymorphism for you

[Philippe Duchon]

Riccardo Brasca said:

I say that T is a type if T has terms

I find this formulation a bit confusing - wouldn't it mean that uninhabited types are not types? (of course, in some contexts, even False has terms)