Enriched Categories for Parameterized Circuit Semantics

Scott Wesley

REVIEW 3 major objections 4 minor 40 references

Enriched Categories for Parameterized Circuit Semantics

T0 review · 3 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Parameterized quantum circuits form braided monoidal categories.

desk verdict Correct but standard change-of-base construction; the promised link to prior parameterized semantics is asserted, not proved. read the letter →

arxiv 2501.12481 v1 pith:SA7KSOGR submitted 2025-01-21 quant-ph cs.LO

Scott Wesley This is my paper · ORCID

classification quant-phcs.LO MSC 18D2018M0518M1081P68

keywords enrichedcategorytheorymonoidalcategoriesbraidedparameterizedquantumcircuitscircuitsemanticsstringdiagramsCartesianequivalencechecking

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper aims to give parameterized families of quantum circuits the same mathematical treatment that ordinary circuits already have: string diagrams in a monoidal category. Its central claim is that if the semantic category is enriched over a Cartesian category $V$, then a parameter object $P$ produces a category $\mathrm{Param}(P,\mathcal{C})$ whose morphisms are parameterized maps, and this category inherits composition, tensor product, and braiding from the original semantics. The result is that parameterized ansatz circuits can be reasoned about with the full categorical toolkit, and prior semantics by continuous parameter functions and by Laurent-polynomial matrices become instances. The paper also embeds parameter-free circuits into the parameterized category as constant families and shows that evaluating at a parameter is a strict monoidal functor.

What carries the argument

The load-bearing object is the enriched hom-object $\mathcal{C}(X,Y)$ together with the parameter object $P$ in a Cartesian category $V$; a $V$-enriched category is one whose homs are objects of $V$ with composition and identity maps living in $V$. A parameterized morphism is defined to be a $P$-shaped element, that is, a morphism $P \to \mathcal{C}(X,Y)$ in $V$. The machinery is the pair of structural maps supplied by the Cartesian structure: the diagonal $\Delta_P : P \to P \times P$ that copies the parameter and the unique deleting map $e_P : P \to I$ that discards it. Precomposing the enriched category's associator, unitors, and braiding with $e_P$ defines the corresponding structure on $\mathrm{Param}(P,\mathcal{C})$, and because deletion is compatible with copying in a Cartesian category, all coherence equations lift.

What would settle it

Exhibit a parameterized circuit family from [20] whose parameter object changes with the number of wires or with earlier parameter choices and show that it cannot be written as $V(P,\mathcal{C}(X,Y))$ for one fixed $P$; that would refute the claimed agreement with prior parameterized semantics.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central result is Theorem 3.14: for any Cartesian category $V$, any $V$-enriched category $\mathcal{C}$, and any parameter object $P$, the category $\mathrm{Param}(P,\mathcal{C})$ whose morphisms $X \to Y$ are the $P$-shaped elements of the hom-object (morphisms $P \to \mathcal{C}(X,Y)$ in $V$) is monoidal, and it is braided when $\mathcal{C}$ is braided; if the enriched braiding $\beta$ is symmetric, then so is the induced braiding $b$. Composition copies the parameter through the diagonal $\Delta_P$ and then composes inside $\mathcal{C}$, and the tensor product does the same before applying the enriched tensor. The structural morphisms $a$, $\ell$, $r$, and $b$ are defined by precomposing the enriched $\alpha$, $\lambda$, $\rho$, and $\beta$ with the deleting map $e_P$, which preserves invertibility and coherence. The parameter-free category embeds as constant families, and each evaluation functor $\mathrm{ev}_\theta$ is strict braided monoidal, so the construction is a categorical account of parameterized semantics rather than an ad hoc model.

Load-bearing premise

In Section 3.1 the paper chooses to model every parameterized morphism as a single $P$-shaped element $P \to \mathcal{C}(X,Y)$ of the enriched hom-object, and it motivates this choice with examples rather than a proof that it captures the semantics of [10] and [20].

Editorial extensions

If this is right

