Scott’s Representation Theorem and the Univalent Karoubi Envelope

We sketch the correspondence between simply-typed lambda calculi (STLCs) and Cartesian closed categories. A STLC is a simply-typed language with at least abstraction and application. The type system of the language should be closed under function types $A\to B$. Lambek and Scott [25] describe the construction of denotational models for such calculi.

Now, a Cartesian closed category $𝐂$ gives rise to a STLC, its “internal language”: roughly, take the objects of the category to be types, and morphisms $f:A\to B$ of the category to be terms of type $B$ in context $A$. Conversely, any simply-typed lambda calculus gives rise to a Cartesian closed category, as follows. A type $A$ of the calculus gives an object $⟦A⟧$ in the category. A term $t:A$ of type $A$ in context $x_1:A_1,\mathrm{\dots },x_n:A_n$ gives a morphism $⟦t⟧:⟦A_1⟧\times \mathrm{\dots }\times ⟦A_n⟧\to ⟦A⟧$.

Internal logic and interpretation, together, provide a correspondence between simply-typed lambda calculi and Cartesian closed categories:

In 1969, Scott gave a famous series of lectures [33] where he initially claimed that untyped $\lambda$-calculi did not have (non-trivial) categorical models. Intuitively, for an object $D$ of some category to be a model of the untyped lambda calculus, one would need functions $D\leftrightarrows D^D$ modelling abstraction and application, such that the composition $D^D\to D\to D^D$ is the identity – to model $\beta$-equality. (For $\eta$-equality, the other composite must be the identity on $D$.) In particular, this would mean that the function space $D^D$ can be embedded into $D$ itself. In the category of sets, this is only possible for $D=1$. However, as Scott’s lectures progressed, he realized that his initial claim was incorrect. In the end, Scott constructed a model ${𝒟}_{\mathrm{\infty }}$ in the category of directed complete partial orders (dcpos). Later, models such as Scott’s graph model and Böhm’s tree model were constructed; see, e.g., [11, Part V].

To arrive at a result similar to the correspondence of Diagram (1), SRT abstracts away from particular calculi and models. We use Hyland’s [23] axiomatization of lambda calculi as $\lambda$-theories, which are particular algebraic theories from universal algebra. A $\lambda$-theory is an algebraic theory equipped with operations modelling abstraction and application, satisfying $\beta$- (and potentially $\eta$-) equality. On the semantic side, a model of a lambda calculus is defined to be a reflexive object $D$ in a Cartesian closed category; that is, a diagram $D\leftrightarrows D^D$ that exhibits $D^D$ as a retract of $D$ (see Definition 16).

For every reflexive object, one can construct its so-called endomorphism theory. Then SRT can be stated as follows: every untyped $\lambda$-calculus arises as the endomorphism theory of a reflexive object. To summarize, SRT provides the following diagram, where $\mathrm{𝖫𝖺𝗆𝖳𝗁}$ consists of $\lambda$-theories and $\mathrm{𝖱𝖮}$ of pairs of a Cartesian closed category and a reflexive object therein:

Unlike in the case of simply-typed lambda calculi, this diagram does not represent an equivalence, but only a section-retraction pair. That is, if we start with a lambda calculus, interpret it and then take the endomorphism theory of the interpretation, we end up with “the same” lambda calculus. However, starting with a reflexive object, taking its endomorphism theory and then the interpretation does not necessarily yield the original reflexive object; see also Remark 19.

Scott and Hyland gave different constructions of the interpretation of a lambda calculus and the proof that this forms a section. In this paper, we formalize both, and compare them, in the light of univalent foundations.

In this section, we give a brief introduction to univalent foundations and univalent category theory. Other short introductions can be found in [18, 9]. A comprehensive introduction is given in the HoTT book [37]; in particular, [37, Chap. 9] discusses univalent categories.

Univalent foundations (UF) are foundations of mathematics satisfying the univalence principle. This principle says, roughly, that two equivalent mathematical objects satisfy all the same properties. Technically, UF are an extension of Martin-Löf type theory (MLTT) [27] by the univalence axiom and, optionally, (certain) higher inductive types. We assume the reader is familiar with the basics of MLTT as discussed, for instance, in [37, Chap. 1]. To fix notation: we write $g\circ f$ for the composition of functions $f:X\to Y$ and $g:Y\to Z$.

