---
references:
- id: Bauer2016Five
  accessed:
    - year: 2016
      month: 10
      day: 11
  author:
    - family: Bauer
      given: Andrej
  citation-key: Bauer2016Five
  container-title: Bulletin of the American Mathematical Society
  container-title-short: Bull. Amer. Math. Soc.
  DOI: 10.1090/bull/1556
  ISSN: 0273-0979, 1088-9485
  issued:
    - year: 2016
  title: Five stages of accepting constructive mathematics
  type: article-journal
  URL: http://www.ams.org/bull/0000-000-00/S0273-0979-2016-01556-4/

- id: Mazur2007When
  accessed:
    - year: 2015
      month: 6
      day: 7
  author:
    - family: Mazur
      given: Barry
  call-number: QA8.4 .P755 2008
  citation-key: Mazur2007When
  collection-title: Spectrum series
  container-title: 'Proof and Other Dilemmas: Mathematics and Philosophy'
  editor:
    - family: Gold
      given: Bonnie
    - family: Simons
      given: Roger A
  event-place: Washington, D.C.
  ISBN: 0-88385-567-4 978-0-88385-567-6
  issued:
    - year: 2007
  page: '221'
  publisher: Mathematical Association of America
  publisher-place: Washington, D.C.
  title: When is one thing equal to some other thing?
  type: chapter
  URL: http://abel.math.harvard.edu/~mazur/preprints/when_is_one.pdf

- id: McAllester2014Implementation
  accessed:
    - year: 2014
      month: 8
      day: 17
  author:
    - family: McAllester
      given: David
  citation-key: McAllester2014Implementation
  container-title: arXiv:1407.7274 [cs]
  issued:
    - year: 2014
      month: 7
      day: 27
  title: Implementation and Abstraction in Mathematics
  type: article-journal
  URL: http://arxiv.org/abs/1407.7274

- id: McAllester2014Morphoid
  accessed:
    - year: 2016
      month: 1
      day: 4
  author:
    - family: McAllester
      given: David
  citation-key: McAllester2014Morphoid
  container-title: arXiv:1407.7274 [cs]
  issued:
    - year: 2014
      month: 7
      day: 27
  title: Morphoid Type Theory
  type: article-journal
  URL: http://arxiv.org/abs/1407.7274

- id: Program2013Homotopy
  author:
    - family: Program
      given: The Univalent Foundations
  citation-key: Program2013Homotopy
  event-place: Institute for Advanced Study
  issued:
    - year: 2013
  publisher: http://homotopytypetheory.org/book
  publisher-place: Institute for Advanced Study
  title: 'Homotopy Type Theory: Univalent Foundations of Mathematics'
  type: book
...
