Category Theory

Motivation

Philosophers of physics use category theory to decide when a formulation of a theory carries excess structure. Weatherall (2016) represents each formulation of electromagnetism as a category of models and the passage from potentials to field strengths as the functor $A \mapsto F = dA$. A functor that is not full forgets structure, one that is not essentially surjective forgets properties, and one that is not faithful forgets stuff. Weatherall's §4 argues on Minkowski space that the potential formulation with gauge transformations as arrows is related to the field-strength formulation by a functor that is full and essentially surjective. His footnote 9 sets topology aside, and the erratum to his Proposition 2 (arXiv v2, p. 15) records that the gauge-theoretic functor is not faithful, because constant gauge transformations act trivially on fields.

On a contractible spacetime these facts all rest on one theorem: the Poincaré lemma, which says closed differential forms are exact. A companion mission (Weatherall 2016: Potentials vs. Field Strengths on a Finite 2-Complex) proves the discrete version, in which fullness, faithfulness and essential surjectivity are equivalent to the vanishing of $H^1$, $H^0$ and $H^2$ of a cell complex. This mission is the continuum version on a vector space, built on Mathlib's exterior derivative.

Timeline. The explicit radial homotopy operator proof of the Poincaré lemma is standard in textbooks; it is the proof of Theorem 4-11 in Spivak's Calculus on Manifolds (1965). Antiexact forms and the same operator are studied in Kycia (2020). Mathlib has the exterior derivative extDeriv with $d^2 = 0$. In 2025 Kudryashov proved the degree-1 case for convex sets, stated for 1-forms written as E → E →L F with a symmetric derivative. Mathlib has no Poincaré lemma in higher degree, no de Rham cohomology and no Hodge star.

Setting

Let $E$ be a real normed space, for example $\mathbb R^n$, and $F$ a real Banach space of field values. A differential $k$-form is a map $\omega : E \to E[\wedge^k]\to_L F$ that assigns to each point a continuous alternating $k$-linear map. Smooth means $C^\infty$ (ContDiff ℝ ∞). The exterior derivative is Mathlib's extDeriv:

$$d\omega(x)(v_0,\dots,v_k) = \sum_{i=0}^{k} (-1)^i\, D\omega(x)(v_i)(v_0,\dots,\widehat{v_i},\dots,v_k).$$

A function $\chi : E \to F$ is a 0-form, and $d\chi$ is its derivative viewed as a 1-form (grad). The radial homotopy operator sends a $(k+1)$-form $\omega$ to the $k$-form

$$(K\omega)(x)(v_1,\dots,v_k) = \int_0^1 t^k\, \omega(tx)(x, v_1,\dots,v_k)\, dt .$$

Field equations enter through an arbitrary predicate $P$ on 2-forms. For example $P(F) \iff {\star d \star F} = J$ once a metric is chosen, and $P \equiv \mathrm{True}$ in vacuum. The categories are:

• Fld P (Weatherall's EM1): smooth closed 2-forms $B$ with $P(B)$, with only identity arrows.
• Pot P (EM2 with gauge arrows, fn. 15): smooth 1-forms $A$ with $P(dA)$. An arrow $A \to A'$ is a smooth $\chi : E \to F$ with $A + d\chi = A'$, and arrows compose by adding gauge functions.
• fieldStrength P : Pot P ⥤ Fld P: the functor $A \mapsto dA$, which sends every gauge arrow to an identity.

The cohomology conditions are elementary Props:

• $H^0 = 0$: smooth $\chi$ with $d\chi = 0$ implies $\chi = 0$.
• $H^1 = 0$: every smooth closed 1-form is $d\chi$ for a smooth $\chi$.
• $H^2 = 0$ on the $P$-sector: every smooth closed 2-form $B$ with $P(B)$ is $dA$ for a smooth $A$.

Formalization targets

Goal: the continuum classification

For every $P$ that admits at least one potential:

$$\texttt{fieldStrength}\ P \text{ is full and essentially surjective},\qquad \text{faithful} \iff F \text{ is trivial},$$ $$H^1 = 0,\qquad H^2 = 0,\qquad H^0 = 0 \iff F \text{ is trivial}.$$

So the potential description with gauge arrows forgets only stuff, namely the constant gauge transformations, and nothing else on a vector space.

Milestones

1. The radial homotopy operator preserves smoothness.
2. The homotopy formula $d(K\omega) + K(d\omega) = \omega$ for smooth $\omega$ of degree $k+1 \ge 1$.
3. The Poincaré lemma: a smooth closed form of degree $\ge 1$ has a smooth primitive.
4. Degree 0: for differentiable $\chi$, $d\chi = 0$ holds iff $\chi$ is constant.
5. $H^1 = 0$ and $H^2 = 0$ in the potentials language.
6. Constants act freely and transitively on gauge arrows $A o A'$ by $\chi \mapsto \chi + c$, so $\mathrm{Hom}(A, A')$ is empty or an $F$-torsor.
7. The structural equivalences, which mirror the discrete mission: full $\iff H^1 = 0$, faithful $\iff H^0 = 0$, essentially surjective $\iff H^2 = 0$.

Four supporting statements isolate the reusable ingredients of Milestone 2:

• An alternating-sum identity for alternating maps.
• An interior-product identity for Mathlib's alternatizeUncurryFin.
• Differentiation of $K\omega$ under the integral sign.
• The radial fundamental theorem of calculus.

Significance

The result. The goal makes precise, on $\mathbb R^n$ and with any field equation, the claim behind Weatherall's §4: up to the constants $H^0 = F$, potentials modulo gauge carry no more information than field strengths. With the discrete mission, it shows that the three ways of forgetting information correspond to $H^1$, $H^0$ and $H^2$ in both settings. The continuum version is metric-free. Maxwell's equations, sources or any other field equation enter only through $P$, so the classification holds for all of them at once.