Evaluating a parameterized circuit at any concrete generalized parameter $\theta : I \to P$ is a strict braided monoidal functor $\mathrm{ev}_\theta$, so evaluation commutes with composition and tensor product.
The parameter-free semantics $\mathcal{C}$ is a retract of $\mathrm{Param}(P,\mathcal{C})$: the embedding $j$ that sends $f$ to the constant family $f \circ e_P$ is strict braided monoidal and faithful whenever $P$ has a generalized element, with $\mathrm{ev}_\theta \circ j = \mathrm{id}_{\mathcal{C}}$.
When the enriched braiding is symmetric, the parameterized category is symmetric monoidal, so the usual four-dimensional string-diagram manipulations apply to parameterized circuits.
The construction recovers expected behavior on simple examples, such as $R_X(\theta_1) \star R_X(2\theta_2) = R_X(\theta_1 + 2\theta_2)$ in the $\mathbf{Top}$-enriched category of finite-dimensional vector spaces with parameter space $\mathbb{R}^2$.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A direct next step suggested by the construction is parameterized equivalence checking: in $\mathrm{Param}(P,\mathcal{C})$, two circuits are equal as parameterized morphisms exactly when their evaluations agree for every generalized parameter, so equality in this category is the object an equivalence-checking algorithm should decide.
The restriction to Cartesian $V$ is convenient but probably not essential; if $P$ carries a comonoid structure in a non-Cartesian $V$, the same diagonal-composition recipe would assemble a category, although deletion would no longer be unique.
In Heyting-semilattice enrichment, $\mathrm{Param}(P,\mathcal{C})$ grades morphisms by entailment at truth value $P$, which could turn classical program analyses into a family of parameterized logical categories; the paper mentions the direction but does not develop these consequences.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Here's the short version: the paper builds a category Param(P,C) of P-shaped elements of an enriched hom, shows it's monoidal/braided, and claims this unifies prior parameterized circuit semantics. The math is correct as far as it goes, but it's a standard change-of-base construction (Kelly's Basic Concepts, hom-functor V(P,-): V→Set), and the claimed agreement with Jeandel et al. and Miller-Bakewell is never actually demonstrated.

What's genuinely nice: the exposition is clear, the string-diagram proofs are readable, and the meet-semilattice example is a good illustration of how the construction works even when evaluation is meaningless. Lemma 3.2 and the evaluation functors are cleanly handled, and the embedding j in Section 4 correctly captures the 'constant parameter' intuition. The heredity theorems are correct; the omitted second braiding hexagon is indeed a routine chase and one can fill it in without trouble.

The load-bearing soft spot is the abstract's promise: 'the parameterized semantics studied in prior work can be understood through enrichment.' The paper never states which V, P, and C make [10] or [20] an instance, nor gives a denotation functor from their circuit syntax into Param. Example 3.4 checks one rotation gate; that is not a semantics. If the intended contribution is 'here is a clean unifying framework,' that framing needs a theorem or at least a precise dictionary. If the contribution is just the abstract construction, then it should be honest that the construction is change of base and the novelty is in the application, not the mathematics.

Also the 'first work to consider categorical semantics for parameterized circuits' sentence in Section 5 is hard to square with [10] and [20] being exactly that. Perhaps it means 'first via enrichment,' but as written it's an overclaim.

Minor: the paper's own Discussion gestures at change of base but doesn't connect it to Param(P,C); that's a missed citation and an opportunity to position the result accurately. The gap in Appendix J is minor.

Verdict: the central theorem holds; the advertised semantics bridge is unproven. This is a solid workshop paper with a fixable overreach. It deserves a serious referee, not a desk reject, because the construction is correct and the examples are illuminating. But the referee should require the author to either prove the agreement with prior work or substantially soften the claims. I'd cite it only as an example application of change of base, and I wouldn't bring it to reading group unless someone is working on parameterized circuits.

Referee Report

3 major / 4 minor

Summary. The paper proposes a categorical model of parameterized circuit semantics. Fixing a Cartesian monoidal category V, a V-enriched category C, and a parameter object P in V, the authors define a category Param(P,C) whose morphisms are P-shaped elements of the enriched hom-objects, i.e. morphisms P → C(X,Y) in V. They prove that Param(P,C) is a category, that it inherits monoidal structure when C is a V-monoidal category, and braided/symmetric monoidal structure when C is V-braided/symmetric. They also define evaluation functors ev_θ and an embedding j of the parameter-free category into the parameterized one, showing that ev_θ is a retraction of j. The paper claims that this construction 'agrees with' and generalizes the parameterized circuit semantics of prior work [10,20], and it offers several examples plus an extended discussion of possible applications to equivalence checking and logic-based abstraction.

