ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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 Kleisli category of the maybe monad is the category of sets and partial functions

Example

Let $T (Y) = Y ⊔ {⊥}$ . With insertion as unit and multiplication that collapses either occurrence of $⊥$ , this is the maybe monad. Its Kleisli arrows are precisely partial functions.

Facts & Assumptions

Given: The assignment $T (Y) = Y ⊔ {⊥}$ on sets.

[L1]

A monad has natural unit and multiplication satisfying two unit laws and associativity (Monad on a category).

[L2]

A Kleisli arrow $X \to Y$ is an ordinary arrow $X \to T (Y)$ , and its composition uses the monad multiplication (Kleisli category of a monad).

Verification

technique · direct

1.1

Define $T (f)$ to act by $f$ on $Y$ and fix $⊥$ , let $η_{Y}$ be the inclusion of $Y$ , and let $μ_{Y} : T (T Y) \to T Y$ fix elements of $Y$ and send both the inner and outer undefined values to $⊥$ . Direct inspection of the defined and undefined cases proves the unit and associativity laws in [L1].

2.1

A function $u : X \to Y ⊔ {⊥}$ determines the partial function with domain $D_{u} = {x : u (x) \in Y}$ and value $u (x)$ there. Conversely, a partial function on $D \subseteq X$ extends uniquely by assigning $⊥$ outside $D$ .

L2step 1.1

3.1

These constructions are inverse. Expanding Kleisli composition shows that $v ⋆ u$ is defined exactly where $u$ is defined and $v$ is defined at $u (x)$ , with value $v (u (x))$ ; this is the usual maximal-domain composition of partial functions.

L2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 8 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

E. Riehl, Category Theory in Context, 2nd ed., Examples 5.1.4(i) and 5.2.11(i) (standard reference, not scraped)