Formalizing it. The homotopy formula and the Poincaré lemma for Mathlib's extDeriv in arbitrary degree are not in Mathlib. They are prerequisites for de Rham cohomology of manifolds, for the homotopy invariance of de Rham cohomology, and for any formal treatment of gauge potentials, Chern–Simons terms or Hamiltonian mechanics that uses local primitives. The classical proof is a textbook argument; the remaining work is to formalize it against Mathlib's alternating-map API. Machine-checked versions exist elsewhere only in other representations: Mathlib proves degree 1 for 1-forms written as E → E →L F on convex sets, and this platform's Rudin chapter 10 mission has proved Poincaré's lemma (Rudin, Theorem 10.39) as Rudin.ch10_poincare_lemma and Rudin.ch10_primitive_of_closed, for its own coefficient-style KForm on convex open subsets of $\mathbb R^n$. A bridge from those statements to Mathlib's extDeriv would be a welcome contribution.

Difficulty

The obstacle is the homotopy formula in general degree. Each side involves the alternatization alternatizeUncurryFin of a derivative, the insertion curryLeft of the position vector as the first argument, and Fin.removeNth reindexing. Matching the two sides requires the signs $(-1)^i$ from moving an argument to the front to cancel exactly against those of $d$. The degree-1 shortcut through Mathlib's existing curve-integral Poincaré lemma does not generalize, because it uses a different representation of 1-forms and has no analogue in degree 2, which the essential-surjectivity clause needs. A second, routine obstacle is smoothness of $K\omega$: $E$ need not be finite-dimensional, so differentiating under the integral needs bounds that are uniform in $t \in [0,1]$ near each point.

Formalization scope

• Forms. Forms are Mathlib's E → E [⋀^Fin k]→L[ℝ] F and the exterior derivative is extDeriv. "Smooth" is ContDiff ℝ ∞, where ∞ means $C^\infty$, not analytic. $E$ is any real normed space, not necessarily finite-dimensional or complete, and $F$ is a real Banach space (CompleteSpace F), so the integral defining $K$ is the Bochner integral.
• Domain. The domain is the whole space $E$, which is star-shaped about $0$. Open subsets and manifolds are out of scope.
• Categories. Fld P is a Mathlib Discrete category. Pot P has a hand-written Category instance whose arrows are the structure GaugeHom. Fullness, faithfulness and essential surjectivity are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj.
• Non-triviality. Statements that need an object assume [Nonempty (Pot P)], meaning the field equation has a solution. Without it Pot P is empty and faithfulness and fullness hold vacuously. The cohomology conditions are explicit statements about extDeriv and grad, not definitions that make a target hold by construction. The goal fixes nothing about $P$.
• Symmetries. Spacetime symmetries are not included as arrows; as in the discrete mission, the categories compare potentials and fields over the fixed space $E$, and the only non-identity arrows are gauge transformations.
• No metric. No Hodge star or metric appears. Duality and 1-form symmetries are out of scope.
• Reusable infrastructure. The definitions file proves smoothness of extDeriv, $d^2 = 0$ in the form used here, and the gauge invariance $d(A + d\chi) = dA$. The homotopy operator, the homotopy formula and the Poincaré lemma are stated for arbitrary degree and are intended for reuse in de Rham and gauge-theory missions. Contributions toward a Mathlib-quality homotopy-operator API are welcome.

Selected references

• J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229, doi:10.1086/687936. §4: EM1/EM2, Proposition 1, footnotes 9 and 15; the erratum to Proposition 2 is on p. 15 of arXiv v2.
• M. Spivak, Calculus on Manifolds, W. A. Benjamin, 1965. Theorem 4-11 (Poincaré lemma) and its proof via the operator $I$, which is $K$ above.
• R. A. Kycia, "The Poincaré lemma, antiexact forms, and fermionic quantum harmonic oscillator", Results in Mathematics 75 (2020) 122. arXiv:1908.02349, doi:10.1007/s00025-020-01247-8.
• J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228.
• Y. Kudryashov, Mathlib, MeasureTheory/Integral/CurveIntegral/Poincare.lean (Poincaré lemma for 1-forms on convex sets), mathlib4 PR #24019.

Motivation

The homotopy hypothesis relates algebraic higher groupoids to spaces. Elementary expansions provide a concrete test of whether adjoining a higher cell preserves homotopy information. The pinned manuscript supplies the research context.

Setting

C is a globular coherator in the encoded convention, X is a cellular model, and Y is a pushout that attaches an (n+1)-disk along the source-face inclusion of an n-disk.

Formalization target

The selected goal is OAI.Grothendieck.elementary_expansion. Its central assertion is

$$X\longrightarrow X\amalg_{D_n}D_{n+1}\quad\text{is a weak equivalence}.$$

The theorem states that, for a coherator C (a globular theory, meaning a category of shapes built from globes by iterated gluing, with morphisms preserving the globular pushouts, which has a cellular presentation as a countable-stage colimit of free extensions along admissible pairs of parallel cells and in which every admissible pair is filled by some morphism), the following holds for models of C, i.e. presheaves on C sending globular pushouts to pullbacks. Let X be a cellular model, meaning that it is built from an initial model by a well-ordered transfinite composition in which each successor step attaches cells freely along boundaries of cells of the previous stage. Let n be a natural number, let a be a map from the free model disk(n) on the n-globe to X, and let J_n : disk(n) → disk(n+1) be the map induced by the source-face inclusion of the n-globe into the (n+1)-globe. If Y, together with i : X → Y and b : disk(n+1) → Y, forms a pushout square of a and J_n, then i is a weak equivalence. Here weak equivalence means that i induces a bijection on sets of components (0-cells modulo being joined by a 1-cell) and, for every 0-cell x of X and every n, a bijection on homotopy groups, which are classes of n-loops based at the degenerate cells above x, identified when joined by an (n+1)-cell.

Significance and status

The selected goal is the elementary-expansion theorem. It does not itself assert the complete equivalence between the homotopy theory of spaces and all coherator models. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The conclusion requires preservation of components and every based homotopy group, for cellular models built through transfinite attachments.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, The Grothendieck homotopy hypothesis via elementary expansions, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

