TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Set is locally cartesian closed

Statement

The category $S e t$ is locally cartesian closed.

Facts & Assumptions

Given: A function $f : X \to Y$ and an object $p : E \to X$ of the slice category $S e t / X$ .

[L1]

A category is locally cartesian closed exactly when each pullback functor $f^{*}$ has a right adjoint (Local cartesian closure is equivalent to every pullback functor having a right adjoint).

[L2]

In $S e t$ , functions are the morphisms and products are cartesian products (Sets and functions form the large locally small category $S e t$ ).

[L3]

In $S e t$ , currying gives the adjunction between product and function-set formation (Currying gives the adjunction $- \times A ⊣ (-)^{A}$ in $S e t$ ).

Proof

technique · direct

1.1

For $p : E \to X$ , define a set over $Y$ by $(Π_{f} E)_{y} : = \prod_{x \in f^{- 1} (y)} E_{x}$ , where $E_{x} = p^{- 1} (x)$ . An element of $(Π_{f} E)_{y}$ is therefore a choice of one element of $E_{x}$ for each $x$ over $y$ ; when $f^{- 1} (y) = \emptyset$ , this product is the singleton empty family. The projection $Π_{f} E \to Y$ sends such a family to $y$ .

givenL2construct

2.1

If $q : B \to Y$ is another object over $Y$ , then a morphism $q \to Π_{f} E$ over $Y$ assigns to each $b \in B$ over $y = q (b)$ a family of elements in the fibers $E_{x}$ for $x \in f^{- 1} (y)$ . Equivalently, it assigns to each pair $(b, x)$ with $q (b) = f (x)$ an element of $E_{x}$ , which is exactly a morphism $f^{*} q \to p$ over $X$ . This correspondence is natural and is the fiberwise form of [L3].

step 1.1L2L3algebra

3.1

Step 2.1 constructs a right adjoint $Π_{f}$ to every pullback functor in $S e t$ . Hence [L1] implies that $S e t$ is locally cartesian closed.

step 2.1L1∎

Depends on

Used by

A slice of Set computed as a locally cartesian closed category Example

Dependency tree · two levels

16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, 2nd ed., Section 4.6 (standard reference, not scraped)