Skip to main content

Questions tagged [w-type]

A W-type is a set or type which is defined inductively in a well-founded way based on a type of “constructors” and a type of “arities”, with one constructor having a certain canonical form. As such it is a particular kind of inductive type. (from nLab)

Filter by
Sorted by
Tagged with
10 votes
1 answer
400 views

Can you build W-types out of natural numbers predicatively?

I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, ...
Ilk's user avatar
  • 547
6 votes
1 answer
250 views

Parameterized Datatypes in a Universe à la Tarski?

I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types? For context, I'm trying ...
Joey Eremondi's user avatar
10 votes
1 answer
585 views

What are well-founded inductive types?

W-types are said to be "a well-founded inductive type" that is parameterized over arities and constructors, similar to a "tree of possible constructions". On nlab, it is said that ...
ice1000's user avatar
  • 6,186