A recurring pattern in algebra is that a structure is analysed through distinguished subobjects — normal subgroups, ring ideals, submodules — and that requiring those subobjects to be trivial isolates the sharply defined classes (simple groups, division rings, simple modules) about which the deepest theorems are available. The manuscript Ideals in Balanced Algebras and the Genesis of Mathematics (A. Winkler, 2020) applies that pattern to a single primitive: a partial binary operation, an operation $a\cdot b$ that need not be defined for every pair. Under one axiom — balance, which asserts that $(ab)c$ is defined exactly when $a(bc)$ is — several families of ideals appear automatically, and declaring each of them trivial (empty, or the whole algebra) carves out semigroups, monoids, quivers, associations, societies, categories, groupoids, groups and rings in turn.

No individual argument here is deep. What makes them worth machine-checking is that their content is definedness rather than equality: a statement such as "the gregarious elements form an ideal" is a claim about which products exist, proved by repeatedly moving brackets across a product that may fail to be defined at any step. Such arguments are easy to state loosely, and easy to get wrong by one implicit existence assumption. They are also the base layer on which the rest of the manuscript's programme rests. This mission formalizes that base layer: §1 (algebras, ideals, units), §2 (quivers), §4 (associators and associations), §4.1 (principal ideals) and §4.2 (the gregarious ideal).

Setting

An algebra on a type $A$ is a partial binary operation: a rule assigning to some pairs $(a,b)\in A\times A$ a value $a\cdot b\in A$. Write $a\cdot b\downarrow$ for "$a\cdot b$ is defined". In the Lean development the operation is a total function $A\to A\to\mathrm{Option}\,A$, where the value $\mathrm{none}$ means undefined. Nothing else is assumed: no totality, no unit, no associativity.

The vocabulary used throughout, all relative to this one partial product:

1. $B\subseteq A$ is a left ideal if $a\cdot b\in B$ whenever $b\in B$ and $a\cdot b\downarrow$; a right ideal if $b\cdot a\in B$ whenever $b\in B$ and $b\cdot a\downarrow$; a subalgebra if $b\cdot c\in B$ whenever $b,c\in B$ and $b\cdot c\downarrow$.
2. The right orbit of $a$ is $aA=\{c:\exists b,\ a\cdot b=c\}$; the left orbit is dual.
3. The algebra is balanced if, for all $a,b,c$, $(a\cdot b)\cdot c$ is defined if and only if $a\cdot(b\cdot c)$ is.
4. $u$ is a left unit if $u\cdot a=a$ whenever $u\cdot a\downarrow$, and $v$ is a right unit if $a\cdot v=a$ whenever $a\cdot v\downarrow$. A left unit $u$ is a source if $a\cdot u\downarrow$ only for $a=u$; a right unit $v$ is a sink if $v\cdot b\downarrow$ only for $b=v$.
5. $b$ is associating if for all $a,c$ the product $(ab)c$ is defined exactly when $a(bc)$ is, and the two values agree whenever both are defined. An association is an algebra all of whose elements are associating.
6. $b$ is gregarious if, whenever $a\cdot b\downarrow$ and $b\cdot c\downarrow$, at least one of $(ab)c$ and $a(bc)$ is defined. An association that coincides with its set of gregarious elements is a society; in the manuscript's terms, a quivered society is a category.
7. $b$ is left cancellable if $b\cdot x=b\cdot y$, with both sides defined, forces $x=y$.

Formalization targets

Goal — the gregarious ideal (§4.2)

$$\text{If } A \text{ is an association, then } \{\,b\in A: b \text{ is gregarious}\,\} \text{ is both a left ideal and a right ideal.}$$

This is the statement that gives the manuscript its notion of society: the gregarious elements of an association form the gregarious ideal, and an association whose gregarious ideal is everything is a society. The goal fixes no cardinality, no units and no totality, so it survives every specialization the manuscript makes afterwards.

Supporting targets

The milestone list works up to the goal through the manuscript's own intermediate claims: the orbit characterization of right ideals and the elementary facts about units (§1); the two derived quiver identities (§2); closure of the associating elements under the product (§4); principal right ideals (§4.1); gregariousness of sinks and sources, and the two one-sided closure statements for gregarious associating elements (§4.2); and the cancellation facts (§4) whose content is that the non-left-cancellable elements form a prime left ideal.

Significance

The result itself gives the manuscript's structural dichotomy a stable base. Once the gregarious elements are known to form an ideal, "society" is a triviality condition on an ideal rather than an ad hoc axiom, and the same is true of quivered (the elements admitting a unit on one side form an ideal, §1), of cancellative (the non-cancellable elements form a prime ideal, §4) and of principal (§4.1). The chain of specializations the manuscript then runs — association, society, quivered society, category, groupoid, group, ring — inherits whatever is proved here.

What this mission adds on top of the manuscript is machine-checked bookkeeping for partial operations. The arguments in the source are written in prose, with the existence of intermediate products often left implicit; formalizing them fixes exactly which existence facts each step consumes. The definitions published with this mission (partial algebra, ideal, balance, associating, gregarious, unit, source, sink, cancellable) are reusable for any later formalization of partial magmas, and nothing equivalent is currently in Mathlib, whose Magma-style structures are total and whose Quiver/Category hierarchy starts from typed hom-families rather than a single partial product.

Difficulty

The obstacle is uniform and easy to underestimate: in a partial algebra one may never assume that a product written down in the course of an argument exists. The naive proof of the goal — "rebracket and apply gregariousness of $b$" — fails at its first step, because from $a\cdot(bc)\downarrow$ alone one cannot conclude $a\cdot b\downarrow$; that inference is exactly what the hypothesis "$b$ is associating" supplies, and it must be invoked explicitly. Gregariousness then returns a disjunction whose two branches produce products on opposite sides of the bracket, so each branch has to be transported back independently, consuming a further associating hypothesis. Counting these obligations correctly, rather than inventing new mathematics, is the work.

Formalization scope

The partial product is A → A → Option A; none is undefined, and a · b = c is rendered as the product evaluating to some c. Subsets are Set A, with no decidability or finiteness assumptions. Ideals are arbitrary subsets and are allowed to be empty — deliberately, since the manuscript's dichotomy turns on an ideal being empty or being everything. Statements quantify over an arbitrary type, including the empty type, where they hold vacuously.