Significance. If the central construction and coherence theorems are correct, the paper provides a clean categorical home for parameterized circuit semantics: rather than hard-coding parameters into the semantic category, parameters become generalized elements of enriched hom-objects, and the monoidal/braided structure is inherited from the base semantics. This is a potentially useful unifying perspective, especially for connecting categorical circuit analysis with analytic techniques. The paper is a definition-theorem-example paper, with many diagrammatic proofs supplied in appendices and explicit examples (e.g., R^2-parameterized rotations in Top-enriched FVect). Its strengths include the self-contained presentation of enriched monoidal categories, the explicit treatment of evaluation and constant embedding as categorical structure, and the demonstration that the construction is well-behaved for non-concrete base categories such as meet semilattices.

major comments (3)

[Introduction and Section 3.1] The paper's central advertised claim is that Param(P,C) 'agrees with' and generalizes the parameterized circuit semantics of [10] and [20], but no theorem, functor, or equivalence is exhibited. For [10], the intended instantiation would presumably be V=Top, P=R (or R^n), and C=FVect, but this is never stated. For [20], which uses matrices over complex Laurent polynomials, it is not even clear which V and P would make finite-support Laurent polynomials into P-shaped elements. Examples 3.4 and 3.5 check single gates and an abstract poset example; Lemma 3.2 and Theorem 3.3 show evaluation is functorial. None of these establish that the full denotation functors of [10] or [20] factor through Param(P,C). Since the abstract's claim that parameterized semantics 'can be understood through enrichment' rests on this bridge, the paper should either state and prove a precise correspondence theorem (e.g., an isomorphism or faithful embedding of the relevant semantic categories) or explicitly downgrade the agreement claim to a conjecture or illustration.
[Appendix J / Theorem 3.14] The proof of Theorem 3.14, that Param(P,C) is braided monoidal, is incomplete: after proving the first braiding hexagon, the text states only that the second coherence condition 'follows in a similar fashion' and provides no diagram chase or other argument. Since Theorem 3.14 is one of the two main structural results of the paper, a referee cannot verify the braided structure from the manuscript as submitted. The missing proof should be included, or the theorem should be supported by a machine-checked proof.
[Theorem 3.1 and Section 2.1] The proof of Theorem 3.1, and the definition of the underlying category in Section 2.1, contain a variance error involving the unitor. In Section 2.1 the composite of generalized elements is defined as 'MC ◦ (g ⊗ f) ◦ ρ_I', and in the proof of Theorem 3.1 the equality '∆_I = ρ_I' is used. But the unitor ρ_I is a morphism I⊗I → I, whereas the composite requires a morphism I → I⊗I, namely ρ_I^{-1} (or λ_I^{-1}); similarly the diagonal ∆_I is the unique morphism I → I⊗I, i.e. ρ_I^{-1}, not ρ_I. As written, the formula is not well-typed. The statement Param(I,C)=C is true, but the proof must be corrected by replacing ρ_I with ρ_I^{-1} in the relevant places.

minor comments (4)

[Corollary 3.15] In the proof of Corollary 3.15, the final sentence says 'for each θ ∈ V(I,C)' but the intended domain is V(I,P).
[Corollary 4.2] The statement of Corollary 4.2 contains a typo: 'F or eachθ ∈ V(I, C)' should read 'For each θ ∈ V(I, P)'.
[Example 3.5] The discussion of the meet-semilattice example would be clearer if the authors explicitly noted that the underlying category C has homsets V(⊤, C_V(X,Y)) = { ⋆ | ⊤ ≤ C_V(X,Y) }, so that the graph with edges labeled ⊤ is exactly the underlying category; the current text moves quickly from the labeled graph to the posetal quotient.
[Section 2.1] The sentence defining composition in the underlying category should be revised to use the inverse unitor, which would remove the ambiguity noted in the third major comment.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the monoidal and braided structure of Param(P,C) is derived from the stated definitions of P-shaped elements and standard enriched category theory; the asserted agreement with prior work is an unproved external-validity bridge, not a circular step.

full rationale

