Scott's Representation Theorem and the Univalent Karoubi Envelope

TL;DR

This paper formalizes Scott's Representation Theorem within univalent foundations, implementing proofs by Scott and Hyland, and explores the role of the Karoubi envelope in categorical lambda calculus.

Contribution

It provides a formalization of Scott's Theorem in univalent foundations and compares two proofs, highlighting the role of the Karoubi envelope and automation techniques.

Findings

Successful formalization of Scott's Representation Theorem in UniMath

Implementation of two distinct proofs by Scott and Hyland

Development of automation for lambda-term reduction

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 $\lambda$-terms.