here are fixed-length vectors defined in terms of naturals
Vec: Type → ℕ → Type
Vec A 0 = ⊤
Vec A (S n) = A × Vec A n
nil: (A: Type) → Vec A 0
nil 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 () = Pn
match A P Pn Pc (S n) (a, as) = Pc n a as
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 https://github.com/UniMath/UniMath/blob/master/UniMath/Induction/W/Core.v and they define W types like this
Definition W := ∑ (X : algebra_ob F), is_initial X.
I'm going down a rabbit hole of Spain without the S
Look look look
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
@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
A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.