The paper's central theorems (3.1, 3.10, 3.14) are proved by explicit diagram chases from the definition of Param(P,C): morphisms are P-shaped elements V(P, C(X,Y)), composition is MC∘(g×f)∘Δ_P, and the identity is 1∘e_P. The monoidal and braided structures are defined as inclusions a=α∘e_P, ℓ=λ∘e_P, r=ρ∘e_P, and b=β∘e_P, and the coherence proofs in Appendices H and J verify the pentagon and hexagon equations by reducing them to the corresponding coherence of C together with the Cartesian equations Δ=σ∘Δ and θ∘e_P=e_I. No parameter is fitted and no prediction is renamed from data; the results are conditional theorems under the stated hypotheses that V is Cartesian and C is a (braided/symmetric) V-monoidal category. The paper contains no self-citations, and the cited enriched-category definitions [14,15] are standard external background, not load-bearing assertions imported from the author's own prior work. The introduction claims that the construction 'agrees with' the parameterized semantics of [10,20], but this bridge is asserted rather than proved by an explicit equivalence or factoring functor, and Example 3.4 only checks a single rotation gate. That is an external-validity or completeness gap, not circularity: Theorem 3.14 holds independently of whether the bridge to prior work is correct. The skeptical reader's concern is therefore best classified as insufficient support for a side claim, not as a circular derivation.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central construction depends on two assumptions: V is a Cartesian monoidal category (so every object P admits uniform copying and deleting), and C is a V-enriched monoidal or braided category. Both are standard domain assumptions, not ad hoc inventions. The paper introduces no free parameters and no new physical or logical entities; Param(P,C) is a definition derived from the input data. The only unstated background is the standard body of enriched category theory, which the paper cites as [14].

assumptions (3)

domain assumption V is a Cartesian monoidal category with uniform copying Δ and uniform deleting e
Required so that each object P has a comonoid structure; used in the definitions of composition (Δ_P), identities (e_P), and the monoidal product (Δ_P). See Section 3.1.
domain assumption C is a V-category (and, for the heredity theorems, V-monoidal or V-braided)
The semantic category is assumed to be enriched over V; the monoidal and braided assumptions are later lifted to Param(P,C). See Sections 3.2 and 3.3.
standard math Standard definitions and results of enriched category theory and monoidal categories
The paper relies on Kelly [14] and Mac Lane [19] for background; no novel unproved background is introduced.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Enriched Categories for Parameterized Circuit Semantics." pith.science (2026). https://pith.science/paper/SA7KSOGR

@misc{pith2026250112481,
  author       = {Pith},
  title        = {Pith review of: Enriched Categories for Parameterized Circuit Semantics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SA7KSOGR}},
  note         = {Machine review of arXiv:2501.12481}
}

abstract

It is well-known that combinatorial circuits are modeled mathematically by string diagrams in a monoidal category. Given a gate set $\Sigma$, the circuits over $\Sigma$ can be thought of as string diagrams in the free monoidal category generated by $\Sigma$. In this model, circuit semantics are then given by monoidal functors out of this free category. For quantum circuits, this functor is often valued in the category of unitary matrices. This model suffices for concrete quantum circuits, but fails to describe parameterized families of quantum circuits, such as those which arise in the analysis of ansatz circuits. Intuitively, this functor should be valued in parameterized families of unitary matices, though it is not immediately clear what this mean through a categorical lens. In this paper, we show that the parameterized semantics studied in prior work can be understood through enrichment and internal constructions. We determine sufficient conditions under which this construction yields a symmetric monoidal category, and suggest how these semantics could be extended to classical circuit analysis and parameterized equivalence checking.

Figures

Figures reproduced from arXiv: 2501.12481 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 25 canonical work pages

[10]

In: Logic in Computer Science, ACM, pp

Emmanuel Jeandel, Simon Perdrix & Renaud Vilmart (2018 ): Diagrammatic reasoning beyond Clifford+T quantum mechanics. In: Logic in Computer Science, ACM, pp. 569–578, doi: 10.1145/3209108.3209139

arXiv 2018
[20]

EPTCS 318, pp

Hector Miller-Bakewell (2020): Finite veriﬁcation of inﬁnite families of diagram equation s. EPTCS 318, pp. 27–52, doi: 10.4204/eptcs.318.3

doi:10.4204/eptcs.318.3 2020
[1]

Quantum 5, p

Miriam Backens, Hector Miller-Bakewell, Giovanni de Fe lice, Leo Lobski & John van de Wetering (2021): There and back again: A circuit extraction tale . Quantum 5, p. 421, doi: 10.22331/q-2021-03-25-421

