Share  Bookmark

 Download from



 Funded by

[1] Steve Awodey and Andrej Bauer. Propositions as [types]. Journal of Logic and Computation, 14(4):447{ 471, 2004. doi: 10.1093/logcom/14.4.447.
[2] Steve Awodey and Michael Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146:45{55, 2009. doi: 10.1017/S0305004108001783.
[3] Robert Lee Constable. Constructive mathematics as a programming logic I: Some principles of theory. In Annals of Mathematics, volume 24, pages 21{37. Elsevier Science Publishers, B.V. (NorthHolland), 1985. Reprinted from Topics in the Theory of Computation, Selected Papers of the International Conference on Foundations of Computation Theory, FCT '83.
[4] Radu Diaconescu. Axiom of choice and complementation. Proc. Amer. Math. Soc., 51:176{178, 1975. doi: 10.1090/S0002993919750373893X.
[5] Michael P. Fourman and Andre Scedrov. The \world's simplest axiom of choice" fails. Manuscripta Math., 38(3):325{332, 1982. doi: 10.1007/BF01170929.
[6] Michael Hedberg. A coherence theorem for MartinLof's type theory. Journal of Functional Programming, 8(4):413{436, 1998. doi: 10.1017/S0956796898003153.
[7] Martin Hofmann and Thomas Streicher. The groupoid interpretation of type theory. In Venice Festschrift, pages 83{111. Oxford University Press, 1996.
[8] William A. Howard. The formulasastypes notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479{ 490. Academic Press, 1980.
[9] Nicolai Kraus. A direct proof of Hedberg's theorem, March 2012. Blog post at homotopytypetheory. org/2012/03/30.
[10] Nicolai Kraus. The truncation map j j : N ! kN k is nearly invertible, October 2013. Blog post at homotopytypetheory.org/2013/10/28.