ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passaudited 2026-08-17

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.

The self-adjunction of the contravariant power-set functor induces the double-power-set monad

Example

The contravariant power-set functor is self-adjoint between $S e t$ and ${S e t}^{o p}$ . The induced monad on $S e t$ is the covariant double-power-set functor $X \mapsto P P X$ .

Facts & Assumptions

Given: The contravariant power-set operation, acting on functions by inverse image.

[L1]

A natural hom-set bijection determines an adjunction (The unit-counit, hom-set, unit-universal, and counit-universal encodings of an adjunction are equivalent).

[L2]

Every adjunction induces a monad on the domain of its left adjoint (Every adjunction induces a monad on the domain of its left adjoint).

[L3]

$P (X)$ is the set of all subsets of $X$ (The power set $P (x) = {z : z \subseteq x}$ ).

Verification

technique · direct

1.1L1L3

A function $X \to P (Y)$ is the characteristic assignment of a relation $R \subseteq X \times Y$ ; transposing $R$ gives a function $Y \to P (X)$ . This natural bijection $S e t (X, P Y) ≅ S e t (Y, P X)$ supplies the self-adjunction by [L1].

2.1L2L3step 1.1

Applying [L2], the induced endofunctor is $T (X) = P P X$ , and its unit is $η_{X} (x) = {A \subseteq X : x \in A}$ .

3.1L2L3step 2.1∎

For $W \in P (P (P (P X)))$ , the multiplication is $μ_{X} (W) = {A \subseteq X : {A \subseteq P X : A \in A} \in W}$ . This has type $T^{2} X \to T X$ . In particular, the construction does not assert a natural map $P P X \to X$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

E. Riehl, Category Theory in Context, 2nd ed., Example 5.1.4(vii) (standard reference, not scraped)