doi:10.22331/q-2021-03-25-421 2021
[2]

Richard Blute & Philip Scott (2004): Category Theory for Linear Logicians . In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet & Philip Scott, editors: Linear Logic in Computer Science , London Mathematical Society Lecture Note Series, Cambridge University Press, pp. 3–64

work page 2004
[3]

In: Principles of Programming Languages , Association for Computing Machinery, pp

Patrick Cousot & Radhia Cousot (1977): Abstract interpretation: a uniﬁed lattice model for static analy- sis of programs by construction or approximation of ﬁxpoint s. In: Principles of Programming Languages , Association for Computing Machinery, pp. 238–252, doi: 10.1145/512950.512973

arXiv 1977
[4]

Bishop, Steven Heidel, Colm A

Andrew Cross, Ali Javadi-Abhari, Thomas Alexander, Nie l De Beaudrap, Lev S. Bishop, Steven Heidel, Colm A. Ryan, Prasahnt Sivarajah, John Smolin, Jay M. Gambet ta & Blake R. Johnson (2022): OpenQASM 3: A Broader and Deeper Assembly Language . ACM Trans. on Quantum Comp. 3(3)

work page 2022
[5]

Self-published

Richard Hammack (2009): Book of Proof . Self-published. Available at https://richardhammack. github.io/BookOfProof/

work page 2009
[6]

Pearson, doi:10.5555/1841628

David Harris & Neil Weste (2010): CMOS VLSI Design: A Circuits and Systems Perspective . Pearson, doi:10.5555/1841628

work page doi:10.5555/1841628 2010

Show all 40 references

[7]

Oxford University Press, doi:10.1093/oso/9780198739623.001.0001

Chris Heunen & Jamie Vicary (2019): Categories for Quantum Theory: An Introduction . Oxford University Press, doi:10.1093/oso/9780198739623.001.0001

2019
[8]

Elektronische Infor- mationsverarbeitung und Kybernetik 1(1), pp

G¨ unter Hotz (1965): Eine Algebraisierung des Syntheseproblems von Schaltkrei sen I. Elektronische Infor- mationsverarbeitung und Kybernetik 1(1), pp. 185–205

1965
[9]

Bir gitta Whaley & E

William Huggins, Piyush Patil, Bradley Mitchell, K. Bir gitta Whaley & E. Miles Stoudenmire (2019): T o- wards quantum machine learning with tensor networks . Quantum Science and Technology 4(2), p. 024001, doi:10.1088/2058-9565/aaea94

2019 doi
[11]

Springer, doi: 10.1007/3-540-44761-X

Thomas Jech (2003): Set Theory. Springer, doi: 10.1007/3-540-44761-X

2003 doi
[12]

Advances in Mathematics 88(1), pp

Andr´ e Joyal & Ross Street (1991): The geometry of tensor calculus, I . Advances in Mathematics 88(1), pp. 55–112, doi: 10.1016/0001-8708(91)90003-P

1991 doi
[13]

M Kelly (1964): On MacLane’s conditions for coherence of natural associati vities, commutativities, etc

G. M Kelly (1964): On MacLane’s conditions for coherence of natural associati vities, commutativities, etc. Journal of Algebra 1(4), pp. 397–402, doi: 10.1016/0021-8693(64)90018-3

1964 doi
[14]

Springer, doi: 10.1112/blms/15.1.96

Max Kelly (1982): Basic Concepts of Enriched Category Theory . Springer, doi: 10.1112/blms/15.1.96

1982 doi
[15]

Advances in Mathemat- ics 323, p

Liang Kong & Hao Zheng (2018): Drinfeld center of enriched monoidal categories . Advances in Mathemat- ics 323, p. 411–426, doi: 10.1016/j.aim.2017.10.038

2018 doi
[16]

arXiv: 2407.03673

Alexander Koziell-Pipe & Aleks Kissinger (2024): Hybrid quantum-classical machine learning with string diagrams. arXiv: 2407.03673

2024 arXiv
[17]

Journal of Pure and Applied Algebra 184(2), pp

Yves Lafont (2003): T owards an algebraic theory of Boolean circuits. Journal of Pure and Applied Algebra 184(2), pp. 257–310

2003
[18]

Rice University Studies 49, pp

Saunders Mac Lane (1963): Natural associativity and commutativity . Rice University Studies 49, pp. 28–46

