refs.bib

@incollection{bishop:numerical:language,
title = "Mathematics as a Numerical Language",
editor = "A. Kino and J. Myhill and R.E. Vesley",
booktitle = "Intuitionism and Proof Theory: Proceedings of the Summer Conference at Buffalo N.Y. 1968",
publisher = "Elsevier",
year = "1970",
volume = "60",
pages = "53--71",
series = "Studies in Logic and the Foundations of Mathematics ",
issn = "0049-237X",
doi = "10.1016/S0049-237X(08)70740-7",
author = "Errett Bishop"
}

@misc{kraus:truncation:invertible,
  author = {Nicolai Kraus},
  title = {The Truncation Map |_| : ℕ -> ‖ℕ‖ is nearly Invertible},
  month = oct,
  year = 2013,
  howpublished = {Homotopy Type Theory blog},
  url = {https://homotopytypetheory.org/2013/10/28/the-truncation-map-_-\%e2\%84\%95-\%e2\%80\%96\%e2\%84\%95\%e2\%80\%96-is-nearly-invertible/}
}
@article{shulman:real:cohesive,
   author = {{Shulman}, Michael},
    title = {Brouwer's fixed-point theorem in real-cohesive homotopy type theory},
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1509.07584},
 primaryClass = "math.CT",
     year = 2015,
    month = sep
}
@inproceedings{hofmann:syntax:semantics,
    author = {Martin Hofmann},
    title = {Syntax and Semantics of Dependent Types},
    booktitle = {Semantics and Logics of Computation},
    year = 1997,
    pages = {79--130},
    publisher = {Cambridge University Press}
}
@article{awodey:warren:models,
  title={Homotopy theoretic models of identity types},
  DOI={10.1017/S0305004108001783},
  eprint = {0709.0248},
  volume=146,
  number=1,
  journal={Mathematical Proceedings of the Cambridge Philosophical Society},
  publisher={Cambridge University Press},
  author={Awodey, Steve and Warren, Michael A.},
  year=2009,
  pages={45–55}
}
@unpublished{CCHM:cubical:type:theory,
author = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M\"ortberg},
title = {Cubical Type Theory: a constructive interpretation of the univalence axiom},
eprint = {1611.02108},
year = 2017,
note = {Linked via the cubicaltt github repository},
url = {http://www.cse.chalmers.se/~coquand/cubicaltt.pdf}
}
@article{riehl:shulman:categories,
   author = {{Riehl}, Emily and {Shulman}, Michael},
    title = "{A type theory for synthetic ∞-categories}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1705.07442},
 primaryClass = "math.CT",
 keywords = {Mathematics - Category Theory, Mathematics - Logic},
     year = 2017,
    month = may,
}
@article{bauer:five:stages,
  abstract = {On the odd day, a mathematician might wonder what constructive mathematics is all about. They may have heard arguments in favor of constructivism but are not at all convinced by them, and in any case they may care little about philosophy. A typical introductory text about constructivism spends a great deal of time explaining the principles and contains only trivial mathematics, while advanced constructive texts are impenetrable, like all unfamiliar mathematics. How then can a mathematician find out what constructive mathematics feels like? What new and relevant ideas does constructive mathematics have to offer, if any? I shall attempt to answer these questions.},
  added-at = {2016-12-09T19:26:42.000+0100},
  author = {Bauer, Andrej},
  biburl = {https://www.bibsonomy.org/bibtex/2518334c85bc9a66f717c3a90f89fe6d8/salotz},
  description = {Bulletin of the American Mathematical Society},
  doi = {10.1090/bull/1556},
  interhash = {bc0108a4e2fca7a3b036c8e77324a292},
  intrahash = {518334c85bc9a66f717c3a90f89fe6d8},
  journal = {Bulletin of the American Mathematical Society},
  keywords = {constructive-mathematics constructivism mathematics},
  timestamp = {2016-12-09T19:26:42.000+0100},
  title = {Five stages of accepting constructive mathematics},
  year = 2016
}
@inproceedings{bauer:hott:library,
 author = {Bauer, Andrej and Gross, Jason and Lumsdaine, Peter LeFanu and Shulman, Michael and Sozeau, Matthieu and Spitters, Bas},
 title = {The {HoTT} Library: A Formalization of Homotopy Type Theory in {Coq}},
 eprint = {1610.04591},
 booktitle = {Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
 series = {CPP 2017},
 year = {2017},
 isbn = {978-1-4503-4705-1},
 location = {Paris, France},
 pages = {164--172},
 numpages = {9},
 doi = {10.1145/3018610.3018615},
 acmid = {3018615},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Coq, Higher inductive types, Homotopy type theory, Univalent foundations, Universe polymorphism},
}

@ARTICLE{lumsdaine:shulman:hits,
   author = {{LeFanu Lumsdaine}, Peter and {Shulman}, Michael},
    title = "Semantics of higher inductive types",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1705.07088},
 primaryClass = "math.LO",
 keywords = {Mathematics - Logic, Mathematics - Category Theory, 18C50 (primary), 03B15, 18G55},
     year = 2017,
    month = may,
   adsurl = {http://adsabs.harvard.edu/abs/2017arXiv170507088L},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}
@INCOLLECTION{forsberg:setzer:indind,
    author    = {Nordvall Forsberg, Fredrik and Setzer, Anton},
    title     = {A finite axiomatisation of inductive-inductive definitions},
    booktitle = {Logic, Construction, Computation},
    publisher = {Ontos Verlag},
    year      = {2012},
    editor    = {Berger, Ulrich and Diener Hannes and  Schuster, Peter and Seisenberger, Monika},
    volume    = {3},
    series    = {Ontos mathematical logic},
    pages     = {259--287}
}

@ARTICLE{escardo:self-contained,
   author = {{H{\"o}tzel Escard{\'o}}, Mart{\'i}n},
    title = {A self-contained, brief and complete formulation of {Voevodsky's} {Univalence Axiom}},
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1803.02294},
 primaryClass = "math.LO",
 keywords = {Mathematics - Logic, 03B15},
     year = 2018,
    month = mar,
   adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180302294H},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}