Scott's Representation Theorem and the Univalent Karoubi Envelope

Arnoud van der Leer


Date: Wed, September 17, 2025
Time: 12:00
Room: Building 28, room Turing
Note: This is a talk to be given at ITP 2025


This talk will present our ITP paper about Scott’s representation theorem: 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. In our paper, we present two formalizations of Scott’s Representation Theorem in the Rocq-UniMath library: one proof 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. Lastly, we report on some automation we have implemented for the reduction of lambda-terms.

Previous: |
Next: |