nLab semantics of W-types -- references

Categorical semantics of $\mathcal{W}$-types

The observation that the categorical semantics of well-founded inductive types ($\mathcal{W}$-types) is given by initial algebras over polynomial endofunctors on the type system:

• Peter Dybjer, Representing inductively defined sets by wellorderings in Martin-Löf’s type theory, Theoretical Computer Science 176 1–2 (1997) 329-335 $[$doi:10.1016/S0304-3975(96)00145-4$]$

• Ieke Moerdijk, Erik Palmgren, Wellfounded trees in categories, Annals of Pure and Applied Logic 104 1-3 (2000) 189-218 $[$doi:10.1016/S0168-0072(00)00012-9$]$

Further discussion:

• Michael Abbott, Thorsten Altenkirch, Neil Ghani, Containers: Constructing strictly positive types, Theoretical Computer Science 342 1 (2005) 3-27 $[$doi:10.1016/j.tcs.2005.06.002$]$

• Benno van den Berg, Ieke Moerdijk, $W$-types in sheaves [arXiv:0810.2398]

Generalization to inductive families (dependent $\mathcal{W}$-types):

• Nicola Gambino, Martin Hyland, Wellfounded Trees and Dependent Polynomial Functors, in: Types for Proofs and Programs TYPES 200, Lecture Notes in Computer Science 3085, Springer (2004) $[$doi:10.1007/978-3-540-24849-1_14$]$

• Michael Abbott, Thorsten Altenkirch, Neil Ghani: Representing Nested Inductive Types using W-types, in: Automata, Languages and Programming, ICALP 2004, Lecture Notes in Computer Science, 3142, Springer (2004) $[$doi:10.1007/978-3-540-27836-8_8, pdf$]$

  exposition: Inductive Types for Free – Representing nested inductive types using W-types, talk at ICALP (2004) $[$pdf$]$

Generalization to homotopy-initial algebras as categorical semantics for $\mathcal{W}$-types in homotopy type theory:

• Steve Awodey, Nicola Gambino, Kristina Sojakova, Inductive types in homotopy type theory, LICS’12: (2012) 95–104 $[$arXiv:1201.3898, doi:10.1109/LICS.2012.21, Coq code$]$

• Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 $[$arXiv:1307.2765, doi:10.1017/S0960129514000516$]$

• Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras, ACM SIGPLAN Notices 50 1 (2015) 31–42 $[$arXiv:1402.0761, doi:10.1145/2775051.2676983$]$

• Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory, Journal of the ACM 63 6 (2017) 1–45 $[$arXiv:1504.05531, doi:10.1145/3006383$]$

• Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory, Mathematical Structures in Computer Science 25 Special Issue 5: From type theory and homotopy theory to Univalent Foundations of Mathematics (2015) 1100-1115 [arXiv:1307.2765, doi:10.1017/S0960129514000516]

Towards combining generalization to dependent and homotopical W-types:

• Christian Sattler, On relating indexed W-types with ordinary ones, in Types for Proofs and Programs – TYPES 2015 (2015) 71-72 $[$pdf, pdf$]$