Is pSet equivalent to W_type id?

Stream: new members

[Matt Diamond]

I'm wondering if pSet is equivalent to W_type (id : Type → Type). They seem similar: both are a fixed point of X ↦ Σ a : Type, a → X and represent (or can represent) well-founded trees. However, I've been struggling a bit with how to prove this equivalence, so I'm wondering if the relation isn't as simple as it looks.

[Chris Hughes]

They are equivalent. Here is a proof. I defined to_pSet in two different ways so you can see how to do it directly from the recursor.

import data.W.basic
import set_theory.zfc

def to_pSet : W_type id → pSet
| (W_type.mk α x) := pSet.mk α (λ a, to_pSet (x a))

def to_pSet2 (x : W_type id) : pSet :=
W_type.rec_on x (λ α x ih, pSet.mk α ih)

def to_W_type : pSet → W_type id
| (pSet.mk α x) := W_type.mk α (λ a, to_W_type (x a))

lemma to_pSet_to_W_type (x : pSet) : to_pSet (to_W_type x) = x :=
begin
  induction x with α x ih,
  simp [ih, to_pSet, to_W_type]
end

lemma to_W_type_to_pSet (x : W_type id) : to_W_type (to_pSet x) = x :=
begin
  induction x with α x ih,
  simp [ih, to_pSet, to_W_type]
end

[Violeta Hernández]

Oh wow

[Violeta Hernández]

I have two questions

• could we redefine pSet as W_type id and take advantage of existing API on W_type?
• is there a similar equivalence on pgame?

[Violeta Hernández]

I think maybe pgame might be equivalent to W_type (sum.elim id id : Type ⊕ Type → Type)

[Violeta Hernández]

Oh wait, are W-types just a formalism of inductive types?

[Eric Wieser]

There's a PR somewhere that encodes nat and list as W-types. It might be a fun project to write a metaprogram to build that sort of encoding automatically

[Matt Diamond]

@Chris Hughes I thought so! Thanks for sharing the proof.

[Matt Diamond]

Violeta Hernández said:

Oh wait, are W-types just a formalism of inductive types?

idk if you're already aware of it, but there's a paper on this topic from some familiar people: Data Types as Quotients of Polynomial Functors

(well, it's technically about polynomial functors, but it mentions W types as initial algebras)

[Matt Diamond]

Eric Wieser said:

There's a PR somewhere that encodes nat and list as W-types.

It's already in master, if you're referring to this: https://leanprover-community.github.io/mathlib_docs/data/W/constructions.html

[Matt Diamond]

I just found it interesting that pSet appears to be the most "generic" W-type, almost like the "free W-type" in a sense (though I'm sure I'm misusing terminology here)

from the viewpoint of W-types as specifying a relation between constructors and arities, pSet is the W-type where each constructor just is the arity... which makes perfect sense when you want a general concept of collections of different sizes

[Matt Diamond]

I wonder if M_type (id : Type → Type) would be like pSets for non-wellfounded set theory

[Patrick Johnson]

In #leantt section 5, Mario explains how all inductive types can be reduced to W-types (with the help of 7 more basic inductive types).

[Matt Diamond]

nice!

[Junyan Xu]

David Wärn proposed using docs#pfunctor.M to define non-wellfounded games but I still haven't studied the details ...