Author Description

Login to generate an author description

Ask a Question About This Mathematician

Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
This thesis introduces the language QML, a functional language for quantum computations on finite types.QML exhibits quantum data and control structures, and integrates reversible and irreversible quantum computations.The design of … This thesis introduces the language QML, a functional language for quantum computations on finite types.QML exhibits quantum data and control structures, and integrates reversible and irreversible quantum computations.The design of QML is guided by the categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive operational semantics of irreversible quantum computations, realisable as quantum circuits.The quantum circuit model is also given a formal categorical definition via the category FQC.QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings, which may lead to the collapse of the quantum wavefunction, explicit.Strict programs are free from measurement, and hence preserve superpositions and entanglement.A denotational semantics of QML programs is presented, which maps QML terms into superoperators, via the operational semantics, made precise by the category Q.Extensional equality for QML programs is also presented, via a mapping from FQC morphisms into the category Q. CONTENTS ix 8 Further research 8.1 Compositionality of QML 8.2 A direct denotational semantics for QML 8.3 Infinite data structures and recursion in QML 8.4 Other areas of further research 8.5 Summary 9 Summary and conclusions 9.1 List of publications References A Shor's algorithm and the Quantum Fourier Transform A.1 Efficient factoring: Shor's algorithm A.2 From period finding to factoring A.3 Probability Analysis A.4 Haskell implementation of Shor's algorithm A.5 Order-finding by phase estimation A.6 Implementing the three qubit Quantum Fourier Transform A.7 Summary x
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model … We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and /spl eta/-rules for /spl Pi/and /spl Sigma/-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously developed denotational … We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously developed denotational semantics of QML. The completeness proof also gives rise to a normalisation algorithm following the normalisation-by-evaluation approach. The current work focuses on the pure fragment of QML, omitting measurements.
We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and … We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and measurement. The effectful part can be modelled using a generalisation of monads called arrows. We express the resulting executable model of quantum computing in the Haskell programming language using its special syntax for arrow computations. However, the embedding in Haskell is not perfect: a faithful model of quantum computing requires type capabilities that are not directly expressible in Haskell.
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In … Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.
Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by … Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory - a higher inductive-inductive type - we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we … As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda.
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of … In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an one, containing a strict equality type former, and an one, which is some version of HoTT. Our type theory is inspired by Voevosky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we no not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of infinite structures which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with schematic definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a … We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda.
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the loop space of the suspension of A + 1. Equivalently, this … Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the loop space of the suspension of A + 1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit: F(A), cons: A~F(A)~F(A), and conditions saying that every cons(a) is an auto-equivalence on F(A). Assuming that A is a set (i.e. satisfies the principle of unique identity proofs), we are interested in the question whether F(A) is a set as well, which is very much related to an open problem in the HoTT book [22, Ex. 8.2]. We show an approximation to the question, namely that the fundamental groups of F(A) are trivial, i.e. that ||F(A)||1 is a set.
Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories … Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g. a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we don't know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work.
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we … As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda. Comment: 36 pages, to appear in the special issue of TLCA'13 (LMCS)
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of … In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an "outer" one, containing a strict equality type former, and an "inner" one, which is some version of HoTT. Our type theory is inspired by Voevosky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we no not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of "infinite structures" which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with "schematic" definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
Abstract Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that … Abstract Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (HoTT), is a preferable and should be considered as an alternative.
Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [13]. Following up on our previous formalisation [3] … Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [13]. Following up on our previous formalisation [3] and Brunerie's notes [6], we present a new formalisation of the syntax of weak ω-groupoids in Agda using heterogeneous equality. We show how to recover basic constructions on ω-groupoids using suspension and replacement. In particular we show that any type forms a groupoid and we outline how to derive higher dimensional composition. We present a possible semantics using globular sets and discuss the issues which arise when using globular types instead.
We show that the model of quantum computation based on density matrices and superoperators can be decomposed in a pure classical (functional) part and an effectful part modeling probabilities and … We show that the model of quantum computation based on density matrices and superoperators can be decomposed in a pure classical (functional) part and an effectful part modeling probabilities and measurement. The effectful part can be modeled using a generalization of monads called arrows. We express the resulting executable model of quantum computing in the programming language Haskell using its special syntax for arrow computations. The embedding in Haskell is however not perfect: a faithful model of quantum computing requires type capabilities which are not directly expressible in Haskell.
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a … We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda.
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
Abstract My goal is to give an accessible introduction to Martin’s work on the groupoid model and how it is related to the recent notion of univalence in Homotopy Type … Abstract My goal is to give an accessible introduction to Martin’s work on the groupoid model and how it is related to the recent notion of univalence in Homotopy Type Theory while sharing some memories of Martin.
We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory. We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory.
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory. We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory.
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven … Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it is difficult because once there is a term witnessing parametricity, it also has to be parametric itself and this results in the appearance of higher dimensional cubes. In previous theories with internal parametricity, either an explicit syntax for higher cubes is present or the theory is extended with a new sort for the interval. In this paper we present a type theory with internal parametricity which is a simple extension of Martin-L\"of type theory: there are a few new type formers, term formers and equations. Geometry is not explicit in this syntax, but emergent: the new operations and equations only refer to objects up to dimension 3. We show that this theory is modelled by presheaves over the BCH cube category. Fibrancy conditions are not needed because we use span-based rather than relational parametricity. We define a gluing model for this theory implying that external parametricity and canonicity hold. The theory can be seen as a special case of a new kind of modal type theory, and it is the simplest setting in which the computational properties of higher observational type theory can be demonstrated.
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of Locally Cartesian Closed Categories (LCCCs) with disjoint … Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of Locally Cartesian Closed Categories (LCCCs) with disjoint coproducts and W-types. Although it is claimed that these developments can also be interpreted in extensional Martin-L\"of type theory, this interpretation is not made explicit. Moreover, as a result of extensionality, these developments freely assume Uniqueness of Identity Proofs (UIP), so it is not clear whether this is a necessary condition. In this paper, we present a formalisation of the result that `containers preserve least and greatest fixed points' in Cubical Agda, thereby giving a formulation in intensional type theory, and showing that UIP is not necessary. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda's path type to coinductive proofs.
The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-L\"of Type Theory to asymmetric … The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-L\"of Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model and is the first step towards directed higher observational type theory.
Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.” Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.”
The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-L\"of Type Theory to asymmetric … The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-L\"of Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model and is the first step towards directed higher observational type theory.
Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.” Abstract We give a brief overview of the special issue of MSCS “Advances in Homotopy Type Theory.”
Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of Locally Cartesian Closed Categories (LCCCs) with disjoint … Containers capture the concept of strictly positive data types in programming. The original development of containers is done in the internal language of Locally Cartesian Closed Categories (LCCCs) with disjoint coproducts and W-types. Although it is claimed that these developments can also be interpreted in extensional Martin-L\"of type theory, this interpretation is not made explicit. Moreover, as a result of extensionality, these developments freely assume Uniqueness of Identity Proofs (UIP), so it is not clear whether this is a necessary condition. In this paper, we present a formalisation of the result that `containers preserve least and greatest fixed points' in Cubical Agda, thereby giving a formulation in intensional type theory, and showing that UIP is not necessary. Our main incentive for using Cubical Agda is that its path type restores the equivalence between bisimulation and coinductive equality. Thus, besides developing container theory in a more general setting, we also demonstrate the usefulness of Cubical Agda's path type to coinductive proofs.
Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven … Parametricity is a property of the syntax of type theory implying, e.g., that there is only one function having the type of the polymorphic identity function. Parametricity is usually proven externally, and does not hold internally. Internalising it is difficult because once there is a term witnessing parametricity, it also has to be parametric itself and this results in the appearance of higher dimensional cubes. In previous theories with internal parametricity, either an explicit syntax for higher cubes is present or the theory is extended with a new sort for the interval. In this paper we present a type theory with internal parametricity which is a simple extension of Martin-L\"of type theory: there are a few new type formers, term formers and equations. Geometry is not explicit in this syntax, but emergent: the new operations and equations only refer to objects up to dimension 3. We show that this theory is modelled by presheaves over the BCH cube category. Fibrancy conditions are not needed because we use span-based rather than relational parametricity. We define a gluing model for this theory implying that external parametricity and canonicity hold. The theory can be seen as a special case of a new kind of modal type theory, and it is the simplest setting in which the computational properties of higher observational type theory can be demonstrated.
Abstract Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that … Abstract Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (HoTT), is a preferable and should be considered as an alternative.
We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory. We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory.
Abstract My goal is to give an accessible introduction to Martin’s work on the groupoid model and how it is related to the recent notion of univalence in Homotopy Type … Abstract My goal is to give an accessible introduction to Martin’s work on the groupoid model and how it is related to the recent notion of univalence in Homotopy Type Theory while sharing some memories of Martin.
We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory. We discuss why Type Theory is preferable as foundation of Mathematics compared to set theory.
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In … Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.
Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the loop space of the suspension of A + 1. Equivalently, this … Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the loop space of the suspension of A + 1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit: F(A), cons: A~F(A)~F(A), and conditions saying that every cons(a) is an auto-equivalence on F(A). Assuming that A is a set (i.e. satisfies the principle of unique identity proofs), we are interested in the question whether F(A) is a set as well, which is very much related to an open problem in the HoTT book [22, Ex. 8.2]. We show an approximation to the question, namely that the fundamental groups of F(A) are trivial, i.e. that ||F(A)||1 is a set.
Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories … Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g. a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we don't know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work.
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a … We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda.
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we … As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-L\"of type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda. Comment: 36 pages, to appear in the special issue of TLCA'13 (LMCS)
Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by … Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory - a higher inductive-inductive type - we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of … In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an one, containing a strict equality type former, and an one, which is some version of HoTT. Our type theory is inspired by Voevosky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we no not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of infinite structures which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with schematic definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a … We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda.
As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we … As the groupoid model of Hofmann and Streicher proves, identity proofs in intensional Martin-Löf type theory cannot generally be shown to be unique. Inspired by a theorem by Hedberg, we give some simple characterizations of types that do have unique identity proofs. A key ingredient in these constructions are weakly constant endofunctions on identity types. We study such endofunctions on arbitrary types and show that they always factor through a propositional type, the truncated or squashed domain. Such a factorization is impossible for weakly constant functions in general (a result by Shulman), but we present several non-trivial cases in which it can be done. Based on these results, we define a new notion of anonymous existence in type theory and compare different forms of existence carefully. In addition, we show possibly surprising consequences of the judgmental computation rule of the truncation, in particular in the context of homotopy type theory. All the results have been formalized and verified in the dependently typed programming language Agda.
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of … In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an "outer" one, containing a strict equality type former, and an "inner" one, which is some version of HoTT. Our type theory is inspired by Voevosky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we no not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of "infinite structures" which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with "schematic" definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [13]. Following up on our previous formalisation [3] … Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [13]. Following up on our previous formalisation [3] and Brunerie's notes [6], we present a new formalisation of the syntax of weak ω-groupoids in Agda using heterogeneous equality. We show how to recover basic constructions on ω-groupoids using suspension and replacement. In particular we show that any type forms a groupoid and we outline how to derive higher dimensional composition. We present a possible semantics using globular sets and discuss the issues which arise when using globular types instead.
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously developed denotational … We develop a sound and complete equational theory for the functional quantum programming language QML. The soundness and completeness of the theory are with respect to the previously developed denotational semantics of QML. The completeness proof also gives rise to a normalisation algorithm following the normalisation-by-evaluation approach. The current work focuses on the pure fragment of QML, omitting measurements.
This thesis introduces the language QML, a functional language for quantum computations on finite types.QML exhibits quantum data and control structures, and integrates reversible and irreversible quantum computations.The design of … This thesis introduces the language QML, a functional language for quantum computations on finite types.QML exhibits quantum data and control structures, and integrates reversible and irreversible quantum computations.The design of QML is guided by the categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive operational semantics of irreversible quantum computations, realisable as quantum circuits.The quantum circuit model is also given a formal categorical definition via the category FQC.QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings, which may lead to the collapse of the quantum wavefunction, explicit.Strict programs are free from measurement, and hence preserve superpositions and entanglement.A denotational semantics of QML programs is presented, which maps QML terms into superoperators, via the operational semantics, made precise by the category Q.Extensional equality for QML programs is also presented, via a mapping from FQC morphisms into the category Q. CONTENTS ix 8 Further research 8.1 Compositionality of QML 8.2 A direct denotational semantics for QML 8.3 Infinite data structures and recursion in QML 8.4 Other areas of further research 8.5 Summary 9 Summary and conclusions 9.1 List of publications References A Shor's algorithm and the Quantum Fourier Transform A.1 Efficient factoring: Shor's algorithm A.2 From period finding to factoring A.3 Probability Analysis A.4 Haskell implementation of Shor's algorithm A.5 Order-finding by phase estimation A.6 Implementing the three qubit Quantum Fourier Transform A.7 Summary x
We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and … We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and measurement. The effectful part can be modelled using a generalisation of monads called arrows. We express the resulting executable model of quantum computing in the Haskell programming language using its special syntax for arrow computations. However, the embedding in Haskell is not perfect: a faithful model of quantum computing requires type capabilities that are not directly expressible in Haskell.
We show that the model of quantum computation based on density matrices and superoperators can be decomposed in a pure classical (functional) part and an effectful part modeling probabilities and … We show that the model of quantum computation based on density matrices and superoperators can be decomposed in a pure classical (functional) part and an effectful part modeling probabilities and measurement. The effectful part can be modeled using a generalization of monads called arrows. We express the resulting executable model of quantum computing in the programming language Haskell using its special syntax for arrow computations. The embedding in Haskell is however not perfect: a faithful model of quantum computing requires type capabilities which are not directly expressible in Haskell.
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model … We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and /spl eta/-rules for /spl Pi/and /spl Sigma/-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.
This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in … This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model … We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, intensional setoid model in Intensional Type theory with a proof-irrelevant universe of propositions and /spl eta/-rules for /spl Pi/and /spl Sigma/-types. The Type Theory corresponding to this model is decidable, has no irreducible constants and permits large eliminations, which are essential for universes.
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these … Homotopy Type Theory is a new field of mathematics based on the recently-discovered correspondence between Martin-Löf's constructive type theory and abstract homotopy theory. We have a powerful interplay between these disciplines - we can use geometric intuition to formulate new concepts in type theory and, conversely, use type-theoretic machinery to verify and often simplify existing mathematical proofs.
It is shown that an intuitionistic model of set theory with the axiom of choice has to be a classical one. It is shown that an intuitionistic model of set theory with the axiom of choice has to be a classical one.
This preprint has been withdrawn. This preprint has been withdrawn.
The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the … The classical lambda calculus may be regarded both as a programming language and as a formal algebraic system for reasoning about computation. It provides a computational model equivalent to the Turing machine, and continues to be of enormous benefit in the classical theory of computation. We propose that quantum computation, like its classical counterpart, may benefit from a version of the lambda calculus suitable for expressing and reasoning about quantum algorithms. In this paper we develop a quantum lambda calculus as an alternative model of quantum computation, which combines some of the benefits of both the quantum Turing machine and the quantum circuit models. The calculus turns out to be closely related to the linear lambda calculi used in the study of Linear Logic. We set up a computational model and an equational proof system for this calculus, and we argue that it is equivalent to the quantum Turing machine.
Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional … Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In … Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.
Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe … Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe higher-dimensional paths.While some aspects of homotopy theory have been developed synthetically and formalized in proof assistants, some seemingly easy examples have proved difficult because the required manipulations of paths becomes complicated.In this paper, we describe a cubical approach to developing homotopy theory within type theory.The identity type is complemented with higher-dimensional cube types, such as a type of squares, dependent on four points and four lines, and a type of three-dimensional cubes, dependent on the boundary of a cube.Path-over-a-path types and higher generalizations are used to describe cubes in a fibration over a cube in the base.These higher-dimensional cube and path-over types can be defined from the usual identity type, but isolating them as independent conceptual abstractions has allowed for the formalization of some previously difficult examples.
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new … Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.
Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development … Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(\infty,1)$-category is presented by some model category to which our results apply.
Particular focus in this paper is on quantum information protocols, which exploit quantum-mechanical effects in an essential way. The particular examples we shall use to illustrate our approach will be … Particular focus in this paper is on quantum information protocols, which exploit quantum-mechanical effects in an essential way. The particular examples we shall use to illustrate our approach will be teleportation (Benett et al., 1993), logic-gate teleportation (Gottesman and Chuang,1999), and entanglement swapping (Zukowski et al., 1993). The ideas illustrated in these protocols form the basis for novel and potentially very important applications to secure and fault-tolerant communication and computation (2001,1999,2000).
This thesis introduces the language QML, a functional language for quantum computations on finite types.QML exhibits quantum data and control structures, and integrates reversible and irreversible quantum computations.The design of … This thesis introduces the language QML, a functional language for quantum computations on finite types.QML exhibits quantum data and control structures, and integrates reversible and irreversible quantum computations.The design of QML is guided by the categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive operational semantics of irreversible quantum computations, realisable as quantum circuits.The quantum circuit model is also given a formal categorical definition via the category FQC.QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings, which may lead to the collapse of the quantum wavefunction, explicit.Strict programs are free from measurement, and hence preserve superpositions and entanglement.A denotational semantics of QML programs is presented, which maps QML terms into superoperators, via the operational semantics, made precise by the category Q.Extensional equality for QML programs is also presented, via a mapping from FQC morphisms into the category Q. CONTENTS ix 8 Further research 8.1 Compositionality of QML 8.2 A direct denotational semantics for QML 8.3 Infinite data structures and recursion in QML 8.4 Other areas of further research 8.5 Summary 9 Summary and conclusions 9.1 List of publications References A Shor's algorithm and the Quantum Fourier Transform A.1 Efficient factoring: Shor's algorithm A.2 From period finding to factoring A.3 Probability Analysis A.4 Haskell implementation of Shor's algorithm A.5 Order-finding by phase estimation A.6 Implementing the three qubit Quantum Fourier Transform A.7 Summary x
In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently … In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently constant functions from A to B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over omega^op. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of coherently constant function is equivalent to the type ||A|| -> B. If B is an n-type for a given finite n, the tower of coherence conditions becomes finite and the requirement of nontrivial Reedy limits vanishes. The whole construction can then be carried out in standard syntactical homotopy type theory and generalises the universal property of the truncation. This provides a way to define functions ||A|| -> B if B is not known to be propositional, and it streamlines the common approach of finding a propositional type Q with A -> Q and Q -> B.
Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. The limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence … Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. The limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence of Cauchy sequences of rationals. This lifting requires the axiom of countable choice or excluded middle, neither of which is available in homotopy type theory. To address this, the Univalent Foundations Program uses a higher inductive-inductive type to define the Cauchy reals as the free Cauchy complete metric space generated by the rationals. We generalize this construction to define the free Cauchy complete metric space generated by an arbitrary metric space. This forms a monad in the category of metric spaces with Lipschitz functions. When applied to the rationals it defines the Cauchy reals. Finally, we can use Altenkirch and Danielson (2016)'s partiality monad to define a semi-decision procedure comparing a real number and a rational number. The entire construction has been formalized in the Coq proof assistant. It is available at https://github.com/SkySkimmer/HoTTClasses/tree/CPP2017 .
The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by … The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by Bishop 1967. The language of the theory is richer than the language of first order predicate logic. This makes it possible to strengthen the axioms for existence and disjunction. In the case of existence, the possibility of strengthening the usual elimination rule seems first to have been indicated by Howard 1969, whose proposed axioms are special cases of the existential elimination rule of the present theory. Furthermore, there is a reflection principle which links the generation of objects and types and plays somewhat the same role for the present theory as does the replacement axiom for Zermelo-Fraenkel set theory. An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis. Mathematical objects and their types. We shall think of mathematical objects or constructions. Every mathematical object is of a certain kind or type. Better, a mathematical object is always given together with its type, that is, it is not just an object, it is an object of a certain type.
Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as … Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corresponding to an ordinary category. This fails to capture many naturally occurring structures, stemming from the fact that the naturally occurring structures in homotopy type theory are not ordinary, but rather higher categories. Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the simplicial strategy is best suited. Work by Lurie and Harpaz motivates the following definition. Given the first ( n +3) levels of a semisimplicial type S , we can equip S with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a complete semi-Segal n -type . This is very similar to an earlier suggestion by Schreiber. The definition of a univalent (1-) category by Ahrens et al. can easily be extended or restricted to the definition of a univalent n -category (more precisely, ( n ,1)-category) for n ∈ {0,1,2}, and we show that the type of complete semi-Segal n -types is equivalent to the type of univalent n -categories in these cases. Thus, we believe that the notion of a complete semi-Segal n -type can be taken as the definition of a univalent n -category. We provide a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.
Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories … Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof of equality is encoded as a term in a context extended by the interval pretype. Our goal is to develop a cubical theory where the identity type is defined recursively over the type structure, and the geometry arises from these definitions. In this theory, cubes are present explicitly, e.g. a line is a telescope with 3 elements: two endpoints and the connecting equality. This is in line with Bernardy and Moulin's earlier work on internal parametricity. In this paper we present a naive syntax for internal parametricity and by replacing the parametric interpretation of the universe, we extend it to univalence. However, we don't know how to compute in this theory. As a second step, we present a version of the theory for parametricity with named dimensions which has an operational semantics. Extending this syntax to univalence is left as further work.
A few conventions for thinking about and writing quantum pseudocode are proposed. The conventions can be used for presenting any quantum algorithm down to the lowest level and are consistent … A few conventions for thinking about and writing quantum pseudocode are proposed. The conventions can be used for presenting any quantum algorithm down to the lowest level and are consistent with a quantum random access machine (QRAM) model for quantum computing. In principle a formal version of quantum pseudocode could be used in a future extension of a conventional language.
Abstract It is consistent with constructive set theory (without Countable Choice, clearly) that the Cauchy reals (equivalence classes of Cauchy sequences of rationals) are not Cauchy complete. Related results are … Abstract It is consistent with constructive set theory (without Countable Choice, clearly) that the Cauchy reals (equivalence classes of Cauchy sequences of rationals) are not Cauchy complete. Related results are also shown, such as that a Cauchy sequence of rationals may not have a modulus of convergence, and that a Cauchy sequence of Cauchy sequences may not converge to a Cauchy sequence, among others. (© 2007 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an … We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.
We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its … We consider the problem of defining the integers in Homotopy Type Theory (HoTT). We can define the type of integers as signed natural numbers (i.e., using a coproduct), but its induction principle is very inconvenient to work with, since it leads to an explosion of cases. An alternative is to use set-quotients, but here we need to use set-truncation to avoid non-trivial higher equalities. This results in a recursion principle that only allows us to define function into sets (types satisfying UIP). In this paper we consider higher inductive types using either a small universe or bi-invertible maps. These types represent integers without explicit set-truncation that are equivalent to the usual coproduct representation. This is an interesting example since it shows how some coherence problems can be handled in HoTT. We discuss some open questions triggered by this work. The proofs have been formally verified using cubical Agda.
In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to … In this paper we develop a functional programming language for quantum computers by extending the simply-typed lambda calculus with quantum types and operations. The design of this language adheres to the ‘quantum data, classical control’ paradigm, following the first author's work on quantum flow-charts. We define a call-by-value operational semantics, and give a type system using affine intuitionistic linear logic. The main results of this paper are the safety properties of the language and the development of a type inference algorithm.
In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of … In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an one, containing a strict equality type former, and an one, which is some version of HoTT. Our type theory is inspired by Voevosky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we no not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of infinite structures which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with schematic definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types … We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.
A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded … A fertile field of research in theoretical computer science investigates the representation of general recursive functions in intensional type theories. Among the most successful approaches are: the use of wellfounded relations, implementation of operational semantics, formalization of domain theory, and inductive definition of domain predicates. Here, a different solution is proposed: exploiting coinductive types to model infinite computations. To every type A we associate a type of partial elements Partial(A), coinductively generated by two constructors: the first, return(a) just returns an element a:A; the second, step(x), adds a computation step to a recursive element x:Partial(A). We show how this simple device is sufficient to formalize all recursive functions between two given types. It allows the definition of fixed points of finitary, that is, continuous, operators. We will compare this approach to different ones from the literature. Finally, we mention that the formalization, with appropriate structural maps, defines a strong monad.
Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by … Capretta's delay monad can be used to model partial computations, but it has the wrong notion of built-in equality, strong bisimilarity. An alternative is to quotient the delay monad by the right notion of equality, weak bisimilarity. However, recent work by Chapman et al. suggests that it is impossible to define a monad structure on the resulting construction in common forms of type theory without assuming (instances of) the axiom of countable choice. Using an idea from homotopy type theory - a higher inductive-inductive type - we construct a partiality monad without relying on countable choice. We prove that, in the presence of countable choice, our partiality monad is equivalent to the delay monad quotiented by weak bisimilarity. Furthermore we outline several applications.
We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and … We show that the model of quantum computation based on density matrices and superoperators can be decomposed into a pure classical (functional) part and an effectful part modelling probabilities and measurement. The effectful part can be modelled using a generalisation of monads called arrows. We express the resulting executable model of quantum computing in the Haskell programming language using its special syntax for arrow computations. However, the embedding in Haskell is not perfect: a faithful model of quantum computing requires type capabilities that are not directly expressible in Haskell.
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower … We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.
A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces … A higher inductive type of level 1 (a 1-hit) has constructors for points and paths only, whereas a higher inductive type of level 2 (a 2-hit) has constructors for surfaces too. We restrict attention to finitary higher inductive types and present general schemata for the types of their point, path, and surface constructors. We also derive the elimination and equality rules from the types of constructors for 1-hits and 2-hits. Moreover, we construct a groupoid model for dependent type theory with 2-hits and point out that we obtain a setoid model for dependent type theory with 1-hits by truncating the groupoid model.
An all optical implementation of quantum information processing with semiconductor macroatoms is proposed. Our quantum hardware consists of an array of quantum dots and the computational degrees of freedom are … An all optical implementation of quantum information processing with semiconductor macroatoms is proposed. Our quantum hardware consists of an array of quantum dots and the computational degrees of freedom are energy-selected interband optical transitions. The quantum-computing strategy exploits exciton-exciton interactions driven by ultrafast multicolor laser pulses. Contrary to existing proposals based on charge excitations, our approach does not require time-dependent electric fields, thus allowing for a subpicosecond, decoherence-free, operation time scale in realistic semiconductor nanostructures.
In this paper we give a summary of the comparisons between different definitions of so-called (∞, 1)-categories, which are considered to be models for ∞-categories whose n-morphisms are all invertible … In this paper we give a summary of the comparisons between different definitions of so-called (∞, 1)-categories, which are considered to be models for ∞-categories whose n-morphisms are all invertible for n > 1. They are also, from the viewpoint of homotopy theory, models for the homotopy theory of homotopy theories. The four different structures, all of which are equivalent, are simplicial categories, Segal categories, complete Segal spaces, and quasi-categories.
Measurements of the birefringence of a single atom strongly coupled to a high-finesse optical resonator are reported, with nonlinear phase shifts observed for an intracavity photon number much less than … Measurements of the birefringence of a single atom strongly coupled to a high-finesse optical resonator are reported, with nonlinear phase shifts observed for an intracavity photon number much less than one. A proposal to utilize the measured conditional phase shifts for implementing quantum logic via a quantum-phase gate (QPG) is considered. Within the context of a simple model for the field transformation, the parameters of the "truth table" for the QPG are determined.
Quantum mechanics can speed up a range of search applications over unsorted data. For example imagine a phone directory containing N names arranged in completely random order. To find someone's … Quantum mechanics can speed up a range of search applications over unsorted data. For example imagine a phone directory containing N names arranged in completely random order. To find someone's phone number with a probability of 50%, any classical algorithm (whether deterministic or probabilistic) will need to access the database a minimum of O(N) times. Quantum mechanical systems can be in a superposition of states and simultaneously examine multiple names. By properly adjusting the phases of various operations, successful computations reinforce each other while others interfere randomly. As a result, the desired phone number can be obtained in only O(sqrt(N)) accesses to the database.
In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do … In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren [2009], which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorization system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure, which we call a homotopy-theoretic model of identity types , and to prove that this is sufficient for a sound interpretation. Now, although both Top and SSet are categories endowed with a weak factorization system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting these leads us to introduce the notion of a path object category . This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet , we endow those categories with the structure of a homotopy-theoretic model and, in this way, obtain the desired topological and simplicial models of identity types.
We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations. We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.