Left/right duality is not obtained from a formal opposite-algebra construction: the dual statements are stated and are to be proved separately (for instance the two one-sided society closure milestones). A contributor who prefers to build the opposite algebra once and derive each dual from its mirror is welcome to; that construction is not part of the published definitions.

The statements are not vacuous: every hypothesis used is satisfiable, since any total associative operation makes all elements associating and gregarious, and the trivial one-element monoid satisfies every unit, source, sink and cancellation hypothesis appearing in the list. No milestone is stated under a hypothesis that cannot be met.

Selected references

• A. Winkler, Ideals in Balanced Algebras and the Genesis of Mathematics, manuscript, 20 March 2020. Source text supplied by the mission owner; section and page references in the items below are to that manuscript.
• S. Eilenberg and S. Mac Lane, General theory of natural equivalences, Transactions of the American Mathematical Society 58 (1945), 231–294. https://doi.org/10.1090/S0002-9947-1945-0013131-6

Motivation

When are two scientific theories "the same theory in different words"? Philosophers of science have used two formal criteria. Definitional equivalence (Glymour) is strict: it requires a common definitional extension and therefore cannot relate theories with different numbers of sorts. Categorical equivalence (Halvorson, Weatherall) is liberal: it asks only that the categories of models be equivalent. It has been applied to classical mechanics, electromagnetism and Newtonian gravitation (Weatherall 2016; survey in Weatherall 2019).

Barrett and Halvorson (2016) proposed Morita equivalence as a syntactic criterion between these two. It allows definitions of new sorts (products, coproducts, subsorts, quotients) in addition to the usual definitions of new predicates and function symbols. Their main results place the new criterion strictly between the other two:

• Morita equivalence implies categorical equivalence (their Theorem 5.1).
• The converse fails (their Theorem 5.2).

This mission formalizes that comparison: the semantic core of Morita extensions, the implication, the separating example, and the paper's motivating "two kinds of things" example.

Setting

A signature $\Sigma$ (Sig) consists of a type of sorts, function symbols $f : \sigma_1\times\dots\times\sigma_m\to\sigma$ and predicate symbols $p\subseteq\sigma_1\times\dots\times\sigma_m$. Formulas (Formula L Γ) are built in a typed context $\Gamma$ from $\bot$, $=$, predicates, $\to$ and $\forall$. A structure (Str) assigns a nonempty set to each sort and interprets the symbols. A theory $T$ is a set of formulas in context, each read as its universal closure; a model of $T$ is a structure satisfying them all.

The category $\mathrm{Mod}(T)$ (Model T) has the models of $T$ as objects and elementary embeddings as arrows: maps on every sort that preserve and reflect every formula. Theories $T_1,T_2$ are categorically equivalent (CategoricallyEquivalent) if $\mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2)$.

A Morita extension of a $\Sigma$-theory $T$ (MoritaData L T) adds to $\Sigma$:

• new sorts, each with its defining symbols:
  • a product $\sigma$ of $\sigma_1,\sigma_2$, with projections $\pi_1,\pi_2$;
  • a coproduct, with injections $\rho_1,\rho_2$;
  • a subsort cut out by a $\Sigma$-formula $\varphi(x)$, with an injection $i$;
  • a quotient by a $\Sigma$-formula $\varphi(x_1,x_2)$, with a projection $\varepsilon$;
• new predicates and function symbols, each explicitly defined by a $\Sigma$-formula.

Each new symbol gets one defining axiom, and the symbols of one new sort share a single axiom. The extension $T^+$ (D.ext) is $T$ together with these axioms. Each definition must satisfy its admissibility condition in every model of $T$:

Definition	Condition
subsort	$\exists x\,\varphi(x)$
quotient	$\varphi$ is an equivalence relation
function symbol	$\forall x\,\exists!y\,\varphi(x,y)$

The reduct gives a functor $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ (D.proj).

$T_1$ and $T_2$ are Morita equivalent (MoritaEquivalent) if two finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ and $T_2\rightsquigarrow T_2'$ (MoritaReach) end in logically equivalent theories, that is, theories with the same models, over a common signature.

Formalization targets

Goal: Morita equivalence implies categorical equivalence

$$T_1 \text{ Morita equivalent to } T_2 \;\Longrightarrow\; \mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2).$$

Milestones

1. Unique expansion. Every model $M$ of $T$ has an expansion $N\models T^+$ with $\Pi N\cong M$, and any two such expansions are isomorphic.
2. $\Pi$ is faithful.
3. $\Pi$ is full.
4. Conservativity. For every $\Sigma$-formula $\alpha$: $T\models\alpha$ iff $T^+\models\alpha$.
5. Translation. Every $\Sigma^+$-formula whose free variables all have old sorts is $T^+$-equivalent to a $\Sigma$-formula.
6. Two kinds of things. $T_1=\{\exists x\,p(x),\ \exists x\,q(x),\ \forall x\,(p(x)\vee q(x)),\ \forall x\,\neg(p(x)\wedge q(x))\}$ over one sort is Morita equivalent to the empty theory over two sorts.
7. Separating example, first half. $T_1=\{\exists^{=1}x\,(x=x)\}$ and $T_2=T_1\cup\{\forall y\,(p_0(y)\to p_i(y)) : i\in\mathbb N\}$, over one sort and countably many unary predicates, are categorically equivalent.
8. Separating example, second half. These two theories are not Morita equivalent.

Milestones 1–3 together say that $\Pi$ is an equivalence of categories. Milestones 6–8 are not needed for the goal; they record the paper's examples, which show that Morita equivalence relates theories with different numbers of sorts and is strictly stronger than categorical equivalence.

Significance

The result itself. The goal makes Morita equivalence a syntactic sufficient condition for categorical equivalence: an explicit dictionary of definitions yields an equivalence of model categories. Milestone 8 shows the converse fails, so categorical equivalence is strictly weaker. Milestone 6 shows that Morita equivalence, unlike definitional equivalence, can relate theories with different numbers of sorts. Together these locate the criterion that later philosophy-of-physics work uses to compare formulations with different ontologies, such as different numbers of kinds of objects.