Given a type $X$ and elements $x,y:X$, we denote by $x=y$ the identity type between $x$ and $y$. The type $x=y$ can contain multiple distinct elements, that is, different identity terms from $x$ to $y$. For any $x:X$, we have the identity term $\mathrm{𝗋𝖾𝖿𝗅}(x):x=x$. In particular, given two types $S$ and $T$ (elements of some universe type), we have the type $S=T$. There is also a seemingly weaker notion of sameness, called equivalence, written $S\simeq T$; its elements are functions $S\to T$ with a two-sided inverse (see [37, Chap. 4] for details). We have a function $\mathrm{idtoequiv}:(S=T)\to (S\simeq T)$, sending $\mathrm{𝗋𝖾𝖿𝗅}(S)$ to the identity equivalence on $S$. The univalence axiom says that this map is an equivalence, for any $S$ and $T$. In particular, every structure on types transports along an equivalence of types.

In univalent foundations, types are stratified according to how “complex” their identity types are: Let $T$ be a type. It is contractible if there is an equivalence $e:T\simeq 1$ to the unit type $1$. It is a proposition if any two of its elements are identical: ${\prod }_{s,t:T}s=t$. It is a set if all of its identity types $s=t$, for $s,t:T$, are propositions (identity proofs in $T$ are unique). It is a groupoid if all of its identity types $s=t$, for $s,t:T$, are sets. This stratification of types can be continued recursively, but the aforementioned definitions suffice for the purpose of this paper.

Given a type $A$, we form a new type $\Vert A\Vert$, the propositional truncation of $A$; $\Vert A\Vert$ is a proposition, and inhabited if and only if $A$ is inhabited. When postulating that something “merely exists in $T$ with property $P$” (such as in Definition 44), we formalize it as $\Vert {\sum }_{x:T}P(x)\Vert$.

There are two notions of category () in univalent foundations. Both kinds consist, in particular, of a type $O$ of objects and a dependent type $M:O\to O\to \mathrm{𝐓𝐲𝐩𝐞}$ of morphisms. Given a category $𝐂$, we write $𝐂(X,Y)$ or $X\to Y$ for the type of morphisms between objects $X$ and $Y$. A category also has suitably typed composition and identity operations, and proofs of the associativity and unitality of composition. To ensure that unitality and associativity are propositions, we require that all the $𝐂(X,Y)$ are sets. Just like with functions, we write $g\circ f$ for the composition of morphisms $f:𝐂(X,Y)$ and $g:𝐂(Y,Z)$. For details, we refer to [5, Def. 3.1] – there, categories are called precategories.

A (pre)category as described above does not correspond to a category in Voevodsky’s model of univalent foundations in simplicial sets [24]; it has data that is not usually present in a category, namely a potentially non-trivial identity type on the type $O$ of objects. There are two ways to “kill” that data. Firstly, we could assert that the type $O$ of objects should also form a set in the above sense; this leads to the notion of setcategory. Secondly, we could assert that the identities $a=b$ of $a,b:O$ correspond exactly to isomorphisms $a\cong b$ of the category; this leads to the notion of univalent category. More precisely, in a univalent category $𝐂$ we demand that for every $a,b:𝐂$, the map ${\mathrm{𝗂𝖽𝗍𝗈𝗂𝗌𝗈}}_{a,b}:(a=b)\to (a\cong b)$, mapping $\text{refl}(a)$ to the identity isomorphism on $a$, is an equivalence, in analogy to the univalence axiom. One can show that the type of objects of a univalent category forms a groupoid.

There are thus two theories of categories in univalent foundations. Setcategory theory behaves much like traditional category theory; however, many naturally occurring categories are not setcategories. On the other hand, there are many univalent categories. Importantly, the category $\mathrm{𝐒𝐞𝐭}$ of sets (of a fixed universe) in the sense described above, is univalent; its objects are pairs of a type $X$ (of a fixed universe) together with a proof that $X$ is a set, and morphisms are type-theoretic functions. Roughly, univalence of this category is a consequence of the univalence axiom (for that universe). Furthermore, for two categories $𝐂$ and $𝐃$, the functor category $[𝐂,𝐃]$ is univalent if $𝐃$ is univalent; hence, in particular, presheaf categories $P𝐀=[{𝐀}^{\mathrm{𝗈𝗉}},\mathrm{𝐒𝐞𝐭}]$ are univalent. Still, not every category is univalent, e.g., the category $\bullet \leftrightarrows \bullet$ with two distinct but isomorphic objects, or the set-Karoubi envelope of Section 3.1, see Example 42. However, every category has a univalent replacement, which we call its Rezk completion:

In summary, univalent foundations give us two flavors of category theory: category theory up to isomorphism (setcategories) and category theory up to adjoint equivalence (univalent categories). We demonstrate the difference between Scott’s and Hyland’s proof of SRT by showing that Scott’s construction happens in the realm of setcategories, whereas Hyland’s construction happens in the realm of univalent categories. Furthermore, Hyland’s construction yields the Rezk completion of Scott’s construction.