1963
[19]

Springer, doi: 10.1007/ 978-1-4757-4721-8

Saunders Mac Lane (2010): Categories for the W orking Mathematician . Springer, doi: 10.1007/ 978-1-4757-4721-8

2010
[21]

IEEE Journal on Emerging and Selected Topics in Circuits and Systems 12(3), pp

Tom Peham, Lukas Burgholzer & Robert Wille (2022): Equivalence Checking of Quantum Circuits With the ZX-Calculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems 12(3), pp. 662–675, doi:10.1109/jetcas.2022.3202204. 14 Enriched Categories for Parameterized ...

2022
[22]

In: New Structures for Physics, Springer, pp

Peter Selinger (2010): A survey of graphical languages for monoidal categories . In: New Structures for Physics, Springer, pp. 289–355, doi: 10.1007/978-3-642-12821-9_4

2010 doi
[23]

Springer, doi: 10.1007/ 978-3-662-03927-4

Heribert V ollmer (1982): Introduction to Circuit Complexity: A Uniform Approach . Springer, doi: 10.1007/ 978-3-662-03927-4

1982
[24]

arXiv: 2401.12877

John van de Wetering, Richie Y eung, Tuomas Laakkonen & A leks Kissinger (2024): Optimal compilation of parametrised quantum circuits, doi:10.48550/arXiv.2401.12877. arXiv: 2401.12877

2024 doi arXiv
[25]

Acar & Zhihao Jia (2022): Quartz: superoptimization of quantum circuits

Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Poi nting, Auguste Hirth, Henry Ma, Jens Pals- berg, Alex Aiken, Umut A. Acar & Zhihao Jia (2022): Quartz: superoptimization of quantum circuits . In: Programming Language Design and Implementation (PLDI) , ACM, pp. 625–640,...

2022 doi
[26]

A collection C0

Objects. A collection C0
[27]

For each X ,Y ∈ C0, a set C (X ,Y ) whose elements are denoted X f − →Y

Morphisms. For each X ,Y ∈ C0, a set C (X ,Y ) whose elements are denoted X f − →Y
[28]

For each X ∈ C0, a morphism 1 X ∈ C (X , X )

Identities. For each X ∈ C0, a morphism 1 X ∈ C (X , X )
[29]

For each X ,Y, Z ∈ C0, a function ◦ : C (Y, Z) × C (X ,Y ) → C (X , Z)

Composition. For each X ,Y, Z ∈ C0, a function ◦ : C (Y, Z) × C (X ,Y ) → C (X , Z). This data satisﬁes the following conditions
[30]

For each X f − →Y g − →Z h− →Z, h ◦ (g ◦ f ) = (h ◦ g) ◦ f

Associativity. For each X f − →Y g − →Z h− →Z, h ◦ (g ◦ f ) = (h ◦ g) ◦ f
[31]

For each X f − →Y , 1Y ◦ f = f = f ◦ 1X

Unitality. For each X f − →Y , 1Y ◦ f = f = f ◦ 1X . Example A.2. Common categories include Set (sets and functions), FVect (ﬁnite-dimensional C-vector spaces and linear transformations), Top (topological spaces and continuous functions), Cat (categories and functors) and Pos ...
[32]

For each X f − →Y g − →Z, FX,Z(g ◦ f ) = FY,Z(g) ◦ FX,Y ( f )

Composition Preservation. For each X f − →Y g − →Z, FX,Z(g ◦ f ) = FY,Z(g) ◦ FX,Y ( f ). 16 Enriched Categories for Parameterized Circuit Semantics
[33]

For each X ∈ C0, FX,X (1X ) = 1F0(X)

Identity Preservation. For each X ∈ C0, FX,X (1X ) = 1F0(X). If FX,Y is inject for each X ,Y ∈ C , then F is faithful. Deﬁnition A.5 ([19]). A natural transformation η : F ⇒ G between functors is an indexed family of morphisms η X : F0(X ) → G0(X ) such that the following diag...
[34]

A functor ⊗ : C × C → C

Monoidal Product. A functor ⊗ : C × C → C
[35]

An object I ∈ C0

Monoidal Unit. An object I ∈ C0
[36]

A natural isomorphism α : (−) ⊗ ((−) ⊗ (−)) ⇒ ((−) ⊗ (−)) ⊗ (−)