Formalizing it. The results are proved on paper and, as far as is known, have no machine-checked proofs. Mathlib's ModelTheory library is single-sorted, so none of this is available there. The mission produces a reusable many-sorted first-order logic with:

• syntax, semantics and signature maps;
• elementary embeddings and the category of models;
• Morita extensions with their reduct functors.

The paper's arguments for conservativity and translation are informal in places; for example, the translation in the appendix uses coding of new-sorted variables. A formal proof fixes these details.

Difficulty

The obvious route to the goal composes the reduct functors along the chains. The work lies in showing that each reduct is an equivalence when the arrows are elementary embeddings.

• Fullness. An elementary embedding of reducts extends uniquely to the new sorts. Showing that the extension is again elementary requires the translation of Milestone 5: every $\Sigma^+$-formula has to be pulled back to a $\Sigma$-formula, including formulas that quantify over the new sorts.
• Coproduct and quotient sorts. Quantifiers over these sorts must be eliminated in favour of quantifiers over the old sorts.

For Milestone 8 the difficulty is reversed. One must rule out every pair of chains, including chains that introduce arbitrary new sorts. The paper's proof argues with a single common Morita extension. The definition, however, allows chains, and the paper notes that a chain need not collapse to a single extension. The argument must therefore be run through conservativity and translation along each chain.

Formalization scope

• Self-contained logic. Signatures have dependent arities (Fin m → Srt). Terms and formulas use de Bruijn variables in typed contexts Γ : Fin n → Srt; Formula.all binds variable 0.
• Theories. A theory is a Set (Axiom L), each axiom being a formula in context read as its universal closure. Because sorts are nonempty, this agrees with the sentence version.
• Nonempty sorts. Every structure has nonempty carriers. This is the paper's convention, and without it Milestone 6 is false: the empty theory over two sorts would have models with an empty sort.
• Morita extensions are built, not recognized. MoritaData L T lists the new sorts and symbols and their defining $\Sigma$-formulas. The signature $\Sigma^+$ (D.sig) and the axioms are generated from it, and admissibility is stated semantically, over all models of $T$. Any Morita extension in the paper's sense is of this form up to renaming of the new symbols.
• A common signature up to renaming. MoritaEquivalent asks for a bijective signature map F between the two chain ends such that a structure is a model of $T_2'$ iff its F-reduct is a model of $T_1'$.
• Universes. Models live in Type.
• Separating example. The paper writes $T_2$ with fresh symbols $q_i$; here $T_1$ and $T_2$ share the signature with predicates $p_i$, which only renames symbols.
• No trivialization. None of the targets holds vacuously: Morita extensions require genuine admissibility proofs, and the arrows are elementary embeddings, not arbitrary maps. Milestone 6 needs explicit chains and an explicit renaming, with arity casts.

A complete development will need:

• the substitution and weakening lemmas for de Bruijn formulas;
• the realization of signature maps;
• the construction of expansions;
• a translation function from $\Sigma^+$-formulas to $\Sigma$-formulas.

These pieces are reusable for any later work on interpretations or theoretical equivalence. Alternative proofs of Milestone 8, for example by counting finitely axiomatized subtheories, are welcome.

Selected references

• T. W. Barrett, H. Halvorson, Morita Equivalence, Rev. Symb. Logic 9 (2016) 556–582. arXiv:1506.04675. Source of all targets: §3–§5 and the appendix; Example 4 and Theorems 4.1–4.3, 5.1, 5.2.
• J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. arXiv:1411.5757.
• J. O. Weatherall, Theoretical Equivalence in Physics, Philos. Compass 14 (2019). arXiv:1810.08192.
• H. Halvorson, The Logic in Philosophy of Science, Cambridge University Press, 2019. doi:10.1017/9781316275603.

Motivation

A gauge theory can be formulated in several mathematically different ways: with potentials (connections), with field strengths (curvature), or with holonomies, the parallel transports around closed loops. Philosophers and physicists ask whether these formulations say the same thing, and which one carries "surplus structure".

Category theory makes the question precise. Each formulation is a category of models, and each translation between formulations is a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. One that is all three forgets nothing and is an equivalence. This taxonomy is due to Baez, Bartels and Dolan (Baez–Shulman, §2.4).

Weatherall (2016) applied it to electromagnetism. Potentials without gauge arrows forget structure relative to field strengths (Proposition 1). The erratum in arXiv v2 (p. 15) corrects his Proposition 2: the principal-bundle formulation, whose arrows include gauge transformations, forgets only stuff, not nothing. Nguyen, Teh and Wells obtain the same verdict for the gauge-orbit functor (their Proposition 3.2.3). In their footnote 26 they identify the forgotten stuff as the constant ("global") gauge transformations. All of this is abelian, U(1) on a contractible spacetime.

The non-abelian counterpart is the holonomy formulation. Barrett's reconstruction and representation theorems, and their categorical upgrade by Rosenstock and Weatherall (Theorem 2), show that on a connected manifold, principal connections and generalized holonomy maps form equivalent categories. On the topological side, Freed and Quinn (eqs. 3.11–3.13) identify the automorphisms of a finite-group gauge field with a centralizer.

This mission states these results for an arbitrary group $G$ on a finite graph. There the smooth and topological subtleties disappear, but the categorical content survives intact.

Setting

A finite directed graph $X$ has vertices $\mathrm{Fin}\,n_V$, edges $\mathrm{Fin}\,n_E$, and maps $\mathrm{src},\mathrm{tgt}$. A step is an edge traversed forwards or backwards, and a walk $x \to y$ is a list of steps whose endpoints chain. $X$ is connected from $x$ if every vertex is reached by a walk from $x$.

