Problem with universe levels

Stream: new members

[Daniel Fabian]

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]

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]

You've introduced some type β.

[Scott Morrison]

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]

So does that mean, that I'd never be able to write cartesian_product \Omega for an \Omega : nat \times nat?

[Daniel Fabian]

Or would I just need to write a coercion between prod and pi, effectively

[Jalex Stark]

Daniel Fabian said:

Or would I just need to write a coercion between prod and pi, effectively

uh, yes?

[Jalex Stark]

if a : α and you write a : β, Lean looks for a coercion

[Jalex Stark]

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

instance : has_lift α β := sorry

[Daniel Fabian]

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]

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

[Jalex Stark]

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

[Daniel Fabian]

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

[Daniel Fabian]

So I was going to use the pi construct to talk about the n-way products.

[Daniel Fabian]

but my examples still look like N x N because easy

[Daniel Fabian]

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

[Daniel Fabian]

take a subset thereof

[Daniel Fabian]

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

[Jalex Stark]

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

[Daniel Fabian]

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

[Daniel Fabian]

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

[Daniel Fabian]

it may not be expressible as a product

[Daniel Fabian]

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

[Daniel Fabian]

(or more than 2 of course)

[Jalex Stark]

(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]

oh, you meant just not talking about set xyz but directly xyz?

[Jalex Stark]

So you want something with this type signature?

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

[Daniel Fabian]

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

[Jalex Stark]

and you want it to be true if x is a product of some y : set α and z : set β

[Daniel Fabian]

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

[Daniel Fabian]

because the rules are something like this:

[Daniel Fabian]

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

[Daniel Fabian]

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

[Daniel Fabian]

it almost feels like pi is too general, but pair too restrictive.

[Mario Carneiro]

@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]

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]

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

[Mario Carneiro]

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]

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]

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]

@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]

the notation for set difference is Ω - A

[Daniel Fabian]

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!