Document Open Access Logo

Scott’s Representation Theorem and the Univalent Karoubi Envelope

Authors Arnoud van der Leer , Kobe Wullaert , Benedikt Ahrens

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.33.pdf
  • Filesize: 1.28 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.33.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Logic and verification
Keywords
  • Lambda calculi
  • algebraic theories
  • categorical semantics
  • Karoubi envelope
  • formalization
  • Rocq-UniMath
  • univalent foundations

Metrics

Abstract

Lambek and Scott constructed a correspondence between simply-typed lambda calculi and Cartesian closed categories. Scott’s Representation Theorem is a cousin to this result for untyped lambda calculi. It states that every untyped lambda calculus arises from a reflexive object in some category.
We present a formalization of Scott’s Representation Theorem in univalent foundations, in the (Rocq-)UniMath library. Specifically, we implement two proofs of that theorem, one by Scott and one by Hyland. We also explain the role of the Karoubi envelope - a categorical construction - in the proofs and the impact the chosen foundation has on this construction. Finally, we report on some automation we have implemented for the reduction of λ-terms.

Cite As Get BibTex

Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens. Scott’s Representation Theorem and the Univalent Karoubi Envelope. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.33

Author Details

Arnoud van der Leer
  • Delft University of Technology, The Netherlands
Kobe Wullaert
  • Delft University of Technology, The Netherlands
Benedikt Ahrens
  • Delft University of Technology, The Netherlands

Acknowledgements

We thank Mohamed Barakat, Tom de Jong, and Niels van der Weide, as well as the anonymous referees for valuable feedback on versions of this paper. We gratefully acknowledge the work by the Rocq development team in providing the Rocq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Rocq.

Supplementary Materials