• A connection is $A : E \to G$. Its holonomy along a walk is the ordered product of $A(e)$ (forwards) and $A(e)^{-1}$ (backwards), as in Baez (1996), §2.
• A gauge transformation is $g : V \to G$, acting by $(g\cdot A)(e) = g(\mathrm{src}\,e)\,A(e)\,g(\mathrm{tgt}\,e)^{-1}$.
• $\mathsf{PotG}$: objects are connections, and arrows $A \to B$ are gauge transformations with $g\cdot A = B$. This is the discrete analogue of the groupoid $C_A$ of Nguyen–Teh–Wells.
• $\mathsf{HolMap}_x$: a holonomy map at $x$ assigns a group element to each walk. It is multiplicative on loops at $x$ and unchanged when a backtrack $s, \bar s$ is inserted into a loop at $x$; this is the discrete form of thin equivalence. Arrows $H \to H'$ are elements $h$ with $H'(\gamma) = h\,H(\gamma)\,h^{-1}$ on every loop at $x$. Only values on loops at $x$ matter.
• Functors. $\mathrm{hol}_x : \mathsf{PotG} \to \mathsf{HolMap}_x$ sends $A \mapsto \mathrm{hol}_A$ and $g \mapsto g(x)$. $\mathrm{orbit}$ sends $\mathsf{PotG}$ to the discrete category of gauge orbits.
• Curvature. On a 2-complex, each face has a base vertex and a boundary loop. The curvature functor sends $A$ to the family of conjugacy classes of its face holonomies, which is the gauge-invariant non-abelian field strength.

Formalization targets

Goal: the holonomy functor is an equivalence

$$X \text{ connected from } x \;\Longrightarrow\; \mathrm{hol}_x \text{ is full, faithful and essentially surjective.}$$

This is the discrete, fixed-base-point form of Rosenstock–Weatherall's Theorem 2. In the taxonomy above, potentials-with-gauge and holonomies forget nothing relative to each other. The statement holds for every group $G$, finite or not. The base-point-changing arrows of Rosenstock–Weatherall are not included.

Milestones

1. Faithful. A gauge arrow between two connections is determined by its value at $x$.
2. Full. Every conjugation relating the holonomy maps of $A$ and $B$ is realized by a gauge transformation.
3. Barrett reconstruction. Every holonomy map at $x$ equals $\mathrm{hol}_A$ on all loops at $x$, for some connection $A$.
4. Barrett representation. $\mathrm{hol}_A = \mathrm{hol}_B$ on loops at $x$ iff $B = g\cdot A$ for a gauge transformation with $g(x) = 1$, and that $g$ is unique.
5. Stabilizer = centralizer. Evaluation at $x$ is a bijection from the gauge stabilizer of $A$ onto the centralizer of its holonomies at $x$. This is the non-abelian $H^0$, the discrete form of Freed–Quinn (3.11)–(3.13).
6. The orbit functor forgets only stuff. It is full and essentially surjective. It is faithful iff $X$ has no vertices or $G$ is trivial. This is the discrete form of Nguyen–Teh–Wells Proposition 3.2.3 and of Weatherall's corrected Proposition 2.
7. Aharonov–Bohm. Take $G$ nontrivial, abelian or not. On the boundary of a triangle, which has no faces, the curvature functor is not full: flat connections with different holonomy are not gauge-equivalent. On the filled triangle the curvature functor is full and essentially surjective but not faithful.

Significance

• Equivalence of formulations. The goal says that, once gauge transformations are arrows, the potential and holonomy formulations of non-abelian lattice gauge theory are categorically equivalent. This is the precise sense in which "the physics is in the holonomies".
• Stuff and global symmetry. Milestones 5–6 locate the forgotten stuff exactly. When potentials are compared with gauge-invariant data that lacks arrows, the stuff is the centralizer of the holonomy group, the global gauge symmetry that survives a choice of connection. In the abelian case this is Nguyen–Teh–Wells' footnote 26. In general it is the automorphism group that weights the Dijkgraaf–Witten / Freed–Quinn sum.
• Topology. Milestone 7 shows that on a non-simply-connected graph the curvature formulation also forgets structure. Weatherall's footnote 9 sets this situation aside for Minkowski space.
• Novelty. Each ingredient is classical in some setting. A machine-checked statement of the non-abelian classification on finite graphs, in the language of forgetful functors, does not appear to exist. It is a step towards treating the theories-as-categories programme formally.

Difficulty

• Combinatorics of walks. Lists of steps, their endpoint conditions, and the interaction of concatenation with backtracking all have to be handled explicitly. The goal and Milestones 1–4 need statements about walks between arbitrary vertices, not only loops.
• Essential surjectivity. Reconstruction has to produce a connection from data that is only constrained on loops at one vertex. Connectivity enters non-trivially.
• Faithfulness versus fullness. These use the hypotheses differently, and the boundary cases (empty graph, trivial group) have to be tracked.
• Milestone 7 needs explicit non-equivalences, and so a gauge invariant separating gauge orbits.

Formalization scope

• Graphs. These are finite directed graphs with Fin-indexed cells and are not required to be simple. Loops and multiple edges are allowed. A 2-complex adds faces with a base vertex and a boundary walk proved to be a loop.
• Groups. $G$ is any Group; finiteness is not assumed.
• Holonomy maps. These are functions on all lists of steps whose axioms only constrain loops at $x$. Two maps agreeing on loops are isomorphic in $\mathsf{HolMap}_x$ (via $h = 1$) but need not be equal. Reconstruction is therefore stated on loops.
• Functor properties. These are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj. The goal is their conjunction, not an explicitly constructed inverse.
• Excluded. Spacetime symmetries (graph automorphisms), base-point-changing holonomy isomorphisms, and smooth or continuum statements are left out.
• Proved in the definitions. Gauge covariance of holonomy along walks is proved in the definitions file, because the functors require it.

Selected references

• J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229. arXiv v2 includes the erratum to Proposition 2 (p. 15).
• J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228
• S. Rosenstock, J. O. Weatherall, "A categorical equivalence between generalized holonomy maps on a connected manifold and principal connections on bundles over that manifold", J. Math. Phys. 57 (2016) 102902. arXiv:1504.02401
• D. S. Freed, F. Quinn, "Chern–Simons theory with finite gauge group", Comm. Math. Phys. 156 (1993) 435–472. arXiv:hep-th/9111004
• J. C. Baez, M. Shulman, "Lectures on n-categories and cohomology", in Towards Higher Categories, Springer (2010) 1–68. arXiv:math/0608420
• J. C. Baez, "Spin network states in gauge theory", Adv. Math. 117 (1996) 253–272. arXiv:gr-qc/9411007

