# Zulip Chat Archive

## Stream: new members

### Topic: Problem with universe levels

#### Daniel Fabian (May 22 2020 at 01:48):

I have come across a problem where I don't quite understand why the thing I'm trying to do doesn't typecheck.

What I'm trying to do, is define a proposition that would allow me to access the components of a cartesian product (`pi`

is copied from mathlib):

```
variables {α : Type*} {π : α → Type*} {β : Type*}
def pi (i : set α) (s : Πa, set (π a)) : set (Πa, π a) := { f | ∀a∈i, f a ∈ s a }
def cartesian_product (Ω : set (Πa, π a)) :=
∃ i m, pi i m = Ω
def cartesian_product2 (Ω : set β) :=
∃ i m, pi i m = Ω
```

The first one seems to be happy, the second one not. And I don't understand; `Πa, π a`

does have a type after all. Granted in a higher universe, but why can't I write `β`

? After all, it's just a different name for an object at Type n+1.

#### Scott Morrison (May 22 2020 at 01:50):

The error message seems pretty clear:

```
type mismatch at application
pi i m = Ω
term
Ω
has type
set β : Type u_3
but is expected to have type
set (Π (a : ?m_1), ?m_2 a) : Type (max ? ?)
```

#### Scott Morrison (May 22 2020 at 01:51):

You've introduced some type `β`

.

#### Scott Morrison (May 22 2020 at 01:51):

There's no reason that type should be of the form `(Π (a : ?m_1), ?m_2 a)`

for some ?m_1 and ?m_2.

#### Daniel Fabian (May 22 2020 at 01:53):

So does that mean, that I'd never be able to write `cartesian_product \Omega`

for an `\Omega : nat \times nat`

?

#### Daniel Fabian (May 22 2020 at 01:54):

Or would I just need to write a coercion between `prod`

and `pi`

, effectively

#### Jalex Stark (May 22 2020 at 01:59):

Daniel Fabian said:

Or would I just need to write a coercion between

`prod`

and`pi`

, effectively

uh, yes?

#### Jalex Stark (May 22 2020 at 02:00):

if `a : α`

and you write `a : β`

, Lean looks for a coercion

#### Jalex Stark (May 22 2020 at 02:01):

I don't know what the word "effectively" means, you can literally make your own coercion like

```
instance : has_lift α β := sorry
```

#### Daniel Fabian (May 22 2020 at 02:04):

I see. So if I consider the product type using $\times$ to be a cons list, I can turn the position into an index and build a mapping function that way, yes? So that I can write $$N \times N \times N\$$ .

#### Jalex Stark (May 22 2020 at 02:06):

i don't have a clear picture of what you're trying to do

#### Jalex Stark (May 22 2020 at 02:06):

from your first post it sounded liek you wanted to reimplement e.g. `fst`

#### Daniel Fabian (May 22 2020 at 02:07):

Some time ago, I showed some properties of cartesian products. But n-way products and not $X^n$ kinds of products.

#### Daniel Fabian (May 22 2020 at 02:07):

So I was going to use the `pi`

construct to talk about the n-way products.

#### Daniel Fabian (May 22 2020 at 02:08):

but my examples still look like `N x N`

because easy

#### Daniel Fabian (May 22 2020 at 02:09):

The idea being, that I take points in a cartesian product

#### Daniel Fabian (May 22 2020 at 02:09):

take a subset thereof

#### Daniel Fabian (May 22 2020 at 02:09):

and now the question is, if the subset is a cartesian product in its own right

#### Jalex Stark (May 22 2020 at 02:09):

is there a reason to use a subset instead of a subtype?

#### Daniel Fabian (May 22 2020 at 02:10):

i.e. exactly a product of its projections to 1 dimension.

#### Daniel Fabian (May 22 2020 at 02:10):

yes... because the subset may not be a product

#### Daniel Fabian (May 22 2020 at 02:10):

it may not be expressible as a product

#### Daniel Fabian (May 22 2020 at 02:10):

in that case, I'd call it a union between two products

#### Daniel Fabian (May 22 2020 at 02:11):

(or more than 2 of course)

#### Jalex Stark (May 22 2020 at 02:11):

(i don't see what that has to do with sets vs types, but the set /type distinction is tangential to the core of your problem so let's set it aside)

#### Daniel Fabian (May 22 2020 at 02:12):

oh, you meant just not talking about `set xyz`

but directly `xyz`

?

#### Jalex Stark (May 22 2020 at 02:12):

So you want something with this type signature?

```
def is_product (x : set α × β) : Prop
```

#### Daniel Fabian (May 22 2020 at 02:13):

No reason, I just only started and have a bit of trouble writing down the definitions.

#### Jalex Stark (May 22 2020 at 02:13):

and you want it to be true if `x`

is a product of some `y : set α`

and `z : set β`

#### Daniel Fabian (May 22 2020 at 02:14):

Yes, kind of. But I need it to talk about n dimension, not 2.

#### Daniel Fabian (May 22 2020 at 02:14):

because the rules are something like this:

#### Daniel Fabian (May 22 2020 at 02:14):

union between two n-way products is a product if they agree on all but 1 dimension

