Zulip Chat Archive

Stream: new members

Topic: Problem with universe levels


view this post on Zulip 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 | ai, 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.

view this post on Zulip 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 ? ?)

view this post on Zulip Scott Morrison (May 22 2020 at 01:51):

You've introduced some type β.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Daniel Fabian (May 22 2020 at 01:54):

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

view this post on Zulip 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?

view this post on Zulip Jalex Stark (May 22 2020 at 02:00):

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

view this post on Zulip 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

view this post on Zulip 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\$$ .

view this post on Zulip Jalex Stark (May 22 2020 at 02:06):

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

view this post on Zulip Jalex Stark (May 22 2020 at 02:06):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:07):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:07):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:08):

but my examples still look like N x N because easy

view this post on Zulip Daniel Fabian (May 22 2020 at 02:09):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:09):

take a subset thereof

view this post on Zulip Daniel Fabian (May 22 2020 at 02:09):

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

view this post on Zulip Jalex Stark (May 22 2020 at 02:09):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:10):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:10):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:10):

it may not be expressible as a product

view this post on Zulip Daniel Fabian (May 22 2020 at 02:10):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:11):

(or more than 2 of course)

view this post on Zulip 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)

view this post on Zulip Daniel Fabian (May 22 2020 at 02:12):

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

view this post on Zulip Jalex Stark (May 22 2020 at 02:12):

So you want something with this type signature?

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:13):

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

view this post on Zulip 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 β

view this post on Zulip Daniel Fabian (May 22 2020 at 02:14):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:14):

because the rules are something like this:

view this post on Zulip 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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:14):

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

view this post on Zulip Daniel Fabian (May 22 2020 at 02:16):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 22 2020 at 04:16):

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

view this post on Zulip 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

view this post on Zulip 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 _)

view this post on Zulip 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 | ai, 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 22 2020 at 19:19):

the notation for set difference is Ω - A

view this post on Zulip 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