Motivation

Philosophers of physics ask when a formulation of a theory carries excess structure: mathematical distinctions between models that make no physical difference. The standard example is electromagnetism written with a vector potential $A$. Potentials that differ by a gauge transformation $A \mapsto A + d\lambda$ have the same field strength $F = dA$, and on the usual view they represent the same physical situation.

Weatherall (2016) made this precise with category theory. Each formulation becomes a category of models, and a translation between formulations becomes a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. Weatherall's Proposition 1 says the functor $A \mapsto dA$ from potentials to field strengths forgets only structure, provided the arrows between potentials are spacetime symmetries that preserve $A$. His Proposition 2 says the principal-bundle formulation, whose arrows include gauge transformations, forgets nothing. His footnote 15 notes that adding gauge transformations as arrows between potentials yields a category equivalent to that of field strengths (Weatherall, arXiv:1411.5757).

These arguments work on Minkowski space, which is contractible. Weatherall's footnote 9 sets topology aside for that reason. The follow-up literature, for example Nguyen, Teh and Wells (2018), compares these and related functors further. This mission states the comparison exactly on a finite cell complex, where topology cannot be set aside. Each of the three ways a functor can forget information then corresponds to one cohomology group.

Setting

A finite oriented 2-complex $X$ has $n_V$ vertices, $n_E$ edges and $n_P$ faces, together with integer incidence numbers $\partial_1(e,v)$ and $\partial_2(p,e)$ satisfying $\sum_e \partial_2(p,e)\,\partial_1(e,v) = 0$ for every face $p$ and vertex $v$. Nothing beyond this identity is required, so the incidence data need not come from a geometric complex; all results hold for any such integer data. Fix an additive commutative group $K$ of coefficients, for example $\mathbb{Z}$, $\mathbb{R}$, or $\mathbb{Z}/n$ as a discrete stand-in for $U(1)$. The cochains are $C^0 = K^{V}$ (gauge parameters $\lambda$), $C^1 = K^{E}$ (potentials $A$) and $C^2 = K^{P}$ (field strengths $F$). The coboundaries are

$$(\delta^0\lambda)(e) = \sum_v \partial_1(e,v)\,\lambda(v), \qquad (\delta^1 A)(p) = \sum_e \partial_2(p,e)\,A(e),$$

and $\delta^1\delta^0 = 0$.

There are three categories, with spacetime symmetries taken to be trivial:

