diff --git a/.cspell.json b/.cspell.json
index 158edf39..b4091af6 100644
--- a/.cspell.json
+++ b/.cspell.json
@@ -45,6 +45,7 @@
"Čech",
"characterisation",
"clopen",
+ "closedness",
"Clowder",
"coaccessible",
"cocartesian",
diff --git a/content/LRS-not-cartesian-closed.md b/content/LRS-not-cartesian-closed.md
new file mode 100644
index 00000000..96af5c59
--- /dev/null
+++ b/content/LRS-not-cartesian-closed.md
@@ -0,0 +1,49 @@
+---
+title: The category of locally ringed spaces is not cartesian closed
+description: A proof that the category of locally ringed spaces over a non-trivial ring R is not cartesian closed
+author: Daniel Schepler
+---
+
+## The category of locally ringed spaces is not cartesian closed
+
+For most of this development, we will be dealing with the case of $\LRS_k$ where $k$ is a field. We begin by describing $\Top$ as a reflective subcategory of $\LRS_k$.
+
+::: Lemma 1
+The forgetful functor $U : \LRS_k \to \Top$ has a right adjoint $K : \Top \to \LRS_k$ of equipping a topological space $X$ with the constant sheaf $\underline{k}$. Furthermore, the functor $K$ is fully faithful, thus making $\Top$ into a reflective subcategory of $\LRS_k$.
+:::
+
+_Proof._ In this adjunction, the counit $UK \to \id$ is just the identity. To describe the unit $\id \to KU$, we need to define a morphism $(X, \O_X) \to (X, \underline{k})$ for any locally ringed space $(X, \O_X)$ over $k$. This morphism will be the identity on topological spaces, and the pullback operation $\underline{k} \to \O_X$ will be the unique morphism of sheaves induced by the given structure of $\O_X$ as a sheaf of $k$-algebras. It is now straightforward to check this indeed defines an adjunction; and since the counit is an isomorphism, that implies that $K$ is fully faithful. $\square$
+
+We now show that this reflective subcategory is in fact also a coreflective subcategory. Recall that for $f \in \O_X(U)$ we have its vanishing set $V(f) \coloneqq \{x \in U : f(x) = 0\}$, where $f(x) \in \kappa(x)$ is the image of $f_x \in \O_{X,x}$ in the residue field.
+
+::: Lemma 2
+For each object $X$ of $\LRS_k$, let $X_0$ be the set of points $x \in X$ such that the induced morphism from $k$ to the residue field $\kappa(x)$ is an isomorphism. We give $X_0$ the following strengthening of the subspace topology: it will be the topology where a neighborhood subbasis at $x \in X_0$ is the collection of sets of the form $X_0 \cap V(f)$ where $f \in \O_X(U)$ for some neighborhood $U$ of $x$ in $X$, and $x \in V(f)$. Then $X \mapsto X_0$ defines a functor $S : \LRS_k \to \Top$ that is right adjoint to $K$.
+:::
+
+_Proof._ First, to see that $S$ is a functor, suppose we have a morphism $f : (X, \O_X) \to (Y, \O_Y)$. Then for $x \in X_0$, we have a sequence $k \to \kappa(f(x)) \to \kappa(x)$ where the composition is an isomorphism. Thus, $\kappa(f(x)) \to \kappa(x)$ is a surjective morphism of fields, and therefore an isomorphism. It follows that $k \to \kappa(f(x))$ is also an isomorphism of fields, so $f(x) \in Y_0$. To see that the restriction map $X_0 \to Y_0$ is continuous, suppose $g \in \O_Y(V)$ is such that $f(x) \in V(g)$. Then $x \in V(f^\sharp g)$, and
+$$X_0 \cap f^{-1}(Y_0 \cap V(g)) = X_0 \cap V(f^\sharp g)$$
+where $f^\sharp g \in \O_X(f^{-1}(V))$. In other words, we have shown that the inverse image in $X_0$ of any subbasic neighborhood of $f(x)$ is a neighborhood of $x$.
+
+Now if we apply the functor $S$ to a space of the form $(X, \underline{k})$, then since by definition any section of the constant sheaf $\underline{k}$ is locally constant, we see that we recover exactly $X$ with its original topology. Thus, we can define the unit $\id \to SK$ of the adjunction to be the identity.
+
+As for the counit $KS \to \id$, for any locally ringed space $(X, \O_X)$ over $k$ we need to define a morphism $(X_0, \underline{k}) \to (X, \O_X)$. The map of topological spaces will be the inclusion map $i : X_0 \hookrightarrow X$, which is continuous since in particular for $U$ an open neighborhood of $x \in X_0$ we have $X_0 \cap U = X_0 \cap V(0_U)$, where $0_U \in \O_X(U)$ is the zero element. The pullback map $\O_X \to i_* \underline{k}$ takes $f \in \O_X(U)$ to the function $X_0 \cap U \to k$ where $x \in X_0 \cap U$ maps to the inverse image of $f(x) \in \kappa(x)$ under the isomorphism $k \to \kappa(x)$. An alternative description of this pullback is that $x \in X_0 \cap U$ maps to the unique $a\in k$ such that $x \in V(f-a)$. Since $X_0 \cap V(f-a)$ is a neighborhood of $x$ in $X_0$ by definition, this shows that we get a locally constant function to $k$ as required.
+
+From here, it is straightforward to show that this does in fact define an adjunction. $\square$
+
+_Remark._ In the special case where $k$ is a finite field, we have
+$$\textstyle X_0 \cap V(f) = \bigcap_{a \in k^\times} (X_0 \cap D(f-a)),$$
+which is already open in the subspace topology. Therefore, in this case, $X_0$ is given exactly the subspace topology.
+
+::: Corollary 3
+If $k$ is a field, then $\LRS_k$ is not cartesian closed.
+:::
+
+_Proof._ We know that $\Top$ is not cartesian closed. By Lemma 2, $\Top$ is a coreflective subcategory of $\LRS_k$. Moreover, the inclusion preserves binary products (in fact, all limits) by Lemma 1. Therefore, the claim follows from Lemma 1 [here](/content/cartesian-closed-results). $\square$
+
+Finally, we generalize this result to arbitrary base rings.
+
+::: Corollary 4
+For any non-trivial commutative ring $R$, the category $\LRS_R$ is not cartesian closed.
+:::
+
+_Proof._ Let $k$ be a residue field of $R$. Then $\LRS_k$ is equivalent to the slice category $\LRS_R / \Spec k$ where $\Spec k$ is subterminal. Therefore, the claim follows from Corollary 3 above and Corollary 2 [here](/content/cartesian-closed-results). $\square$
diff --git a/content/cartesian-closed-results.md b/content/cartesian-closed-results.md
new file mode 100644
index 00000000..0c9f8593
--- /dev/null
+++ b/content/cartesian-closed-results.md
@@ -0,0 +1,27 @@
+---
+title: Results about cartesian closed categories
+description: We prove in particular when a coreflective subcategory of a cartesian closed category is again cartesian closed.
+author: Daniel Schepler
+---
+
+## Results about cartesian closed categories
+
+::: Lemma 1
+Suppose $\D$ is a coreflective subcategory of $\C$ such that $\D$ has binary products and the inclusion functor preserves these binary products. If $\C$ is cartesian closed, then so is $\D$.
+:::
+
+_Proof._ Let $U : \D \to \C$ be the inclusion functor with right adjoint $R : \C \to \D$. Then for any objects $X, Y, Z$ of $\D$ we have natural isomorphisms
+
+$$
+\begin{align*}
+\Hom_\D(Z\times X, Y) & \cong \Hom_\C(UZ \times UX, UY) \\
+& \cong \Hom_\C(UZ, [UX,UY]) \\
+& \cong \Hom_\D\bigl(Z, R([UX,UY])\bigr).
+\end{align*}
+$$
+
+::: Corollary 2
+If $\C$ is a cartesian closed category and $P$ is a [subterminal object](https://ncatlab.org/nlab/show/subterminal+object) of $\C$, then the slice category $\C / P$ is also cartesian closed.
+:::
+
+_Proof._ The forgetful functor $\C / P \to \C$ is fully faithful; it has right adjoint ${-} \times P$; and it preserves binary products (in fact all inhabited limits). Hence, Lemma 1 applies. $\square$
diff --git a/databases/catdat/data/categories/LRS_R.yaml b/databases/catdat/data/categories/LRS_R.yaml
index 112b01fe..f5417843 100644
--- a/databases/catdat/data/categories/LRS_R.yaml
+++ b/databases/catdat/data/categories/LRS_R.yaml
@@ -53,6 +53,22 @@ unsatisfied_properties:
Alternatively, using the usual adjunction between affine schemes and locally ringed spaces (EGA I (1971), Ch. 1, Prop. 1.6.3), a generating set in $\LRS_R$ would induce a generating set in the category of affine $R$-schemes, which contradicts the fact that $\CAlg(R)$ does not have a cogenerating set.
+ - property: cartesian closed
+ proof: This is proved here.
+ check_redundancy: false
+
+ - property: cartesian filtered colimits
+ proof: As a corollary of the results here, if we choose a quotient field $k$ of $R$, then the functor $\Top \to \LRS_R$ of equipping a topological space with the constant sheaf of $k$ is fully faithful, and preserves all colimits and all inhabited limits. Therefore, if $\LRS_R$ had cartesian filtered colimits, then $\Top$ would also, giving a contradiction.
+
+ - property: regular
+ proof: 'As a corollary of the results here, if we choose a quotient field $k$ of $R$, then the functor $\Top \to \LRS_R$ of equipping a topological space with the constant sheaf of $k$ is fully faithful, and preserves all colimits and all inhabited limits. Therefore, if $\LRS_R$ were regular, then for every regular epimorphism $X \to Y$ and morphism $Z \to Y$, the pullback $f : Z \times_Y X \to X$ would satisfy that the canonical morphism from the quotient of the kernel pair of $f$ to $X$ is an isomorphism. This would be inherited by the subcategory $\Top$, and since $\Top$ is finitely complete and has coequalizers, that would imply $\Top$ is also regular, giving a contradiction.'
+
+ - property: cofiltered-limit-stable epimorphisms
+ proof: 'As a corollary of the results here, if we choose a quotient field $k$ of $R$, then the functor $\Top \to \LRS_R$ of equipping a topological space with the constant sheaf of $k$ is fully faithful, and preserves all colimits and all inhabited limits. From here, the proof is similar to the one from $\Top$: we apply the contrapositive of the dual of this lemma to the functor $\Set \to \LRS_k$ which equips a set with the indiscrete topology and the constant sheaf of $k$.'
+
+ - property: effective cocongruences
+ proof: As a corollary of the results here, if we choose a quotient field $k$ of $R$, then the functor $\Top \to \LRS_R$ of equipping a topological space with the constant sheaf of $k$ is fully faithful, and preserves all colimits and all inhabited limits. Therefore, if $\LRS_R$ had effective cocongruences, then for every cocongruence $E$ on $X$, the canonical morphism from the cokernel pair of the equalizer of $E$ to $E$ would be an isomorphism. This would be inherited by the subcategory $\Top$, giving a contradiction.
+
special_objects:
initial object:
description: empty space
diff --git a/databases/catdat/data/category-implications/cartesian closed.yaml b/databases/catdat/data/category-implications/cartesian closed.yaml
index a952b113..88d76953 100644
--- a/databases/catdat/data/category-implications/cartesian closed.yaml
+++ b/databases/catdat/data/category-implications/cartesian closed.yaml
@@ -107,3 +107,12 @@
- locally cartesian closed
proof: Each slice is thin, semi-strongly connected, and has a terminal object. Thus, it corresponds to a linear order with a largest element $1$. Every such category is cartesian closed, where the exponential $a \Rightarrow b$ (Heyting implication) is $1$ when $a \leq b$ and otherwise $b$.
is_equivalence: false
+
+- id: cartesian_closed_thin_implies_lcc
+ assumptions:
+ - cartesian closed
+ - thin
+ conclusions:
+ - locally cartesian closed
+ proof: In a thin category, every object is subterminal. Thus, the result follows from Corollary 2 here.
+ is_equivalence: false