Name
Abstract | ||
|---|---|---|
In this paper we present and study a categorical formulation of the W-types of Martin-Löf. These are essentially free term algebras where the operations may have finite or infinite arity. It is shown that W-types are preserved under the construction of sheaves and Artin gluing. In the proofs we avoid using impredicative or nonconstructive principles. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1016/S0168-0072(00)00012-9 | Annals of Pure and Applied Logic |
Keywords | Field | DocType |
primary: 03B15,03G30,18A15,18B25,18C15,18F20,secondary: 18C50,68N18 | Discrete mathematics,Intuitionistic type theory,Arity,Algebra,Categorical variable,Mathematical proof,Impredicativity,Mathematics | Journal |
Volume | Issue | ISSN |
104 | 1-3 | 0168-0072 |
Citations | PageRank | References |
40 | 3.35 | 4 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ieke Moerdijk | 1 | 133 | 21.41 |
| Erik Palmgren | 2 | 233 | 43.17 |