here are fixed-length vectors defined in terms of naturals

``Vec: Type → ℕ → TypeVec A 0 = ⊤Vec A (S n) = A × Vec A nnil: (A: Type) → Vec A 0nil A = ()cons: (A: Type) → (n: ℕ) → (a: A) → Vec A n → Vec A (S n)cons A n a as = (a, as) as A × Vec A (S n)match: (A: Type)  → (P: (n: ℕ) → Vec A n → Type)  → P 0 (nil A)  → ((n: ℕ) → (a: A) → (as: Vec A n)    → P (S n) (cons A n a as))  → (n: ℕ) → (Vec A n)match A P Pn Pc 0 () = Pnmatch A P Pn Pc (S n) (a, as) = Pc n a as``

I've always thought that vectors are more "complex" than lists because they have a length index but I don't think I can define parametrized, non-indexed lists with only the power of naturals (and maybe equality)

lists in terms of naturals and pairs

``List: Type → TypeList A = (n: ℕ) × Vec n Anil: (A: Type) → List Anil A = (0, ())cons: (A: Type) → A → List A → List Acons A a (n, as) = (S n, (a, as))``

Well what do you know! We've got lists

Can I encode W types using nothing but pairs, naturals, and equality? I feel like if it were possible the HoTT book would've already done it
I think there's something more to W types than just naturals. Like okay, lists and vectors are just linear nested tuples, I bet trees can be encoded as branching nested tuples, but W types can have infinite branches, and I don't think that's something I can do

I'm looking at this github.com/UniMath/UniMath/blo and they define W types like this

``Definition W := ∑ (X : algebra_ob F), is_initial X.``

???

``Local Notation F := (polynomial_functor A B).``

That doesn't help

Look look look
cse.chalmers.se/research/group
Chapter 16
There's these things called "general trees" and a) you can defined W types in them but also b) they can be defined by W types

Whoa there's a lot more in this book
It's basically... all of MLTT

@ionchy Are sigma types allowed? Then it's Sigma n : N . Vec n a

@turion :o I think that'll work...

@ionchy With the power of container types 💪 (or polynomial functors, whatever you prefer)

@ionchy You probably need some class of ordinals for W types because you can use them to define some pretty fancy classes of ordinals IIRC. Naturals probably don't suffice.

@ionchy For W-types you need some kind of fixpoint. E.g. inductive types. But if you're already allowed naturals then maybe inductive types are OK?

@ionchy I guess in the HoTT book they just didn't want to bother with inductive types because HITs weren't quite ready yet

@ionchy Ah yes, the W type is just the initial algebra of a polynomial functor.

lists in terms of naturals and pairs