Associator. A natural isomorphism α : (−) ⊗ ((−) ⊗ (−)) ⇒ ((−) ⊗ (−)) ⊗ (−)
[37]

Natural isomorphism λ : I ⊗ (−) ⇒ (−) and ρ : (−) ⊗ I ⇒ (−)

Unitors. Natural isomorphism λ : I ⊗ (−) ⇒ (−) and ρ : (−) ⊗ I ⇒ (−). This data is subject to the condition that the following diag rams commute for all X ,Y, Z,W ∈ C0. (X ⊗Y ) ⊗ (Z ⊗W ) X ⊗ (Y ⊗ (Z ⊗W )) (( X ⊗Y ) ⊗ Z) ⊗W X ⊗ ((Y ⊗ Z) ⊗W ) ( X ⊗ (Y ⊗ Z)) ⊗W α (X⊗Y,Z,W)α (X,Y,...
[38]

J = F(I)

Preserves Units. J = F(I)
[39]

If X f − →Y and X ′ g − →Y ′, then F( f ⊗ g) = F( f ) ⊠ F(g)

Preserves Products. If X f − →Y and X ′ g − →Y ′, then F( f ⊗ g) = F( f ) ⊠ F(g)
[40]

For each X ,Y, Z ∈ C0, F(α (X,Y,Z)) = a(X,Y,Z), F(λ X ) = ℓX , and F(ρ X ) = rX

Preserves Structure. For each X ,Y, Z ∈ C0, F(α (X,Y,Z)) = a(X,Y,Z), F(λ X ) = ℓX , and F(ρ X ) = rX . Moreover, when C admits a braiding β and D admits a braiding b, then F is a (strict) braided monoidal functor when F(β (X,Y )) = b(F(X),F(Y )) for each X ,Y ∈ C0. The equatio...

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [10]

In: Logic in Computer Science, ACM, pp

Emmanuel Jeandel, Simon Perdrix & Renaud Vilmart (2018 ): Diagrammatic reasoning beyond Clifford+T quantum mechanics. In: Logic in Computer Science, ACM, pp. 569–578, doi: 10.1145/3209108.3209139

arXiv 2018

[2] [20]

EPTCS 318, pp

Hector Miller-Bakewell (2020): Finite veriﬁcation of inﬁnite families of diagram equation s. EPTCS 318, pp. 27–52, doi: 10.4204/eptcs.318.3

doi:10.4204/eptcs.318.3 2020

[3] [1]

Quantum 5, p

Miriam Backens, Hector Miller-Bakewell, Giovanni de Fe lice, Leo Lobski & John van de Wetering (2021): There and back again: A circuit extraction tale . Quantum 5, p. 421, doi: 10.22331/q-2021-03-25-421

doi:10.22331/q-2021-03-25-421 2021

[4] [2]

Richard Blute & Philip Scott (2004): Category Theory for Linear Logicians . In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet & Philip Scott, editors: Linear Logic in Computer Science , London Mathematical Society Lecture Note Series, Cambridge University Press, pp. 3–64

work page 2004

[5] [3]

In: Principles of Programming Languages , Association for Computing Machinery, pp

Patrick Cousot & Radhia Cousot (1977): Abstract interpretation: a uniﬁed lattice model for static analy- sis of programs by construction or approximation of ﬁxpoint s. In: Principles of Programming Languages , Association for Computing Machinery, pp. 238–252, doi: 10.1145/512950.512973

arXiv 1977

[6] [4]

Bishop, Steven Heidel, Colm A

Andrew Cross, Ali Javadi-Abhari, Thomas Alexander, Nie l De Beaudrap, Lev S. Bishop, Steven Heidel, Colm A. Ryan, Prasahnt Sivarajah, John Smolin, Jay M. Gambet ta & Blake R. Johnson (2022): OpenQASM 3: A Broader and Deeper Assembly Language . ACM Trans. on Quantum Comp. 3(3)

work page 2022

[7] [5]

Self-published

Richard Hammack (2009): Book of Proof . Self-published. Available at https://richardhammack. github.io/BookOfProof/

work page 2009

[8] [6]

Pearson, doi:10.5555/1841628

David Harris & Neil Weste (2010): CMOS VLSI Design: A Circuits and Systems Perspective . Pearson, doi:10.5555/1841628

work page doi:10.5555/1841628 2010