# Zulip Chat Archive

## Stream: new members

### Topic: prod and pprod

#### Horatiu Cheval (Apr 11 2021 at 05:45):

What's the reason, or the use-case of having distinct Type-valued and general Sort-valued analogous definitions like `prod`

/`pprod`

and the like? I don't understand why one doesn't have just the more general `pprod`

and uses that in all situations, even when only `Types`

are involved; it seems like in principle you could do that. So, what's the reason for this design? Thanks in advance!

#### Mario Carneiro (Apr 11 2021 at 05:51):

`pprod`

is a straight generalization of `prod`

, so it can be used anywhere `prod`

is, in principle. But the target universe of `pprod`

is `Sort (max 1 u v)`

which can be difficult to unify with other things

#### Mario Carneiro (Apr 11 2021 at 05:53):

In particular, there is no solution to the equation `Sort (max 1 u v) = Type ?`

, so an arbitrary `pprod`

will not be accepted where a `Type ?`

is required

#### Mario Carneiro (Apr 11 2021 at 05:54):

```
example {α β} := set (α × β) -- ok
example {α β} := set (pprod α β) -- fail
```

#### Horatiu Cheval (Apr 11 2021 at 06:09):

I don't know much about how unification works, so I'm just speaking intuitively and I'm probably wrong, but since `max 1 u v`

is $\ge 1$, isn't it always a `Type`

, namely `Type (max 1 u v) - 1`

, so to say? Isn't `Type u`

just a notation for `Sort (u + 1)`

?

#### Horatiu Cheval (Apr 11 2021 at 06:11):

Or is this not the way things work?

#### Mario Carneiro (Apr 11 2021 at 06:15):

The problem is that `-1`

isn't a thing

#### Mario Carneiro (Apr 11 2021 at 06:15):

the syntax of levels contains `0`

, `_ + 1`

, `max _ _`

, `imax _ _`

and variables

#### Mario Carneiro (Apr 11 2021 at 06:16):

In that language, there is no term representing `max 1 u v - 1`

, even though that is a natural number

#### Horatiu Cheval (Apr 11 2021 at 06:19):

I knew I couldn't write `-1`

there in Lean, but I thought that maybe internally, in the implementation Lean could do other natural number manipulations besides what I'm allowed to write in universe arguments. But I get it now, thanks!

#### Mario Carneiro (Apr 11 2021 at 06:22):

The unification algorithm, when faced with the goal `max 1 u v = ? + 1`

, has to find an actual term for `?`

making the two sides equal, and there is no such term (there is if you substitute `u+1`

for `u`

and `v+1`

for `v`

, though)

#### Mario Carneiro (Apr 11 2021 at 06:23):

that impoverished grammar is actually baked into the kernel (and external typecheckers), so the elaborator isn't allowed to do magic with it

#### Horatiu Cheval (Apr 11 2021 at 06:25):

So universes are represented in the kernel as actual terms in the language you described, not as some generic natural number datatype, right?

#### Mario Carneiro (Apr 11 2021 at 06:25):

right

#### Mario Carneiro (Apr 11 2021 at 06:25):

They can't be generic natural numbers anyway, because they have variables in them, `u`

and `v`

#### Mario Carneiro (Apr 11 2021 at 06:26):

In fact, if these were numbers there would be no problem: `max 1 0 4 = ? + 1`

has a solution

#### Mario Carneiro (Apr 11 2021 at 06:27):

They can't be arbitrary terms of type `nat`

either, because that would be inconsistent (which is a fun paradox)

#### Mario Carneiro (Apr 11 2021 at 06:30):

The paradox, by the way, involves the question of what universe `λ n, Type n`

lives in; it's not hard to go from that to girard's paradox

#### Horatiu Cheval (Apr 11 2021 at 06:31):

Indeed, thank you, I think all is clear now with regards to unification

#### Horatiu Cheval (Apr 11 2021 at 06:33):

The paradox does seem interesting, I'll try to see how to get to Girard's paradox from there

Last updated: Dec 20 2023 at 11:08 UTC