In Section 2 we present our formalization of SRT as shown in Equation 2. More precisely, we formalize two different constructions of the function labelled “interpretation”, one by Scott, and one by Hyland, and we prove that both are sections to the function associating to a reflexive object its endomorphism theory. In Section 3 we zoom in on the different interpretation functions. Both use a variant of the Karoubi envelope of a category. We provide a novel analysis and comparison of the two variants, through the lens of univalent foundations, and show how the two variants relate Scott’s and Hylands constructions. In Section 4 we describe a tactic for the manipulation of lambda terms. In Section 5 we discuss related work.

Most of the definitions and results presented in this paper are formalized and computer-checked in UniMath [42], a library of univalent mathematics based on Rocq. Our code has been integrated into the UniMath library, and comprises more than 11000 lines of code, split up more or less evenly between definitions and proofs. We can identify the following main components: the definitions of the basic categories with their object and morphism types (3000 lines); the proof of Scott’s version of SRT, which uses a lot of reasoning about $\lambda$-terms (3000 lines); the definition of the Karoubi envelope (2000 lines); the constructions of various algebraic theories, like the endomorphism theory, and the proof of the relation between the representation theorems (both 1000 lines).

Throughout the paper, definitions and results are decorated with links, for example, , to an HTML version of UniMath. That HTML version is derived from commit 5941f44 of UniMath. Proof-checking and creation of the HTML documentation can be reproduced locally by following the UniMath compilation instructions. Note that for technical reasons, the formalization does not always closely follow the material in this paper, with the main difference described in Remark 21. Another point of complication is the necessary switching between two different ways to encode n-tuples $x:X^n$, either as nested 2-tuples $((\mathrm{\dots }((x_1,x_2),x_3),\mathrm{\dots }),x_n)$ or as functions $x:\{1,\mathrm{\dots },n\}\to X$.

We give a definition of untyped $\lambda$-calculi (Definition 8), an extension of the concept of an algebraic theory from universal algebra (Definition 4). We also define reflexive objects in Cartesian closed categories, the intended denotational semantics for such calculi.

Algebraic theories are also known as (abstract) clones; they are similar to operads – see, e.g., [22, 36] for details.

Algebraic theories and their morphisms form a category $\mathrm{𝐀𝐥𝐠𝐓𝐡}$ (). Furthermore, an isomorphism $S\cong T$ of algebraic theories consists of pointwise bijections $f_n:S_n\cong T_n$ that respect the variables and substitution. By univalence, each $f_n$ corresponds to an identity $p_n:S_n=T_n$ also respecting the algebraic structure. Again by univalence, the $p_n$’s combine into an identity of algebraic theories $S=T$. Hence:

Let ${\iota }_{m,n}:T_m\to T_{m+n}$ be the “weakening” function $f\mapsto f\bullet (x_{m+n,1},\mathrm{\dots },x_{m+n,m})$. Note that ${\iota }_{m,n}(f)\bullet g=f\bullet {(g_i)}_{i\le m}$ and ${\iota }_{m,n}(f\bullet g)=f\bullet {({\iota }_{m,n}(g_i))}_i$.

We also formalized the notion of $\lambda$-theory without $\beta$-equality, and of $\lambda$-theory with both $\beta$- and $\eta$-equality (meaning ${\lambda }_n\circ {\rho }_n={\mathrm{𝗂𝖽}}_{L_n}$), but we only formalized the main results for the $\lambda$-theories of Definition 8.

$\lambda$-theories and their morphisms form a category $\mathrm{𝐋𝐚𝐦𝐓𝐡}$ () with $\mathrm{𝖫𝖺𝗆𝖳𝗁}$ as the underlying type of objects.

We can prove the following analogously to Proposition 6:

Proposition 13 expresses that identities $T=T^{\prime }$ of $\lambda$-theories are equivalent to isomorphisms $T\cong T^{\prime }$; this enables us to express SRT purely on the level of types, without needing to mention (iso)morphisms of $\lambda$-theories, as discussed in Remark 3.

Let $L$ be a $\lambda$-theory. Hyland shows that ${\rho }_n(f)$ corresponds to $f{x}_{n+1}$, which is $f$ applied to $x_{n+1}$ [23, Section 3.1]. Now consider the element $\rho (x_{1,1}):L_2$.

Now we are ready to talk about denotational semantics for the untyped $\lambda$-calculus, for which we will need the following definition.

