Skip to main content
14 votes
Accepted

What are well-founded inductive types?

"Well-founded" and "inductive" mean roughly the same thing. I think the reason different terminology tends to get used for W-types is that their definition looks similar to ...
Dan Doel's user avatar
  • 982
14 votes
Accepted

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

The answer is no. According to Anton Setzer's PhD thesis: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe: Aczel has shown in [Acz77] that Martin-Löf’s type theory ...
Couchy's user avatar
  • 2,231
6 votes
Accepted

Parameterized Datatypes in a Universe à la Tarski?

Arg : (c : Code) -> (El c -> Desc) -> Desc Are you sure this is what you mean? I think the usual constructor is closer to the following: ...
gallais's user avatar
  • 1,166

Only top scored, non community-wiki answers of a minimum length are eligible