Inductive types in
Homotopy Type Theory, written with S. Awodey and K.
Sojakova Proceedings of the 2012 27th
Annual ACM/IEEE Symposium on Logic in Computer Science (LICS
2012), pp. 95-104.
The related Coq code is available on here.
Postal address: School of Mathematics, University of
Leeds, Leeds LS2 9JT, United Kingdom Phone: +44 (0)113 343 51 43 Email: n.gambino AT leeds.ac.uk Web: http://www.maths.leeds.ac.uk/~pmtng Office: Room 9.15, School of Mathematics
This page was last updated on 9th June
2021 by Nicola Gambino.