refs.bib

@misc{nlab,
    title = {Open problems in homotopy type theory},
    howpublished = {\url{https://ncatlab.org/nlab/show/open+problems+in+homotopy+type+theory}},
    note = {nLab},
    year = {2024}
}

@misc{mynameMentioned,
    author = {Nawrocki, Wojciech and others},
    title = {Certifying Synthetic Mathematics in {Lean}},
    year = {2026},
    url = {https://voidma.in/assets/slides/2026nawrocki_certifying_synthetic_mathematics_lean.pdf},
    note = {Slides}
}

@misc{HoTTESTSS,
    author = {Rijke, Egbert and others},
    title = {{HoTT}est Summer School},
    year = {2022},
    url = {https://github.com/martinescardo/HoTTEST-Summer-School}
}

@book{LADM,
    author = {David Gries and Fred B. Schneider},
    title = {A Logical Approach to Discrete Math},
    publisher = {Springer},
    year = {1993}
}

@book{NotesOST,
  title        = {Notes on Set Theory},
  author       = {Moschovakis, Yiannis},
  year         = {2006},
  edition      = {2nd},
  series       = {Undergraduate Texts in Mathematics},
  publisher    = {Springer},
  address      = {New York, NY},
  isbn         = {9780387316093},
}

@misc{Agda,
    title = {Agda Language Documentation},
    year = {2024},
    url = {https://agda.readthedocs.io/}
}

@misc{Belmont,
    author = {Belmont, Emily},
    title = {A Basic Introduction to Homotopy Type Theory},
    url = {https://mathweb.ucsd.edu/~ebelmont/hott.pdf}
}

@misc{Mathias,
    author = {Stout, Mathias and others},
    title = {Many-Sorted Model Theory},
    year = {2026},
    url = {https://github.com/Mathias-Stout/Many-sorted-model-theory}
}

@inproceedings{LicataSchulman,
    author = {Daniel R. Licata and Michael Shulman},
    title = {Calculating the Fundamental Group of the Circle in Homotopy Type Theory},
    booktitle = {Proceedings of the 28th Annual {ACM/IEEE} Symposium on Logic in Computer Science ({LICS})},
    year = {2013},
    url = {https://dlicata.wescreates.wesleyan.edu/pubs/ls13pi1s1/ls13pi1s1.pdf}
}

@mastersthesis{EgbertRijke,
    author = {Egbert Rijke},
    title = {Homotopy Type Theory},
    school = {Utrecht University},
    year = {2012}
}

@techreport{MaxBlans,
    author = {Max Blans},
    institution = {University of Amsterdam},
    title = {Homotopy Type Theory: Synthetic Homotopy Theory and Proof Verification},
    year = {2019}
}

@misc{HottBlDan,
    author = {{Homotopy Type Theory blog}},
    title = {Homotopy Theory in Type Theory: Progress Report},
    year = {2013},
    url = {https://homotopytypetheory.org/2013/05/20/homotopy-theory-in-type-theory-progress-report/}
}

@book{DocsLean,
    author = {{Lean Community}},
    publisher = {Microsoft Corporation and Lean FRO},
    title = {Functional Programming in {Lean}},
    year = {2023}
}

@manual{MathLean,
    author = {{Lean Community}},
    title = {Mathematics in {Lean}}
}

@book{Farmer,
    author = {William M. Farmer},
    title = {Simple Type Theory},
    publisher = {Birkh\"auser},
    year = {2025}
}

@book{Kam,
    author = {Holger Kammeyer},
    title = {Introduction to Algebraic Topology},
    publisher = {Birkh\"auser},
    year = {2023}
}

@book{Hatcher,
    author = {Allen Hatcher},
    title = {Algebraic Topology},
    publisher = {Cambridge University Press},
    year = {2002},
    url = {https://pi.math.cornell.edu/~hatcher/AT/ATpage.html}
}

@book{HottI,
    author = {Egbert Rijke},
    title = {Introduction to Homotopy Type Theory},
    publisher = {Cambridge University Press},
    year = {2022}
}

@book{HottON,
    author = {{The Univalent Foundations Program}},
    title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
    publisher = {The Univalent Foundations Program},
    year = {2013},
    url = {https://homotopytypetheory.org/book/}
}

@misc{hottorg,
    title = {Homotopy Type Theory},
    url = {https://homotopytypetheory.org/blog/}
}

@misc{vlad,
    author = {Voevodsky, Vladimir},
    title = {Univalent Foundations ({IAS})},
    url = {https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html}
}

@misc{myissue,
    title = {{HoTTLean} Magma Definition},
    url = {https://github.com/sinhp/HoTTLean/issues/165}
}

@misc{sinhp,
    title = {{HoTTLean} Issues},
    url = {https://github.com/sinhp/HoTTLean/issues}
}

@misc{myrepo,
    title = {{HoTTLean} Contributions},
    url = {https://github.com/PradCoder/HoTTLean/tree/master/test}
}

@misc{1lab,
    author = {{1lab contributors}},
    title = {1lab},
    url = {https://1lab.dev/}
}

@article{HoTTLean3,
    author = {Ulrik Buchholtz and Floris van Doorn and Egbert Rijke},
    title = {Homotopy Type Theory in {Lean}},
    journal = {Interactive Theorem Proving},
    year = {2017}
}

@misc{VoevodskyObituary,
    author = {{Institute for Advanced Study}},
    title = {Vladimir Voevodsky, 1966--2017},
    year = {2017},
    url = {https://www.ias.edu/news/2017/vladimir-voevodsky-obituary}
}

@misc{VoevodskyIAS2014,
    author = {Voevodsky, Vladimir},
    title = {Univalent Foundations: New Foundations of Mathematics},
    year = {2014},
    note = {Lecture at the Institute for Advanced Study},
    url = {https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2014_IAS.pdf}
}

@misc{TYPES2025abstract,
    author = {Nawrocki, Wojciech and others},
    title = {Certifying Synthetic Mathematics in {Lean}},
    year = {2025},
    note = {Abstract, TYPES 2025},
    url = {https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper25.pdf}
}

@misc{HomotopyNotes,
    title = {Homotopy Theory Primer for HoTT},
    author ={Brandon Shapiro},
    note = {Cornell University},
    url = {https://pi.math.cornell.edu/~bts82/events/hott/notes/HomotopyNotes.pdf}
}

@misc{CubicalAgda,
    title = {Cubical {Agda}},
    year = {2024},
    url = {https://agda.readthedocs.io/en/latest/language/cubical.html}
}

@misc{Wadler,
pages = {75-84},
publisher = {Association for Computing Machinery},
abstract = {Powerful insights arise from linking two fields of study previously thought separate. Examples include Descartes' coordinates, which links geometry to algebra, Planck's Quantum Theory, which links particles to waves, and Shannon's Information Theory, which links thermodynamics to communication. Such a synthesis is offered by the principle of Propositions as Types, which links logic to computation. At first sight it appears to be a simple coincidence -- almost a pun -- but it turns out to be remarkably robust, inspiring the design of automated proof assistants and programming languages, and continuing to influence the forefronts of computing. Propositions as Types is a notion with depth, breadth, and mystery. Proposition as Types informs our view of the universality of certain programming languages.},
author = {Wadler, Philip},
address = {New York},
copyright = {Copyright Association for Computing Machinery Dec 2015},
issn = {0001-0782},
journal = {Communications of the ACM},
keywords = {Computer science ;  Information theory ;  Quantum theory},
language = {eng},
number = {12},
volume = {58},
year = {2015},
title = {Propositions as types},
}