UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

View the Project on GitHub UniMath/UniMath

On this page, we collect articles that have accompanying proofs in UniMath, or built upon UniMath. But also articles that describe UniMath.

We try to indicate the category to which a listed article belongs. There are

A paper can belong to more than one category, e.g. if it is mainly in cat. L but has a detailed introduction to UniMath, it could be listed as LG.

  1. [L] Ahrens, B., Frumin, D., Maggesi, M., van der Weide, N., 2019. Bicategories in Univalent Foundations 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), https://doi.org/10.4230/LIPIcs.FSCD.2019.5, preprint
  2. Ahrens, Benedikt ; Hirschowitz, André ; Lafont, Ambroise ; Maggesi, Marco, 2018. High-Level Signatures and Initial Semantics. 27th EACSL Annual Conference on Computer Science Logic (CSL 2018), https://doi.org/10.4230/LIPIcs.CSL.2018.4
  3. Ahrens, Benedikt ; Hirschowitz, André ; Lafont, Ambroise ; Maggesi, Marco, 2019. Modular Specification of Monads Through Higher-Order Presentations, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), https://doi.org/10.4230/LIPIcs.FSCD.2019.6
  4. [L] Ahrens, B., Kapulkin, K., and Shulman, M. (2015). Univalent categories and the Rezk completion. Math. Struct. Comput. Sci. 25(5): 1010-1039 (2015) https://doi.org/10.1017/S0960129514000486, preprint
  5. [L] Ahrens, B. and Lumsdaine, P. L., 2019. Displayed Categories. Logical Methods in Computer Science, March 5, 2019, Volume 15, Issue 1 - https://doi.org/10.23638/LMCS-15(1:20)2019, preprint
  6. Ahrens, Benedikt and Lumsdaine, Peter LeFanu and Voevodsky, Vladimir (2018). Categorical structures for type theory in univalent foundations. Logical Methods in Computer Science, September 11, 2018, Volume 14, Issue 3 - https://doi.org/10.23638/LMCS-14(3:18)2018
  7. [L] Ahrens, Benedikt ; Matthes, Ralph, 2018. Heterogeneous Substitution Systems Revisited. Postproceedings of 21st International Conference on Types for Proofs and Programs (TYPES 2015). https://doi.org/10.4230/LIPIcs.TYPES.2015.2, preprint
  8. [L] Ahrens, B., Matthes, R. and Mörtberg, A., 2019. From signatures to monads in UniMath. Journal of Automated Reasoning, 63(2), pp.285-318. https://link.springer.com/article/10.1007/s10817-018-9474-4
  9. [L] Ahrens, B., Matthes, R. and Mörtberg, A., 2022. Implementing a category-theoretic framework for typed abstract syntax. Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2022), pp.307-323. https://doi.org/10.1145/3497775.3503678
  10. [L] Ahrens, B. and Mörtberg, A., 2016, July. Some Wellfounded Trees in UniMath. In International Congress on Mathematical Software (pp. 9-17). Springer, Cham. https://link.springer.com/chapter/10.1007/978-3-319-42432-3_2
  11. [L] Amato, G., Maggesi, M., Parton, M. and Brogi, C.P., 2020. Universal Algebra in UniMath. arXiv preprint arXiv:2007.04840. https://arxiv.org/pdf/2007.04840
  12. [L] Bezem, M., Buchholtz, U. and Grayson, D.R., 2019. Construction of the Circle in UniMath. arXiv preprint arXiv:1910.01856. https://arxiv.org/pdf/1910.01856
  13. de Boer, Menno. “A Proof and Formalization of the Initiality Conjecture of Dependent Type Theory”. Master thesis, http://urn.kb.se/resolve?urn=urn%3Anbn%3Ase%3Asu%3Adiva-181640
  14. Borthelle, P., Hirschowitz, T., and Lafont, A., 2020. A Cellular Howe Theorem. LICS 2020: 273-286, https://doi.org/10.1145/3373718.3394738
  15. [G] Daniel R. Grayson, 2018. An introduction to univalent foundations for mathematicians. Bulletin of the American Mathematical Society 55 (2018), pp.427-450. https://dx.doi.org/10.1090/bull/1616, preprint
  16. [L] Ralph Matthes, Kobe Wullaert, and Benedikt Ahrens. “Substitution for Non-Wellfounded Syntax with Binders Through Monoidal Categories”, 2024. Proceedings of FSCD 2024, https://doi.org/10.4230/LIPIcs.FSCD.2024.25. Version with full appendices: https://doi.org/10.48550/arXiv.2308.05485.
  17. [L] Pelayo, Á., Voevodsky, V., and Warren, M. A., 2015. A univalent formalization of the p-adic numbers. Math. Structures Comput. Sci., 25(5):1147-1171, https://dx.doi.org/10.1017/S0960129514000541, pdf, preprint
  18. [L] Rech, F., 2018. Constructing Inductive Families in UniMath. http://www.ps.uni-saarland.de/~rech/ril/slides.pdf
  19. [G] Voevodsky, V. (2015). An experimental library of formalized mathematics based on the univalent foundations. Math. Structures Comput. Sci., 25(5):1278-1294, 2015, https://dx.doi.org/10.1017/S0960129514000577, pdf, preprint
  20. van der Weide, Niels, and Herman Geuvers. “The construction of set-truncated higher inductive types.” Electronic Notes in Theoretical Computer Science 347 (2019): 261-280.
  21. van der Weide, Niels, and Niccolò Veltri. “Constructing Higher Inductive Types as Groupoid Quotients.” Logical Methods in Computer Science 17 (2021).
  22. Ahrens, Benedikt, North, Paige Randall, van der Weide, Niels, “Semantics for two-dimensional type theory”. LICS (2022).
  23. van der Weide, Niels, “The Formal Theory of Monads, Univalently”. FSCD (2023).
  24. [L] Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. “Univalent Monoidal Categories”. In post-proceedings of TYPES 2022, LIPIcs vol. 269, 2023. https://dx.doi.org/10.4230/LIPIcs.TYPES.2022.15.
  25. [L] Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert. “Displayed Monoidal Categories for the Semantics of Linear Logic”. In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024 (2024): 260-273. https://doi.org/10.1145/3636501.3636956
  26. [L] van der Weide, Niels, “Univalent Enriched Categories and the Enriched Rezk Completion”, FSCD 2024.
  27. [L] Hilhorst, Dennis , and Paige North, “Formalizing the algebraic small object argument in UniMath”, ITP 2024.