Schreiber Towards Quantum Programming via Linear Homotopy Types

Urs Schreiber:

Towards Quantum Programming via Linear Homotopy Types

talk at

Homotopy Type Theory and Computing – Classical and Quantum,

CQTS @ New York University Abu Dhabi

19-21 April 2024

Abstract. Remarkably, among the $\infty$ -toposes into which HoTT interprets are “tangent $\infty$ -toposes” of parameterized module spectra, which behave like semantics for an enhancement of HoTT by dependent *linear* homotopy types, neatly combining the linear aspect of typed quantum programming languages (like Proto-Quipper) with homotopy-theoretic aspects needed for future *topological quantum* languages. The talk surveys this HoTT-perspective on (topological) quantum systems, developed jointly with Hisham Sati (“Topological Quantum Gates in HoTT” arXiv:2303.02382, “Entanglement of Sections” arXiv:2309.07245, “The Quantum Monadology” arXiv:2310.15735, “Quantum and Reality” arXiv:2311.11035).

Contents

Quantum Systems via Linear Homotopy Types
Modal Quantum Circuit Logic via Dependent Linear Types
Topological Quantum Gates via Linear Type Transport

(1) Quantum Systems via Linear Homotopy Types

Following Awodey 2009, it is now well-understood [Cisinski 2012, 2014; Shulman 2015, 2019] that

univalent $\;$ HoTT $\;$ finds its categorical semantics

\array{ &&&& \big[ (\Gamma, x \colon A, y \colon B(x)) \big] \\ &&&& \Big\downarrow \mathrlap{ {}^{ \big[ \Gamma, x \colon A \,\vdash\, B(x) \colon Type \big] } } \\ [\Gamma] && \overset{ [\Gamma \vdash a \colon A] } {\longrightarrow} && \big[ (\Gamma, x \colon A) \big] \\ & {}_{id}\searrow && \swarrow_{\mathrlap{[\Gamma \vdash A \colon Type]}} \\ && [\Gamma] }

in $\infty$ -toposes presented by well-behaved (type-theoretic) model categories.

Remarkably [Biedermann 2007; Joyal 2008; Hoyois 2019],

among these $\infty$ -toposes are

tangent $\infty$ -toposes $\;T^R Grpd_\infty$

of parameterized $R$ -module spectra

over varying $\infty$ -groupoids (cf. the talk by Finster).

This can be surprising, because these are amalgamations

T^R Grpd_\infty \;\;\;\; \simeq \;\;\;\; \int_{\mathcal{X} \in Grpd_\infty} \, R Mod^{\mathcal{X}}

of stable $\infty$ -categories $R Mod^{\mathcal{X}}$

of parameterized $R$ -module spectra over fixed bases $\mathcal{X}$

which as such are far from being $\infty$ -toposes themselves.

This fact can indeed be so surprising that

when I first highlighted it to a HoTT-audience in 2014 (slide 6)

it was ferociously doubted.

Specifically [Robinson 1987; Shipley 2007],

when $R \equiv H\mathbb{C}$ is the Eilenberg-MacLane spectrum of the complex numbers, say, then

$H\mathbb{C} Mod \;\simeq\; Ch_{\mathbb{C}} \;\;$ is equivalent to $\mathbb{C}$ -chain complexes
$H \mathbb{C} Mod^{\mathcal{X}} \;\simeq\; Loc_{\mathbb{X}}\big(\mathcal{X}\big) \;\;$ is equivalent to flat $\infty$ -vector bundles (aka “ $\infty$ -local systems”) over $\mathcal{X}$ .

More concretely [Sati and S. 2023, Prop. 3.23 p. 40]:

a model category-presentation for $T^{H\mathbb{R}} Grpd_\infty$

is given by the integral model structure for

the projective model structures of simplicial functor categories

from simplicial groupoids to the model structure on simplicial chain complexes

\mathbf{Loc}_{\mathbb{C}} \;=\; \int_{\mathbf{X} \in sGrpd} \mathbf{sCh}_{\mathbb{C}}^{\mathbf{X}} \,.

Alongside its Cartesian product, this category carries

(“external”) symmetric monoidal tensor product-structure $\boxtimes$ :

\begin{array}{l} \big( \mathscr{V}_1 \,\colon\, \mathbf{X}_1 \longrightarrow \mathbf{sCh}_{\mathbb{C}} \big) \boxtimes \big( \mathscr{V}_2 \,\colon\, \mathbf{X}_2 \longrightarrow \mathbf{sCh}_{\mathbb{C}} \big) \\ \;\coloneqq \;\; \Big( \mathrm{pr}_1^\ast \mathscr{V}_1 \otimes \mathrm{pr}_2^\ast \mathscr{V}_2 \;\;\coloneqq\;\; \mathbf{X}_1 \times \mathbf{X}_2 \longrightarrow \mathbf{sCh}_{\mathbb{C}} \Big) \,. \end{array}

It turns out [Sati and S. 2023, Thm. 3.42 p. 53, Rem. 344 p. 54],

that this is rather well-behaved

as far as models categories for parameterized spectra go [cf. Malkiewich 2023]

but it is not quite a $\boxtimes$ -monoidal model category-structure.

However [Sati and S. 2023, Thm. 3.46 p. 56]

it becomes monoidal model

when restricted to 1-truncated classical base types,

Loc^{Grpd}_{\mathbb{C}} \;=\; \int_{\mathcal{X} \in Grpd} sCh_{\mathbb{C}}^{\mathcal{X}} \,.

So this is a well-behaved extension by symmetric monoidal chain complexes

of the original groupoid model for 1-truncated HoTT [Hofmann & Streicher 1994].

To get a sense of the nature of this extension,

focus on the “hearts” of these fiber-wise stable symmetric monoidal $\infty$ -categories, which form

over the point:

the category of complex vector spaces

$\mathbb{C} Mod \xhookrightarrow{\phantom{---}} Ch_\bullet(\mathbb{C}) \xhookrightarrow{\phantom{---}} T^{H \mathbb{C}} Grpd_\infty$
over any base homotopy type $\mathcal{X}$ :

its category of flat vector bundles (“local systems”)

$\mathbb{C} Mod^{\mathcal{X}} \xhookrightarrow{\phantom{---}} Ch_\bullet(\mathbb{C})^{\mathcal{X}} \xhookrightarrow{\phantom{---}} T^{H \mathbb{C}} Grpd_\infty$
over varying discrete base spaces:

the category of indexed sets of complex vector spaces,

hence the free coproduct completion of $Mod_{\mathbb{C}}$ :

$\int_{W \colon Set} \mathbb{C} Mod^{W} \;\;\;\xhookrightarrow{\phantom{---}}\;\;\; \int_{W \colon Set} Ch_\bullet(\mathbb{C})^{W} \;\;\;\xhookrightarrow{\phantom{---}}\;\;\; T^{H \mathbb{C}} Grpd_\infty \,.$