use ∀ k : α, ∃ (W : Type) ... to get a "union" type?

Stream: new members

[Malvin Gattinger]

Is the following doable? I think I want a Σ type but am not sure whether there is some fundamental problem I am missing. Do I need choice for this? (The property > 10 part is just to make this toy example.)

structure thing (W : Type) : Type := (property : W → ℕ)

lemma toy { α : Type } :
  ( ∀ k : α, ∃ (W : Type) (t : thing W) (w : W), t.property w > 10 )
    → (∃ (union : Type) (b : thing union) (v : union), b.property v > 100 ) :=
begin
  intro lhs,
  -- get something like "map : α → Type" from lhs ??
  -- let "union" be the product of all the "map α" ??
  -- define b by saying that "property" is the sum of all the given "property"
  -- let w be the tuple(?) of all the w ...
  sorry,
end

[Eric Wieser]

The hypothesis is useless because α may be empty

[Eric Wieser]

I think you can prove your lemma with exact ⟨unit, ⟨function.const 101⟩, (), by linarith⟩

[Eric Wieser]

Which suggests to me it doesn't state what you want it to say either

[Malvin Gattinger]

oh, right. Indeed then it does not say what I want ;-) Thank you!

[Eric Wieser]

If you want a particular choice of thing union that satisfies more than just the > 100 property in the statement,then you probably want a def with sigma not a lemma with exists

[Malvin Gattinger]

I now have a separate definition and a lemma about the definition. :rocket: Would you (or someone else) have recommendations to improve this?

structure thing (W : Type) : Type := (property : W → ℕ)

def unionOfThings { α : Type } :
  ( Π k : α, Σ (W : Type), thing W )
    → ( Σ (union : Type), thing union ) :=
begin
  intro collection,
  -- let "union" be the sum of all the W indexed by k
  use Σ k : α, (collection k).fst,
  -- define newt: "property" is the corresponding "property" of the old t
  have newt : thing (Σ (k : α), (collection k).fst), {
    fconstructor,
    intro world,
    cases world with k tw,
    exact (collection k).snd.property tw,
  },
  use newt,
end

lemma unionOfThingsPreservesMinimum { α : Type } { N : ℕ } { collection : (Π k : α, Σ (W : Type), thing W) } :
  ( ∀ k X, (collection k).snd.property X > N)  → ( ∀ X, (unionOfThings collection).snd.property X > N) :=
begin
  intro hyp,
  intro X,
  cases X,
  tauto,
end

[Malvin Gattinger]

For example, I am wondering whether it would be possible and better to say in the def already that union should be indexed by the same α.

[Eric Wieser]

I would be tempted to not have the def return a sigma type at all

[Eric Wieser]

structure thing (W : Type) : Type := (property : W → ℕ)

def unionOfThings { α : Type } (collection : α → Σ (W : Type), thing W) : thing (Σ k : α, (collection k).fst) :=
{ property :=
  λ world, (collection world.fst).snd.property world.snd }

[Eric Wieser]

This probably exists already without the thing structure (replacing thing W with W → ℕ.

[Malvin Gattinger]

Ah, thank you! I was wondering whether I want a "thing of sigmas" instead of a "sigma of things".

[Eric Wieser]

What you had was both

[Malvin Gattinger]

ah, a sigma of things of sigmas :laughter_tears: ...

[Malvin Gattinger]

And I would guess that for simple functions this can be done much simpler. I am mostly doing this for practice - my real things have multiple propertys.