Scott's Representation Theorem and the Univalent Karoubi Envelope
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.
Keywords
Cite
@article{arxiv.2506.22196,
title = {Scott's Representation Theorem and the Univalent Karoubi Envelope},
author = {Arnoud van der Leer and Kobe Wullaert and Benedikt Ahrens},
journal= {arXiv preprint arXiv:2506.22196},
year = {2025}
}
Comments
20 pages, LaTeX; submitted to the 16th International Conference on Interactive Theorem Proving (ITP 2025)