• $\mathsf{Fld}$ (Weatherall's EM1): its objects are the 2-cochains $F$, and its only arrows are identities.
• $\mathsf{Pot}_0$ (Weatherall's EM2): its objects are the 1-cochains $A$, and its only arrows are identities.
• $\mathsf{Pot}_G$ (potentials with gauge arrows): its objects are the 1-cochains $A$. An arrow $A \to A'$ is a gauge parameter $\lambda \in C^0$ with $A + \delta^0\lambda = A'$, and composition adds the parameters. Arrows are the parameters $\lambda$ themselves, so two parameters differing by an element of $\ker\delta^0$ (e.g. a constant) are distinct arrows, just as distinct vertical automorphisms are distinct arrows in Weatherall's bundle category EM3. This is the category of his footnote 15.

The field-strength functors $\mathsf{Pot}_0 \to \mathsf{Fld}$ and $\mathsf{Pot}_G \to \mathsf{Fld}$ send $A \mapsto \delta^1 A$. In the second functor every gauge arrow goes to an identity.

Cohomology vanishing is stated elementarily:

• $H^0 = 0$ means $\delta^0\lambda = 0 \Rightarrow \lambda = 0$.
• $H^1 = 0$ means every $A$ with $\delta^1 A = 0$ equals $\delta^0\lambda$ for some $\lambda$.
• $H^2 = 0$ means every $F$ equals $\delta^1 A$ for some $A$.

Formalization targets

Goal: the cohomological classification

For every finite 2-complex $X$ and coefficient group $K$, the functor $\mathsf{Pot}_G \to \mathsf{Fld}$ satisfies

$$\text{faithful} \iff H^0 = 0,\qquad \text{full} \iff H^1 = 0,\qquad \text{essentially surjective} \iff H^2 = 0.$$

Milestones

1. Proposition 1 analogue. If some $\delta^0\lambda \neq 0$, then $\mathsf{Pot}_0 \to \mathsf{Fld}$ is faithful and not full, and it is essentially surjective iff $H^2 = 0$.
2. Faithful iff $H^0 = 0$.
3. Full iff $H^1 = 0$.
4. Essentially surjective iff $H^2 = 0$.
5. Aharonov–Bohm. On the triangle boundary circle3 with $\mathbb{Z}$ coefficients, the potential equal to $1$ on one edge has the same field strength as $0$. No gauge arrow connects the two, so the functor is not full.
6. Forgetting only stuff. On the filled triangle with $\mathbb{Z}$ coefficients, the functor is full and essentially surjective but not faithful.

Significance

The result. The classification turns a qualitative philosophical diagnostic into a cohomological criterion.

• Structure: Weatherall's "forgets structure" verdict for potentials without gauge arrows is the statement that $\ker\delta^1 \neq 0$.
• Topology: once gauge arrows are added, whether any structure is still forgotten is exactly the question whether $H^1 \neq 0$. A nonzero $H^1$ is the Aharonov–Bohm situation, in which potentials with equal field strength differ by a gauge-invariant holonomy.
• Stuff: the clause $\text{faithful} \iff H^0 = 0$ shows that on a geometric complex (every edge has boundary head minus tail) with at least one vertex and $K \neq 0$, constant gauge parameters are non-identity automorphisms that the functor sends to identities. The functor therefore forgets stuff. This contrasts with the faithfulness clause of Weatherall's Proposition 2 for the bundle formulation, where the analogous constant vertical automorphisms are the subtle case.

Formalizing it. No machine-checked version of the theories-as-categories programme for gauge theory is known to the author of this mission. This mission is the base case of a planned discrete gauge-functor development: non-abelian groups, nontrivial symmetry groups, and holonomy-based equivalences.

Difficulty

The mathematics is elementary once stated. The work is in making the categorical notions line up with the cochain conditions. Three points need care:

• In a discrete category, an isomorphism is an equality.
• Fullness must be tested against arrows between arbitrary pairs of potentials, not only potentials with zero field strength.
• Faithfulness concerns parallel gauge arrows, which differ exactly by elements of $\ker\delta^0$.

The concrete milestones require computations on explicit complexes, including a gauge-invariant obstruction for the Aharonov–Bohm example.

Formalization scope

• Complexes. Cells are indexed by Fin types, and the incidence numbers are integer-valued. The complex is finite but may be empty in any dimension.
• Coefficients. $K$ is any AddCommGroup, and integers act on it by zsmul.
• Categories. Fld and Pot0 are Mathlib Discrete categories. PotG carries a hand-written Category instance whose arrows are the structure GaugeHom.
• Functor properties. Fullness, faithfulness and essential surjectivity are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj.
• Symmetries. Spacetime symmetries are fixed to be trivial, so the results compare categories of potentials and fields over a fixed complex.
• Non-triviality. The cohomology conditions are explicit Props about the coboundaries, so none of them is a definition that makes a target hold trivially. The hypothesis of Milestone 1 excludes the degenerate case $\delta^0 = 0$, in which that functor is full.
• Infrastructure. The cochain API (delta0, delta1, $\delta^1\delta^0 = 0$) is proved in the definitions file and is reusable for discrete gauge theory and toric-code missions.

Selected references

• J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229, doi:10.1086/687936
• J. O. Weatherall, "Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?". arXiv:1411.5757
• J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228

Motivation

Quantum mechanics predicts probabilities, but it is notoriously quiet about what a probability is. Categorical quantum mechanics answers that by rewriting the finite-dimensional formalism in the language of dagger categories: a state is a morphism $I \to A$, an effect is a morphism $A \to I$, and the probability of an outcome is a scalar — an endomorphism of the tensor unit. On that translation the Born rule stops being an axiom and becomes a theorem about a complete, disjoint family of effects.

This mission formalizes that theorem, together with the two lemmas it rests on, in Lean 4 over Mathlib. It covers the dagger and measurement material of Chapter 2 of Reutter and Vicary's Categorical Quantum Mechanics.

Setting

Fix a monoidal dagger category $\mathcal{C}$ with zero morphisms. The unit object $I$ carries a commutative monoid structure $\mathrm{End}(I)$ — the scalars. For a state $a : I \to c$ and an effect $x : c \to I$, the probability that $x$ occurs on $a$ is the scalar

$$\mathrm{Prob}(a,x) \;=\; a^\dagger \circ x^\dagger \circ x \circ a .$$

A family of effects $x : I \to \mathrm{Eff}(c)$ is complete when the induced map $\langle x \rangle : \bigoplus_i I \to c$ satisfies $\bigvee_i x_i = \mathrm{id}_c$, and disjoint when $x_i^\dagger \circ x_j = 0$ for $i \neq j$. Both conditions are stated for a dagger biproduct of the unit objects.

Formalization targets

Goal — the Born rule

$$\sum_{i} \mathrm{Prob}(a, x_i) \;=\; \mathrm{id}_I \qquad \text{for } x \text{ complete and disjoint}$$

This is the mission's goal. It fixes nothing beyond completeness and disjointness; the statement is exactly the categorical Born rule for a finite outcome set.

Supporting results

• Lemma 2.52. A family of effects is disjoint if and only if the dagger of its lift is an isometry; and complete if and only if the kernel of its lift is trivial.
• Lemma 2.53. A complete and disjoint family of effects lifts to a unitary $\langle x \rangle : \bigoplus_i I \to c$.
• Lemma 2.41, Corollary 2.42. Dagger biproducts: transposing a matrix of morphisms daggers every entry, and daggers distribute over addition.

Significance

The Born rule is the point where the categorical and the Hilbert-space pictures are reconciled: the abstract statement specialises, in $\mathbf{Hilb}$, to the usual $\sum_i |\langle x_i | a \rangle|^2 = 1$. Proving it categorically means the rule is a consequence of the dagger-biproduct structure rather than an extra assumption, which is what makes the framework usable for quantum protocols — measurement, teleportation and the like are all built on complete disjoint families.

The supporting lemmas are reusable well beyond this mission: dagger biproducts are the categorical home of matrix calculus, and the isometry/unitary characterisations of disjointness and completeness are the standard toolkit for any later argument about measurements.

Difficulty

Moderate. The mathematics is elementary once the definitions are in place — the work is in bookkeeping: biproduct universal properties, the interaction of the dagger with the biproduct structure, and careful handling of the scalar monoid. The main intellectual step is realising that completeness alone, not equalizers, gives the second unitary identity.

Formalization scope

Formalized here: dagger categories and their morphism classes (§2.3), dagger biproducts (§2.3.3), and the scalar/state/effect vocabulary with the Born rule (§2.4.3). Mathlib has no dagger-category theory at all, so the definitions are supplied from scratch as Lean Definitions and are importable independently of this mission.

Not formalized: the Hilbert-space and relational models, the graphical calculus of §2.2, and the measurement/post-processing material after §2.4.3.

Two corrections to the source are made and documented in the formalization. The printed statement of Proposition 2.55 assumes completeness only, which is false; disjointness is required, as the book's own proof (which invokes Lemma 2.52) already assumes. And the book attributes the identity $x^\dagger \circ x = \mathrm{id}$ on $A$ to Lemma 2.52, whereas Lemma 2.52 only gives the identity on $\bigoplus_i I$; the identity on $A$ is Lemma 2.53. Lemma 2.53 is proved here without the book's equalizer hypothesis, so it is strictly stronger than the printed version.

Selected references

• D. Reutter and J. Vicary, Categorical Quantum Mechanics, §2.3.3 and §2.4.3.
• S. Abramsky and B. Coecke, A categorical semantics of quantum protocols, LICS 2004.
• The Mathlib CategoryTheory.Limits.Biproducts and CategoryTheory.Monoidal.Category API, on which the definitions are built.