#### Daniel Fabian (May 22 2020 at 02:14):

and it's shown by induction on the number of dimensions

#### Daniel Fabian (May 22 2020 at 02:16):

it almost feels like `pi`

is too general, but pair too restrictive.

#### Mario Carneiro (May 22 2020 at 04:05):

@Daniel Fabian I don't think this is expressing what you want. (That said I'm not entirely certain what you want.) It sounds like you want to talk about "types that are pi-types" in a more general sense than literally pi's, for example products should qualify. One way you could formalize this is that it is a type equipped with an equiv to a pi-type

#### Mario Carneiro (May 22 2020 at 04:15):

```
import data.equiv.basic
@[class] def {u v w} is_a_pi (α : Type u) (ι : out_param (Type v)) (β : out_param (ι → Type w)) :
Type (max u v w) := α ≃ Π i, β i
instance pi.is_a_pi {ι : Type*} (β : ι → Type*) : is_a_pi (Π i, β i) ι β := equiv.refl _
instance prod.is_a_pi (α β : Type*) : is_a_pi (α × β) bool (λ b, cond b α β) :=
⟨λ ⟨a, b⟩, λ i, bool.cases_on i b a, λ f, (f tt, f ff),
λ ⟨a, b⟩, rfl, λ f, funext $ by rintro ⟨⟩; refl⟩
```

#### Mario Carneiro (May 22 2020 at 04:16):

Are you trying to define "cylinder sets" as used in e.g. the product topology?

#### Mario Carneiro (May 22 2020 at 04:22):

After reading this thread again, I think what you want is what you first posted:

```
def cartesian_product (Ω : set (Πa, π a)) :=
∃ i m, pi i m = Ω
```

The `cartesian_product2`

version doesn't make any sense because "being a product" doesn't make sense in the abstract, without a coordinatization, to say what it means for a set to be "axis-aligned". What is true is that given a set that satisfies `cartesian_product`

, you can construct another pi type (which we view as the subset) which is bijective with the original set

#### Mario Carneiro (May 22 2020 at 04:48):

```
import tactic
variables {α : Type*} {π : α → Type*} {β : Type*}
def pi (s : Πa, set (π a)) : set (Πa, π a) := { f | ∀a, f a ∈ s a }
def cartesian_product (Ω : set (Πa, π a)) := ∃ s, pi s = Ω
def proj (Ω : set (Πa, π a)) (a:α) : set (π a) := { x | ∃ f ∈ Ω, (f : Π a, π a) a = x}
theorem cartesian_product.is_proj {Ω : set (Πa, π a)} (H : cartesian_product Ω) :
pi (proj Ω) = Ω :=
begin
refine set.ext (λ x, _),
rcases H with ⟨s, rfl⟩,
simp [pi, proj],
refine ⟨λ h a, _, λ h a, ⟨_, h, rfl⟩⟩,
obtain ⟨f, h, e⟩ := h a,
rw ← e, apply h,
end
def pi.equiv (s : Πa, set (π a)) : pi s ≃ Π a, s a :=
⟨λ f a, ⟨f.1 a, f.2 a⟩, λ f, ⟨λ a, (f a).1, λ a, (f a).2⟩,
λ ⟨f, h⟩, rfl, λ f, funext $ λ a, by dsimp; cases f a; refl⟩
def sub_pi {Ω : set (Πa, π a)} (H : cartesian_product Ω) : Ω ≃ Π a, proj Ω a :=
equiv.trans (by rw H.is_proj) (pi.equiv _)
```

#### Mario Carneiro (May 22 2020 at 05:04):

By the way, if you are wondering why I took out the first argument of `pi`

, it's because it is unnecessary:

```
def pi' (i : set α) (s : Πa, set (π a)) : set (Πa, π a) := { f | ∀a∈i, f a ∈ s a }
theorem pi'_eq_pi (i : set α) (s : Πa, set (π a)) :
pi' i s = pi (λ a, {b : π a | a ∈ i → b ∈ s a}) := rfl
```

#### Daniel Fabian (May 22 2020 at 11:45):

@Mario Carneiro this is great, I think I can express my notion of a subspace. From taking a quick glance at cylinder sets, I think they may be related. Not quite sure they are the same thing.

At any rate, the definition is easy now:

```
def subspace (Ω : set (Πa, π a)) (A : set (Πa, π a)) :=
A ⊆ Ω ∧ cartesian_product Ω ∧ cartesian_product A
def co_subspace (Ω : set (Πa, π a)) (A : set (Πa, π a)) := subspace Ω (Ω\A)
```

Assuming `Ω\A`

stands for set difference

#### Mario Carneiro (May 22 2020 at 19:19):

the notation for set difference is `Ω - A`

#### Daniel Fabian (May 22 2020 at 20:29):

Is `-`

the symm diff? Because `\`

seemed to work just fine...

At any rate it took me a while to get a mental model for what Pi types really are.

It's really straight-forward when thinking about propositions, but at the signature level, I didn't get it at first.

Until I realised, that the Pi construct is very similar to lambda abstraction, just at the signature level and that it allows for arbitrary computation to happen.

But it clicked now!

Last updated: May 13 2021 at 05:21 UTC