The proofs that $E(X)$ is an algebraic theory follow mainly from properties of the product and naturality of ${\phi }_Y$. Note that $E(X)$ would satisfy $\eta$-equality if $\mathrm{app}$ were a section.

Because of cardinality reasons, Example 18 is the only reflexive object in the category of sets. Hence, for nontrivial models of the untyped $\lambda$-calculi, we have to look in categories different from $\mathrm{𝐒𝐞𝐭}$. Scott’s model $D_{\mathrm{\infty }}$ lives in the category of dcpos whose morphisms are (continuous) section-retraction pairs [31].

SRT states that we can represent every untyped $\lambda$-calculus as an endomorphism theory of some reflexive object:

In the following two subsections, we will discuss two proofs of this theorem: the original proof by Dana Scott (Theorem 24) and a more abstract proof by Martin Hyland (Theorem 36).

In this subsection, we will give Scott’s original proof [32] of SRT.

It is a fairly syntactical proof, making heavy use of the operations of the $\lambda$-calculus for the various constructions. We first define the category $𝐑$ (Definition 22) and show that it has products and exponential objects. Then we construct an object in this category and show that it is a reflexive object. Lastly, we construct the endomorphism theory and show that it is isomorphic to the $\lambda$-theory that we started with (Theorem 24).

Let $L$ be a $\lambda$-theory. First of all, for $a_1,a_2:L_0$, we define

Although, actually, since every one of these starts with a $\lambda$-abstraction, we need to lift the constants $a_i$ to ${\iota }_{0,1}(a_i):L_1$ to make the definitions above typecheck. Note that ${\pi }_i(a_1,a_2)=a_i$ and ${\pi }_i\circ ⟨a_1,a_2⟩=\lambda x_1,a_i{x}_1$.

We define ${(a_i)}_i=(a_1,\mathrm{\dots },a_n)=((\mathrm{\dots }(((\lambda x_1,x_1),a_1),a_2),\mathrm{\dots }),a_n)$ (analogous for ${⟨a_i⟩}_i$) and correspondingly ${\pi }_{n,i}={\pi }_2\circ \pi _1^{}{}_{}{}^{n-i}$.

Scott introduces the following category, referred to as the category of retracts:

$𝐑$ has a terminal object, given by $I=\lambda x_1{x}_2,x_2:𝐑$ (). It is terminal because for $f:A\to I$, we have $f=I\circ f=I$.

$𝐑$ also has binary products $A_1\times A_2=⟨p_1,p_2⟩$ for $p_i=A_i\circ {\pi }_i$ the projections, with product morphisms $⟨f,g⟩$ ().

For $B,C:𝐑$, we have an exponential object $C^B=\lambda x_1,C\circ x_1\circ B$, with a bijection $\psi :𝐑(A\times B,C)\stackrel{\sim }{\to }𝐑(A,C^B)$, given by $\psi (f)=\lambda x_1{x}_2,f(x_1,x_2)$ and ${\psi }^{-1}(f)=\lambda x_1,g({\pi }_1{x}_1)({\pi }_2{x}_1)$ ().

Now we can define our reflexive object:

This allows us to give Scott’s proof of the representation theorem:

While Scott proves the representation theorem in a very syntactical way, constructing the category $𝐑$ for his representation theorem using the $\lambda$-calculus operations, Hyland uses more machinery from category theory, and works with a different category: the category of ($T$-)presheaves ${\mathrm{𝐏𝐬𝐡𝐟}}_T$ of a $\lambda$-theory $T$.

In this section, we define the category of presheaves (Definition 26), and construct a reflexive object herein Corollary 32. Furthermore, we show that the endomorphism theory of the reflexive object is isomorphic to the $\lambda$-theory that we started with (Theorem 36).

A prime example of a $T$-presheaf is $T$ itself:

$T$-presheaves and their morphisms form the category of $T$-presheaves ${\mathrm{𝐏𝐬𝐡𝐟}}_T$ (). Because presheaf (iso)morphisms preserve $\bullet$, we have, analogous to Proposition 6:

In this section, we construct a category ${𝐑}^S(𝐂)$ from a category $𝐂$, and show that it is the setcategory Karoubi envelope if $𝐂$ is a setcategory. The construction is the same as the one formalized in the 1lab [26] (see also Section 5).

In this section, we construct a category ${𝐑}^U(𝐂)$ from a category $𝐂$, and show that it is the univalent Karoubi envelope of $𝐂$, regardless of whether $𝐂$ is univalent or not. We use the fully faithful Yoneda embedding $\text{H}:𝐂\hookrightarrow P𝐂$.