-
Topological Quantum Gates in Homotopy Type Theory
Authors:
David Jaz Myers,
Hisham Sati,
Urs Schreiber
Abstract:
Despite the evident necessity of topological protection for realizing scalable quantum computers, the conceptual underpinnings of topological quantum logic gates had arguably remained shaky, both regarding their physical realization as well as their information-theoretic nature.
Building on recent results on defect branes in string/M-theory and on their holographically dual anyonic defects in co…
▽ More
Despite the evident necessity of topological protection for realizing scalable quantum computers, the conceptual underpinnings of topological quantum logic gates had arguably remained shaky, both regarding their physical realization as well as their information-theoretic nature.
Building on recent results on defect branes in string/M-theory and on their holographically dual anyonic defects in condensed matter theory, here we explain how the specification of realistic topological quantum gates, operating by anyon defect braiding in topologically ordered quantum materials, has a surprisingly slick formulation in parameterized point-set topology, which is so fundamental that it lends itself to certification in modern homotopically typed programming languages, such as cubical Agda.
We propose that this remarkable confluence of concepts may jointly kickstart the development of topological quantum programming proper as well as of real-world application of homotopy type theory, both of which have arguably been falling behind their high expectations; in any case, it provides a powerful paradigm for simulating and verifying topological quantum computing architectures with high-level certification languages aware of the actual physical principles of realistic topological quantum hardware.
In a companion article, we will explain how further passage to "dependent linear" homotopy data types naturally extends this scheme to a full-blown quantum programming/certification language in which our topological quantum gates may be compiled to verified quantum circuits, complete with quantum measurement gates and classical control.
△ Less
Submitted 4 March, 2023;
originally announced March 2023.
-
Commuting Cohesions
Authors:
David Jaz Myers,
Mitchell Riley
Abstract:
Shulman's spatial type theory internalizes the modalities of Lawvere's axiomatic cohesion in a homotopy type theory, enabling many of the constructions from Schreiber's modal approach to differential cohomology to be carried out synthetically. In spatial type theory, every type carries a spatial cohesion among its points and every function is continuous with respect to this. But in mathematical pr…
▽ More
Shulman's spatial type theory internalizes the modalities of Lawvere's axiomatic cohesion in a homotopy type theory, enabling many of the constructions from Schreiber's modal approach to differential cohomology to be carried out synthetically. In spatial type theory, every type carries a spatial cohesion among its points and every function is continuous with respect to this. But in mathematical practice, objects may be spatial in more than one way at the same time; for example, a simplicial space has both topological and simplicial structures.
In this paper, we put forward a type theory with "commuting focuses" which allows for types to carry multiple kinds of spatial structure. The theory is a relatively painless extension of spatial type theory, and enables us to give a synthetic account of simplicial, differential, equivariant, and other cohesions carried by the same types. We demonstrate the theory by showing that the homotopy type of any differential stack may be computed from a discrete simplicial set derived from the Čech nerve of any good cover. We also give other examples of commuting cohesions, such as differential equivariant types and supergeometric types, laying the groundwork for a synthetic account of Schreiber and Sati's proper orbifold cohomology.
△ Less
Submitted 31 January, 2023;
originally announced January 2023.
-
Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory
Authors:
David Jaz Myers
Abstract:
Informally, an orbifold is a smooth space whose points may have finitely many internal symmetries. Formally, however, the notion of orbifold has been presented in a number of different guises -- from Satake's V-manifolds to Moerdijk and Pronk's proper étale groupoids -- which do not on their face resemble the informal definition. The reason for this divergence between formalism and intuition is th…
▽ More
Informally, an orbifold is a smooth space whose points may have finitely many internal symmetries. Formally, however, the notion of orbifold has been presented in a number of different guises -- from Satake's V-manifolds to Moerdijk and Pronk's proper étale groupoids -- which do not on their face resemble the informal definition. The reason for this divergence between formalism and intuition is that the points of spaces cannot have internal symmetries in traditional, set-level foundations. The extra data of these symmetries must be carried around and accounted for throughout the theory. More drastically, maps between orbifolds presented in the usual ways cannot be defined pointwise.
In this paper, we will put forward a definition of orbifold in synthetic differential cohesive homotopy type theory: an orbifold is a microlinear type for which the type of identifications between any two points is properly finite. In homotopy type theory, a point of a type may have internal symmetries, and we will be able to construct examples of orbifolds by defining their type of points directly. Moreover, the map** space between two orbifolds is merely the type of functions.
We will justify this synthetic definition by proving, internally, that every proper étale groupoid is an orbifold. In this way, we will show that the synthetic theory faithfully extends the usual theory of orbifolds. Along the way, we will investigate the microlinearity of higher types such as étale groupoids, showing that the methods of synthetic differential geometry generalize gracefully to higher analogues of smooth spaces. We will also investigate the relationship between the Dubuc-Penon and open-cover definitions of compactness in synthetic differential geometry, and show that any discrete, Dubuc-Penon compact subset of a second-countable manifold is subfinitely enumerable.
△ Less
Submitted 31 May, 2022;
originally announced May 2022.
-
Modal Fracture of Higher Groups
Authors:
David Jaz Myers
Abstract:
In this paper, we examine the modal aspects of higher groups in Shulman's Cohesive Homotopy Type Theory. We show that every higher group sits within a modal fracture hexagon which renders it into its discrete, infinitesimal, and contractible components. This gives an unstable and synthetic construction of Schreiber's differential cohomology hexagon. As an example of this modal fracture hexagon, we…
▽ More
In this paper, we examine the modal aspects of higher groups in Shulman's Cohesive Homotopy Type Theory. We show that every higher group sits within a modal fracture hexagon which renders it into its discrete, infinitesimal, and contractible components. This gives an unstable and synthetic construction of Schreiber's differential cohomology hexagon. As an example of this modal fracture hexagon, we recover the character diagram characterizing ordinary differential cohomology by its relation to its underlying integral cohomology and differential form data, although there is a subtle obstruction to generalizing the usual hexagon to higher types. Assuming the existence of a long exact sequence of differential form classifiers, we construct the classifiers for circle k-gerbes with connection and describe their modal fracture hexagon.
△ Less
Submitted 29 June, 2021;
originally announced June 2021.
-
Behavioral Mereology: A Modal Logic for Passing Constraints
Authors:
Brendan Fong,
David Jaz Myers,
David I. Spivak
Abstract:
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may…
▽ More
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may assume a completely elementary set-theoretic discussion. We consider the relationship between various parts of a whole in terms of how behavioral constraints are passed between them, and give an inter-modal logic that generalizes the usual alethic modalities in the setting of symmetric accessibility.
△ Less
Submitted 25 January, 2021;
originally announced January 2021.
-
Cartesian Factorization Systems and Grothendieck Fibrations
Authors:
David Jaz Myers
Abstract:
Every Grothendieck fibration gives rise to a vertical/cartesian orthogonal factorization system on its domain. We define a cartesian factorization system to be an orthogonal factorization in which the left class satisfies 2-of-3 and is closed under pullback along the right class. We endeavor to show that this definition abstracts crucial features of the vertical/cartesian factorization system asso…
▽ More
Every Grothendieck fibration gives rise to a vertical/cartesian orthogonal factorization system on its domain. We define a cartesian factorization system to be an orthogonal factorization in which the left class satisfies 2-of-3 and is closed under pullback along the right class. We endeavor to show that this definition abstracts crucial features of the vertical/cartesian factorization system associated to a Grothendieck fibration, and give comparisons between various 2-categories of factorization systems and Grothendieck fibrations to demonstrate this relationship. We then give a construction which corresponds to the fiberwise opposite of a Grothendieck fibration on the level of cartesian factorization systems.
Apart from the final double categorical results, this paper is entirely review of previously established material. It should be read as an expository note.
△ Less
Submitted 20 January, 2021; v1 submitted 24 June, 2020;
originally announced June 2020.
-
Double Categories of Open Dynamical Systems (Extended Abstract)
Authors:
David Jaz Myers
Abstract:
A (closed) dynamical system is a notion of how things can be, together with a notion of how they may change given how they are. The idea and mathematics of closed dynamical systems has proven incredibly useful in those sciences that can isolate their object of study from its environment. But many changing situations in the world cannot be meaningfully isolated from their environment - a cell will…
▽ More
A (closed) dynamical system is a notion of how things can be, together with a notion of how they may change given how they are. The idea and mathematics of closed dynamical systems has proven incredibly useful in those sciences that can isolate their object of study from its environment. But many changing situations in the world cannot be meaningfully isolated from their environment - a cell will die if it is removed from everything beyond its walls. To study systems that interact with their environment, and to design such systems in a modular way, we need a robust theory of open dynamical systems.
In this extended abstract, we put forward a general definition of open dynamical system. We define two general sorts of morphisms between these systems: covariant morphisms which include trajectories, steady states, and periodic orbits; and contravariant morphisms which allow for plugging variables of some systems into parameters of other systems. We define an indexed double category of open dynamical systems indexed by their interface and use a double Grothendieck construction to construct a double category of open dynamical systems.
In our main theorem, we construct covariantly representable indexed double functors from the indexed double category of dynamical systems to an indexed double category of spans. This shows that all covariantly representable structures of dynamical systems - including trajectories, steady states, and periodic orbits - compose according to the laws of matrix arithmetic.
△ Less
Submitted 3 February, 2021; v1 submitted 12 May, 2020;
originally announced May 2020.
-
Dirichlet Functors are Contravariant Polynomial Functors
Authors:
David Jaz Myers,
David I. Spivak
Abstract:
Polynomial functors are sums of covariant representable functors from the category of sets to itself. They have a robust theory with many applications -- from operads and opetopes to combinatorial species. In this paper, we define a contravariant analogue of polynomial functors: Dirichlet functors. We develop the basic theory of Dirichlet functors, and relate them to their covariant analogues.
Polynomial functors are sums of covariant representable functors from the category of sets to itself. They have a robust theory with many applications -- from operads and opetopes to combinatorial species. In this paper, we define a contravariant analogue of polynomial functors: Dirichlet functors. We develop the basic theory of Dirichlet functors, and relate them to their covariant analogues.
△ Less
Submitted 8 April, 2020;
originally announced April 2020.
-
Dirichlet Polynomials form a Topos
Authors:
David I. Spivak,
David Jaz Myers
Abstract:
One can think of power series or polynomials in one variable, such as $P(x)=2x^3+x+5$, as functors from the category $\mathsf{Set}$ of sets to itself; these are known as polynomial functors. Denote by $\mathsf{Poly}_{\mathsf{Set}}$ the category of polynomial functors on $\mathsf{Set}$ and natural transformations between them. The constants $0,1$ and operations $+,\times$ that occur in $P(x)$ are a…
▽ More
One can think of power series or polynomials in one variable, such as $P(x)=2x^3+x+5$, as functors from the category $\mathsf{Set}$ of sets to itself; these are known as polynomial functors. Denote by $\mathsf{Poly}_{\mathsf{Set}}$ the category of polynomial functors on $\mathsf{Set}$ and natural transformations between them. The constants $0,1$ and operations $+,\times$ that occur in $P(x)$ are actually the initial and terminal objects and the coproduct and product in $\mathsf{Poly}_{\mathsf{Set}}$.
Just as the polynomial functors on $\mathsf{Set}$ are the copresheaves that can be written as sums of representables, one can express any Dirichlet series, e.g.\ $\sum_{n=0}^\infty n^x$, as a coproduct of representable presheaves. A Dirichlet polynomial is a finite Dirichlet series, that is, a finite sum of representables $n^x$. We discuss how both polynomial functors and their Dirichlet analogues can be understood in terms of bundles, and go on to prove that the category of Dirichlet polynomials is an elementary topos.
△ Less
Submitted 4 November, 2020; v1 submitted 10 March, 2020;
originally announced March 2020.
-
A Yoneda-Style Embedding for Virtual Equipments
Authors:
David Jaz Myers
Abstract:
In this paper, we exhibit a "Yoneda"-style embedding of any virtual equipment into the virtual equipment of categories enriched in it. We show that this embedding preserves composition, is full on 2-cells and arrows, and coreflective on proarrows.
In this paper, we exhibit a "Yoneda"-style embedding of any virtual equipment into the virtual equipment of categories enriched in it. We show that this embedding preserves composition, is full on 2-cells and arrows, and coreflective on proarrows.
△ Less
Submitted 2 March, 2020;
originally announced March 2020.
-
Good Fibrations through the Modal Prism
Authors:
David Jaz Myers
Abstract:
Homotopy type theory is a formal language for doing abstract homotopy theory -- the study of identifications. But in unmodified homotopy type theory, there is no way to say that these identifications come from identifying the path-connected points of a space. In other words, we can do abstract homotopy theory, but not algebraic topology. Shulman's Real Cohesive HoTT remedies this issue by introduc…
▽ More
Homotopy type theory is a formal language for doing abstract homotopy theory -- the study of identifications. But in unmodified homotopy type theory, there is no way to say that these identifications come from identifying the path-connected points of a space. In other words, we can do abstract homotopy theory, but not algebraic topology. Shulman's Real Cohesive HoTT remedies this issue by introducing a system of modalities that relate the spatial structure of types to their homotopical structure. In this paper, we develop a theory of modal fibrations for a general modality, and apply it in particular to the shape modality of Real Cohesion. We then give examples of modal fibrations in Real Cohesive HoTT, and develop the theory of covering spaces.
△ Less
Submitted 4 April, 2022; v1 submitted 21 August, 2019;
originally announced August 2019.
-
Node Diversification in Complex Networks by Decentralized Coloring
Authors:
Richard Garcia-Lebron,
David J. Myers,
Shouhuai Xu,
Jie Sun
Abstract:
We develop a decentralized coloring approach to diversify the nodes in a complex network. The key is the introduction of a local conflict index that measures the color conflicts arising at each node which can be efficiently computed using only local information. We demonstrate via both synthetic and real-world networks that the proposed approach significantly outperforms random coloring as measure…
▽ More
We develop a decentralized coloring approach to diversify the nodes in a complex network. The key is the introduction of a local conflict index that measures the color conflicts arising at each node which can be efficiently computed using only local information. We demonstrate via both synthetic and real-world networks that the proposed approach significantly outperforms random coloring as measured by the size of the largest color-induced connected component. Interestingly, for scale-free networks further improvement of diversity can be achieved by tuning a degree-biasing weighting parameter in the local conflict index.
△ Less
Submitted 27 November, 2018;
originally announced November 2018.
-
Behavioral Mereology (Proofs and Properties)
Authors:
Brendan Fong,
David Jaz Myers,
David I. Spivak
Abstract:
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may…
▽ More
Mereology is the study of parts and the relationships that hold between them. We introduce a behavioral approach to mereology, in which systems and their parts are known only by the types of behavior they can exhibit. Our discussion is formally topos-theoretic, and agnostic to the topos, providing maximal generality; however, by using only its internal logic we can hide the details and readers may assume a completely elementary set-theoretic discussion. We consider the relationship between various parts of a whole in terms of how behavioral constraints are passed between them, and give an inter-modal logic that generalizes the usual alethic modalities in the setting of symmetric accessibility.
△ Less
Submitted 2 July, 2020; v1 submitted 1 November, 2018;
originally announced November 2018.
-
String Diagrams For Double Categories and Equipments
Authors:
David Jaz Myers
Abstract:
A popular graphical calculus for monoidal categories makes computations tactile and intuitive. Complicated diagram chases can be expressed in a few pictures and discovered by playing with a shoelace. Joyal and Street's proof of the soundness of this calculus says that any deformation of a diagram, any bending of the strings, describes the same morphism. In this paper, we extend the graphical calcu…
▽ More
A popular graphical calculus for monoidal categories makes computations tactile and intuitive. Complicated diagram chases can be expressed in a few pictures and discovered by playing with a shoelace. Joyal and Street's proof of the soundness of this calculus says that any deformation of a diagram, any bending of the strings, describes the same morphism. In this paper, we extend the graphical calculus to double categories and proarrow equipments in order to bring the string diagrammatic method to formal category theory. Our main theorem proves this calculus sound with the help of Dawson and Pare's results on composition in double categories.
△ Less
Submitted 2 March, 2018; v1 submitted 8 December, 2016;
originally announced December 2016.