References

  1. Benedikt Ahrens. Modules over relative monads for syntax and semantics. Math. Struct. Comput. Sci., 26(1):3-37, 2016. URL: https://doi.org/10.1017/S0960129514000103.
  2. Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, and Niels van der Weide. Bicategories in univalent foundations. Math. Struct. Comput. Sci., 31(10):1232-1269, 2021. URL: https://doi.org/10.1017/S0960129522000032.
  3. Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. High-level signatures and initial semantics. In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 4:1-4:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.4.
  4. Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular specification of monads through higher-order presentations. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 6:1-6:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.6.
  5. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25(5):1010-1039, January 2015. URL: https://doi.org/10.1017/s0960129514000486.
  6. Benedikt Ahrens and Peter LeFanu Lumsdaine. Displayed categories. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:20)2019.
  7. Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical structures for type theory in univalent foundations. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:18)2018.
  8. Benedikt Ahrens, Ralph Matthes, Niels van der Weide, and Kobe Wullaert. Displayed monoidal categories for the semantics of linear logic. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 260-273. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636956.
  9. Benedikt Ahrens and Paige Randall North. Univalent foundations and the equivalence principle. In Stefania Centrone, Deborah Kant, and Deniz Sarikaya, editors, Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts, pages 137-150. Springer International Publishing, Cham, 2019. URL: https://doi.org/10.1007/978-3-030-15655-8_6.
  10. Thorsten Altenkirch, Ambrus Kaposi, Artjoms Šinkarovs, and Tamás Végh. Combinatory Logic and Lambda Calculus Are Equal, Algebraically. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), volume 260 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2023.24.
  11. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  12. Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. The HoTT library: a formalization of homotopy type theory in Coq. In Yves Bertot and Viktor Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 164-172. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018615.
  13. Nick Benton, Andrew Kennedy, and Carsten Varming. Some Domain Theory and Denotational Semantics in Coq. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, pages 115-130, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-03359-9_10.
  14. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Log. Methods Comput. Sci., 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:1)2012.
  15. Tom de Jong. The Scott model of PCF in univalent type theory. Math. Struct. Comput. Sci., 31(10):1270-1300, 2021. URL: https://doi.org/10.1017/S0960129521000153.
  16. Tom de Jong and Martín Hötzel Escardó. Domain theory in constructive and predicative univalent foundations. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 28:1-28:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CSL.2021.28.
  17. Robert Dockins. Formalized, effective domain theory in coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 209-225. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_14.
  18. Daniel R. Grayson. An introduction to univalent foundations for mathematicians. Bulletin of the American Mathematical Society, 55(4):427-450, 2018. URL: https://doi.org/10.1090/bull/1616.
  19. Jason Gross, Adam Chlipala, and David I. Spivak. Experience Implementing a Performant Category-Theory Library in Coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 275-291. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_18.
  20. André Hirschowitz and Marco Maggesi. Modules over monads and initial semantics. Information and Computation, 208(5):545-564, 2010. Special Issue: 14th Workshop on Logic, Language, Information and Computation (WoLLIC 2007). URL: https://doi.org/10.1016/j.ic.2009.07.003.
  21. Jason Z. S. Hu and Jacques Carette. Formalizing category theory in Agda. In Catalin Hritcu and Andrei Popescu, editors, CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021, pages 327-342. ACM, 2021. URL: https://doi.org/10.1145/3437992.3439922.
  22. J. Martin E. Hyland. Towards a notion of lambda monoid. In John Power and Cai Wingfield, editors, Proceedings of the Workshop on Algebra, Coalgebra and Topology, WACT 2013, Bath, UK, March 1, 2013, volume 303 of Electronic Notes in Theoretical Computer Science, pages 59-77. Elsevier, 2013. URL: https://doi.org/10.1016/J.ENTCS.2014.02.004.
  23. J. Martin E. Hyland. Classical lambda calculus in modern dress. Mathematical Structures in Computer Science, 27(5):762-781, 2017. URL: https://doi.org/10.1017/S0960129515000377.
  24. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23(6):2071-2126, 2021. URL: https://doi.org/10.4171/jems/1050.
  25. J. Lambek and P. J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1986. Google Scholar
  26. Amélia Liao, Jonathan Coates, Reed Mullanix, et al. 1lab. URL: https://1lab.dev/.
  27. Per Martin-Löf. An intuitionistic theory of types. Bibliopolis, 1984. Google Scholar
  28. Rasmus Ejlers Møgelberg. Interpreting polymorphic FPC into domain theoretic models of parametric polymorphism. In Michele Bugliesi, Bart Preneel, Vladimiro Sassone, and Ingo Wegener, editors, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, volume 4052 of Lecture Notes in Computer Science, pages 372-383. Springer, 2006. URL: https://doi.org/10.1007/11787006_32.
  29. Rasmus Ejlers Møgelberg and Marco Paviotti. Denotational semantics of recursive types in synthetic guarded domain theory. Math. Struct. Comput. Sci., 29(3):465-510, 2019. URL: https://doi.org/10.1017/S0960129518000087.
  30. Pierre-Marie Pédrot. Ltac2: Tactical warfare, 2019. Talk at CoqPL 2019. URL: https://popl19.sigplan.org/details/CoqPL-2019/8/Ltac2-Tactical-Warfare.
  31. Dana S. Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, pages 97-136, Berlin, Heidelberg, 1972. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0073967.
  32. Dana S. Scott. Relating theories of the λ-calculus. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic and Formalism, pages 403-450. 1980. Google Scholar
  33. Dana S. Scott. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science, 121(1):411-440, 1993. URL: https://doi.org/10.1016/0304-3975(93)90095-B.
  34. Michael Shulman. Idempotents in intensional type theory. Log. Methods Comput. Sci., 12(3), 2016. URL: https://doi.org/10.2168/LMCS-12(3:9)2016.
  35. The Coq Development Team. The Coq reference manual - release 8.19.0. https://coq.inria.fr/doc/V8.19.0/refman, 2024.
  36. S. N. Tronin. Abstract clones and operads. Siberian Mathematical Journal, 43:746-755, 2002. URL: https://doi.org/10.1023/A:1016340806503.
  37. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  38. Arnoud van der Leer. Universal algebra, univalent foundations and the untyped λ-calculus. Master’s thesis, Delft University of Technology, December 2024. URL: https://repository.tudelft.nl/record/uuid:e6582866-9c0d-4a13-8eda-42c25e0deba4.
  39. Niels van der Weide. The internal languages of univalent categories. CoRR, abs/2411.06636, 2024. URL: https://doi.org/10.48550/arXiv.2411.06636.
  40. Niels van der Weide, Nima Rasekh, Benedikt Ahrens, and Paige Randall North. Univalent double categories. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 246-259. ACM, 2024. URL: https://doi.org/10.1145/3636501.3636955.
  41. Niels van der Weide and Kobe Wullaert. Rezk completions for (elementary) topoi. https://msp.cis.strath.ac.uk/types2025/abstracts/TYPES2025_paper71.pdf, 2025. Abstract presented at TYPES 2025.
  42. Vladimir Voevodsky, Benedikt Ahrens, Daniel R. Grayson, et al. Unimath - a computer-checked library of univalent mathematics. available at http://unimath.org. URL: https://doi.org/10.5281/zenodo.13828995.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact