## 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