Calculating the Fundamental Group of the Circle in Homotopy Type Theory

Authors

Daniel R. Licata, Michael Shulman

Type: Article

Publication Date: 2013-06-01

Citations: 59

DOI: https://doi.org/10.1109/lics.2013.28

Ask PDF

Abstract

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.

Locations

arXiv (Cornell University)
PDF
CiteSeer X (The Pennsylvania State University)
View PDF

Ask a Question About This Paper

Summary

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-01-15

Daniel R. Licata , Michael Shulman

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 category theory and … 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 category theory and homotopy theory suggest new principles to add to type theory, and type theory can be used in novel ways to formalize these areas of mathematics. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Though simple, this example is interesting for several reasons: it illustrates the new principles in homotopy type theory; it mixes ideas from traditional homotopy-theoretic proofs of the result with type-theoretic inductive reasoning; and it provides a context for understanding an existing puzzle in type theory---that a universe (type of types) is necessary to prove that the constructors of inductive types are disjoint and injective.

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-01-01

Daniel R. Licata , Michael Shulman

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 category theory and … 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 category theory and homotopy theory suggest new principles to add to type theory, and type theory can be used in novel ways to formalize these areas of mathematics. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Though simple, this example is interesting for several reasons: it illustrates the new principles in homotopy type theory; it mixes ideas from traditional homotopy-theoretic proofs of the result with type-theoretic inductive reasoning; and it provides a context for understanding an existing puzzle in type theory---that a universe (type of types) is necessary to prove that the constructors of inductive types are disjoint and injective.

View PDF Chat

Eilenberg-MacLane spaces in homotopy type theory

2014-07-14

Daniel R. Licata , Eric Finster

Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs … Homotopy type theory is an extension of Martin-Löf type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of Eilenberg-MacLane spaces. For an abelian group G, an Eilenberg-MacLane space K(G,n) is a space (type) whose nth homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in G. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.

View PDF Chat

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01

Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more

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.

View PDF Chat

Homotopy type theory

2015-01-28

Steve Awodey , Robert Harper

Homotopy type theory is a recently-developed unification of previously disparate frameworks, which can serve to advance the project of formalizing and mechanizing mathematics. One framework is based on a computational … Homotopy type theory is a recently-developed unification of previously disparate frameworks, which can serve to advance the project of formalizing and mechanizing mathematics. One framework is based on a computational conception of the type of a construction, the other is based on a homotopical conception of the homotopy type of a space. The computational notion of type has its origins in Brouwer's program of intuitionism, and Church's λ-calculus, both of which sought to ground mathematics in computation (one would say "algorithm" these days). The homotopical notion comes from Grothendieck's late conception of homotopy types of spaces as represented by ∞-groupoids [Grothendieck 1983]. The computational perspective was developed most fully by Per Martin-Löf, leading in particular to his Intuitionistic Theory of Types [Martin-Löf and Sambin 1984], on which the formal system of homotopy type theory is based. The connection to homotopy theory was first hinted at in the groupoid interpretation of Hofmann and Streicher [Hofmann and Streicher 1994; 1995]. It was then made explicit by several researchers, roughly simultaneously. The connection was clinched by Voevodsky's introduction of the univalence axiom , which is motivated by the homotopical interpretation, and which relates type equality to homotopy equivalence [Kapulkin et al. 2012; Awodey et al. 2013].

View PDF Chat

π n (S n ) in Homotopy Type Theory

2013-01-01

Daniel R. Licata , Guillaume Brunerie

On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths

2018-01-01

Tiago Mendonça Lucena de Veras , Arthur Ramos , Ruy J. G. B. de Queiroz +1 more

One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the … One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the equality between two terms of the same type as a collection of homotopical paths between points of the same space. Since this is only a semantical interpretation, the addition of paths to the syntax of homotopy type theory has been recently proposed by De Queiroz, Ramos and De Oliveira . In these works, the authors propose an entity known as `computational path', proposed by De Queiroz and Gabbay in 1994, and show that it can be used to formalize the identity type. We have found that it is possible to use these computational paths as a tool to achieve one central result of algebraic topology and homotopy type theory: the calculation of fundamental groups of surfaces. We review the concept of computational paths and the $LND_{EQ}-TRS$, which is a term rewriting system proposed by De Oliveira in 1994 to map redundancies between computational paths. We then proceed to calculate the fundamental group of the circle, cylinder, M{\"o}bius band, torus and the real projective plane. Moreover, we show that the use of computational paths make these calculations simple and straightforward, whereas the same result is much harder to obtain using the traditional code-encode-decode approach of homotopy type theory.

View PDF Chat

On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths.

2018-04-03

Tiago Mendonça Lucena de Veras , Arthur Ramos , Ruy J. G. B. de Queiroz +1 more

One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the … One of the most interesting entities of homotopy type theory is the identity type. It gives rise to an interesting interpretation of the equality, since one can semantically interpret the equality between two terms of the same type as a collection of homotopical paths between points of the same space. Since this is only a semantical interpretation, the addition of paths to the syntax of homotopy type theory has been recently proposed by De Queiroz, Ramos and De Oliveira . In these works, the authors propose an entity known as `computational path', proposed by De Queiroz and Gabbay in 1994, and show that it can be used to formalize the identity type. We have found that it is possible to use these computational paths as a tool to achieve one central result of algebraic topology and homotopy type theory: the calculation of fundamental groups of surfaces. We review the concept of computational paths and the $LND_{EQ}-TRS$, which is a term rewriting system proposed by De Oliveira in 1994 to map redundancies between computational paths. We then proceed to calculate the fundamental group of the circle, cylinder, M{o}bius band, torus and the real projective plane. Moreover, we show that the use of computational paths make these calculations simple and straightforward, whereas the same result is much harder to obtain using the traditional code-encode-decode approach of homotopy type theory.

Homotopy type theory

2014-01-01

Álvaro Pelayo , Michael A. Warren

We give a glimpse of an emerging field at the intersection of homotopy theory, logic, and theoretical computer science: homotopy type theory. One key ingredient of this approach is Vladimir … We give a glimpse of an emerging field at the intersection of homotopy theory, logic, and theoretical computer science: homotopy type theory. One key ingredient of this approach is Vladimir Voevodsky’s Univalence Axiom. It is the goal of this paper to provide a short introduction to some of the ideas of homotopy type theory and univalence. The approach taken here is to first develop some of the historical and mathematical context in which homotopy type theory arose and then to describe the Univalence Axiom and related technical machinery.

Introduction to Homotopy Type Theory

2022-01-01

Egbert Rijke

This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common … This is an introductory textbook to univalent mathematics and homotopy type theory, a mathematical foundation that takes advantage of the structural nature of mathematical definitions and constructions. It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal. This textbook introduces the reader to Martin-L\"of's dependent type theory, to the central concepts of univalent mathematics, and shows the reader how to do mathematics from a univalent point of view. Over 200 exercises are included to train the reader in type theoretic reasoning. The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.

The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory

2016-11-03

Kristina Sojakova

Homotopy type theory is a new branch of mathematics that merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us … Homotopy type theory is a new branch of mathematics that merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us to represent a variety of mathematical objects as basic type-theoretic construction, higher inductive types. We present a proof that in homotopy type theory, the torus is equivalent to the product of two circles. This result indicates that the synthetic definition of torus as a higher inductive type is indeed correct.

View PDF Chat

Voevodsky’s Univalence Axiom in Homotopy Type Theory

2013-09-11

Steve Awodey , Álvaro Pelayo , Michael A. Warren

In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir … In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study. The Institute for Advanced Study in Princeton is hosting a special program during the academic year 2012-2013 on a new research theme that is based on recently discovered connections between homotopy theory, a branch of algebraic topology, and type theory, a branch of mathematical logic and theoretical computer science. In this brief paper our goal is to take a glance at these developments. For those readers who would like to learn more about them, we recommend a number of references throughout. Type theory was invented by Bertrand Russell [20], but it was first developed as a rigorous formal system by Alonzo Church [3, 4, 5]. It now has numerous applications in computer science, especially in the theory of programming languages [19]. Per Martin-Lof [15, 11, 13, 14], among others, developed a generalization of Church’s system which is now usually called dependent, constructive, or simply Martin-Lof type theory; this is the system that we consider here. It was originally intended as a rigorous framework for constructive mathematics. In type theory objects are classified using a primitive notion of type, similar to the data-types used in programming languages. And as in programming languages, these elaborately structured types can be used to express detailed specifications of the objects classified, giving rise to principles of reasoning about them. To take a simple example, the objects of a product type A × B are known to be of the form 〈a, b〉, and so one automatically knows how to form them and how to decompose them. This aspect of type

View PDF Chat

The equivalence of the torus and the product of two circles in homotopy type theory

2015-01-01

Kristina Sojakova

Homotopy type theory is a new branch of mathematics which merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us … Homotopy type theory is a new branch of mathematics which merges insights from abstract homotopy theory and higher category theory with those of logic and type theory. It allows us to represent a variety of mathematical objects as basic type-theoretic constructions, higher inductive types. We present a proof that in homotopy type theory, the torus is equivalent to the product of two circles. This result indicates that the synthetic definition of torus as a higher inductive type is indeed correct.

View PDF Chat

The equivalence of the torus and the product of two circles in homotopy type theory

2015-10-13

Kristina Sojakova

Homotopy Type Theory: A Synthetic Approach to Higher Equalities

2018-01-18

Michael Shulman

Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which … Homotopy type theory and univalent foundations (HoTT/UF) is a new foundation of mathematics, based not on set theory but on “infinity-groupoids”, which consist of collections of objects, ways in which two objects can be equal, ways in which those ways-to-be-equal can be equal, ad infinitum. Though apparently complicated, such structures are increasingly important in mathematics. Philosophically, they are an inevitable result of the notion that whenever we form a collection of things, we must simultaneously consider when two of those things are the same. The “synthetic” nature of HoTT/UF enables a much simpler description of infinity groupoids than is available in set theory, thereby aligning with modern mathematics while placing “equality” back in the foundations of logic. This chapter will introduce the basic ideas of HoTT/UF for a philosophical audience, including Voevodsky’s univalence axiom and higher inductive types.

View PDF Chat

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-01-01

Nicolai Kraus , Jakob von Raumer

The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove … The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman '13), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman '16). We provide a formalization of the main technical results in the proof assistant Lean.

View PDF Chat

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-01-17

Nicolai Kraus , Jakob von Raumer

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-06-01

Nicolai Kraus , Jakob von Raumer

The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove … The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.

View PDF Chat

Formalizing π4(S3) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda

2023-06-26

Axel Ljungström , Anders Mörtberg

Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of the classical result that the fourth homotopy group of the 3-sphere is ℤ/2ℤ. The proof … Brunerie's 2016 PhD thesis contains the first synthetic proof in Homotopy Type Theory (HoTT) of the classical result that the fourth homotopy group of the 3-sphere is ℤ/2ℤ. The proof is one of the most impressive pieces of synthetic homotopy theory to date and uses a lot of advanced classical algebraic topology rephrased synthetically. Furthermore, the proof is fully constructive and the main result can be reduced to the question of whether a particular "Brunerie number" β can be normalized to ±2. The question of whether Brunerie's proof could be formalized in a proof assistant, either by computing this number or by formalizing the pen-and-paper proof, has since remained open. In this paper, we present a complete formalization in Cubical Agda. We do this by modifying Brunerie's proof so that a key technical result, whose proof Brunerie only sketched in his thesis, can be avoided. We also present a formalization of a new and much simpler proof that β is ±2. This formalization provides us with a sequence of simpler Brunerie numbers, one of which normalizes very quickly to −2 in Cubical Agda, resulting in a fully formalized computer-assisted proof that ${\pi _4}({\mathbb{S}^3}) \cong \mathbb{Z}/2\mathbb{Z}$.

View PDF Chat

An Interesting Link Between Type Theory and Algebraic topology.

2009-07-20

F. Lamarche

Henri Poincare invented both homology and homotopy theory around 1899. The spaces he used for homotopy were pieces of R^n glued together; the general concept of topological spaces had not … Henri Poincare invented both homology and homotopy theory around 1899. The spaces he used for homotopy were pieces of R^n glued together; the general concept of topological spaces had not been invented yet. He could not do the same for homology, so he resorted to simple combinatorial objects to define the necessary spaces, which he called simplicial complexes, and where computations were easy anyway. It is only in the forties that Eilenberg showed how do define homology directly on topological spaces, and in the early fifties that combinato- rial objects were found--that we now call simplicial sets, and that are also due to Eilenberg and his students--which are sufficiently powerful to enable direct definitions and quite few computations in homotopy. The most fundamental concept of homotopy is the notion of path between two points in space. For several years it has been tempting to give logical meaning to this notion of path, namely as a constructive proof that two points are equal. One way to formalize this intuitive notion would be to interpret the Martin-Lo f type-theoretical equality predicate in suitable category of spaces. The first positive results in this direction have been given by Michael Warren, working under the supervision of Steve Awodey. They are quite technical and depend very much on modern abstract homotopy theory la Quillen. I will present very concrete model, which I also think is the simplest that has been discovered so far. It is based on well-known specialization of simplicial set, for which I will define concrete path object which doubles as an identity type, along with suitable notion of dependent type.

Higher Inductive Types as Homotopy-Initial Algebras

2014-12-19

Kristina Sojakova

View PDF Chat

An introduction to univalent foundations for mathematicians

2018-03-05

Daniel R. Grayson

We offer an introduction for mathematicians to the univalent foundations of Vladimir Voevodsky, aiming to explain how he chose to encode mathematics in type theory and how the encoding reveals … We offer an introduction for mathematicians to the univalent foundations of Vladimir Voevodsky, aiming to explain how he chose to encode mathematics in type theory and how the encoding reveals a potentially viable foundation for all of modern mathematics that can serve as an alternative to set theory.

View PDF Chat

Finite sets in homotopy type theory

2018-01-08

Dan Frumin , Herman Geuvers , Léon Gondelman +1 more

We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.

View PDF Chat

The Hurewicz theorem in homotopy type theory

2023-07-25

J. Daniel Christensen , Luis Scoccola

We prove the Hurewicz theorem in homotopy type theory, i.e., that for X a pointed, (n -1)-connected type (n ≥ 1) and A an abelian group, there is a natural … We prove the Hurewicz theorem in homotopy type theory, i.e., that for X a pointed, (n -1)-connected type (n ≥ 1) and A an abelian group, there is a natural isomorphism πn(X) ab ⊗ A ∼ = Hn(X; A) relating the abelianization of the homotopy groups with the homology.We also compute the connectivity of a smash product of types and express the lowest non-trivial homotopy group as a tensor product.Along the way, we study magmas, loop spaces, connected covers and prespectra, and we use 1-coherent categories to express naturality and for the Yoneda lemma.As homotopy type theory has models in all ∞-toposes, our results can be viewed as extending known results about spaces to all other ∞-toposes.

View PDF Chat

On symmetries of spheres in univalent foundations

2024-06-21

Pierre Cagne , Ulrik Buchholtz , Nicolai Kraus +1 more

View PDF Chat

Homotopy Type Theory and the Vertical Unity of Concepts in Mathematics

2017-06-22

David Corfield

The mathematician Alexander Borovik speaks of the importance of the `vertical unity' of mathematics. By this he means to draw our attention to the fact that many sophisticated mathematical concepts, … The mathematician Alexander Borovik speaks of the importance of the `vertical unity' of mathematics. By this he means to draw our attention to the fact that many sophisticated mathematical concepts, even those introduced at the cutting-edge of research, have their roots in our most basic conceptualisations of the world. If this is so, we might expect any truly fundamental mathematical language to detect such structural commonalities. It is reasonable to suppose then that the lack of philosophical interest in such vertical unity is related to the prominence given by philosophers to languages which do not express well such relations. In this chapter, I suggest that we look beyond set theory to the newly emerging homotopy type theory, which makes plain what there is in common between very simple aspects of logic, arithmetic and geometry and much more sophisticated concepts. With this language in mind, new light is thrown on thenature of mathematical concepts with clear benefits for educationalists.

Impredicative Encodings of (Higher) Inductive Types

2018-06-27

Steve Awodey , Jonas Frey , Sam Speight

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit … Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant η-equalities and consequently do not admit dependent eliminators. To recover η and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

View PDF Chat

The univalence axiom for elegant Reedy presheaves

2013-07-23

Michael Shulman

We show that Voevodsky's univalence axiom for intensional type theory is valid in categories of simplicial presheaves on elegant Reedy categories. In addition to diagrams on inverse categories, as considered … We show that Voevodsky's univalence axiom for intensional type theory is valid in categories of simplicial presheaves on elegant Reedy categories. In addition to diagrams on inverse categories, as considered in previous work of the author, this includes bisimplicial sets and $\Theta_n$-spaces. This has potential applications to the study of homotopical models for higher categories.

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01

Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more

View PDF Chat

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-06-01

Nicolai Kraus , Jakob von Raumer

The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove … The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.

View PDF Chat

Eilenberg-MacLane spaces in homotopy type theory

2014-07-14

Daniel R. Licata , Eric Finster

View PDF Chat

Quotient Inductive-Inductive Types

2018-01-01

Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more

View PDF Chat

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

2016-07-05

Kuen-Bang Hou , Eric Finster , Daniel R. Licata +1 more

This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result … This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.

View PDF Chat

Formalizing π4(S3) ≅Z/2Z and Computing a Brunerie Number in Cubical Agda

2023-06-26

Axel Ljungström , Anders Mörtberg

View PDF Chat

The Seifert-van Kampen Theorem in Homotopy Type Theory

2016-08-01

Kuen-Bang Hou , Michael Shulman

Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic … Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic theorems, yielding homotopy theory. Here we consider the Seifert-van Kampen theorem, which characterizes the loop structure of spaces obtained by gluing. This is useful in homotopy theory because many spaces are constructed by gluing, and the loop structure helps distinguish distinct spaces. The synthetic proof showcases many new characteristics of synthetic homotopy theory, such as the encode-decode method, enforced homotopy-invariance, and lack of underlying sets.

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-01-17

Nicolai Kraus , Jakob von Raumer

A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory

2016-01-01

Kuen-Bang Hou , Eric Finster , Daniel R. Licata +1 more

This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the … This paper continues investigations in "synthetic homotopy theory": the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory We present a mechanized proof of the Blakers-Massey connectivity theorem, a result relating the higher-dimensional homotopy groups of a pushout type (roughly, a space constructed by gluing two spaces along a shared subspace) to those of the components of the pushout. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which has been studied in previous formalizations. The new proof is more elementary than existing ones in abstract homotopy-theoretic settings, and the mechanization is concise and high-level, thanks to novel combinations of ideas from homotopy theory and type theory.

View PDF Chat

Homotopy type theory

2015-01-28

Steve Awodey , Robert Harper

View PDF Chat

Constructing Higher Inductive Types as Groupoid Quotients

2021-04-22

Niccolò Veltri , Niels van der Weide

In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. … In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

View PDF Chat

The univalence axiom for elegant Reedy presheaves

2015-01-01

Michael Shulman

We show that Voevodsky's univalence axiom for homotopy type theory is valid in categories of simplicial presheaves on elegant Reedy categories.In addition to diagrams on inverse categories, as considered in … We show that Voevodsky's univalence axiom for homotopy type theory is valid in categories of simplicial presheaves on elegant Reedy categories.In addition to diagrams on inverse categories, as considered in previous work of the author, this includes bisimplicial sets and Θ n -spaces.This has potential applications to the study of homotopical models for higher categories.

View PDF Chat

Free Higher Groups in Homotopy Type Theory

2018-06-27

Nicolai Kraus , Thorsten Altenkirch

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.

View PDF Chat

The Equivalence of the Torus and the Product of Two Circles in Homotopy Type Theory

2016-11-03

Kristina Sojakova

View PDF Chat

A proposition is the (homotopy) type of its proofs

2017-01-08

Steve Awodey

Higher Inductive Types as Homotopy-Initial Algebras

2015-01-14

Kristina Sojakova

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. Higher inductive types form a crucial part of this new system since they allow us to represent mathematical objects, such as spheres, tori, pushouts, and quotients, in the type theory. We investigate a class of higher inductive types called W-suspensions which generalize Martin-Löf's well-founded trees. We show that a propositional variant of W-suspensions, whose computational behavior is determined up to a higher path, is characterized by the universal property of being a homotopy-initial algebra. As a corollary we get that W-suspensions in the strict form are homotopy-initial.

View PDF Chat

Homotopy type theory

2014-01-01

Álvaro Pelayo , Michael A. Warren

Adjoint Logic with a 2-Category of Modes

2015-12-09

Daniel R. Licata , Michael Shulman

π n (S n ) in Homotopy Type Theory

2013-01-01

Daniel R. Licata , Guillaume Brunerie

Cubical synthetic homotopy theory

2020-01-20

Anders Mörtberg , Loïc Pujet

Homotopy type theory is an extension of type theory that enables synthetic reasoning about spaces and homotopy theory. This has led to elegant computer formalizations of multiple classical results from … Homotopy type theory is an extension of type theory that enables synthetic reasoning about spaces and homotopy theory. This has led to elegant computer formalizations of multiple classical results from homotopy theory. However, many proofs are still surprisingly complicated to formalize. One reason for this is the axiomatic treatment of univalence and higher inductive types which complicates synthetic reasoning as many intermediate steps, that could hold simply by computation, require explicit arguments. Cubical type theory offers a solution to this in the form of a new type theory with native support for both univalence and higher inductive types. In this paper we show how the recent cubical extension of Agda can be used to formalize some of the major results of homotopy type theory in a direct and elegant manner.

View PDF Chat

A Cubical Approach to Synthetic Homotopy Theory

2015-07-01

Daniel R. Licata , Guillaume Brunerie

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.

View PDF Chat

Finite sets in homotopy type theory

2017-12-22

Dan Frumin , Herman Geuvers , Léon Gondelman +1 more

View PDF Chat

Impredicative Encodings of (Higher) Inductive Types

2018-01-01

Steve Awodey , Jonas Frey , Sam Speight

Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit … Postulating an impredicative universe in dependent type theory allows System F style encodings of finitary inductive types, but these fail to satisfy the relevant {\eta}-equalities and consequently do not admit dependent eliminators. To recover {\eta} and dependent elimination, we present a method to construct refinements of these impredicative encodings, using ideas from homotopy type theory. We then extend our method to construct impredicative encodings of some higher inductive types, such as 1-truncation and the unit circle S1.

View PDF Chat

Partial Univalence in n-truncated Type Theory

2020-05-01

Christian Sattler , Andrea Vezzosi

It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms … It is well known that univalence is incompatible with uniqueness of identity proofs (UIP), the axiom that all types are h-sets. This is due to finite h-sets having non-trivial automorphisms as soon as they are not h-propositions. A natural question is then whether univalence restricted to h-propositions is compatible with UIP. We answer this affirmatively by constructing a model where types are elements of a closed universe defined as a higher inductive type in homotopy type theory. This universe has a path constructor for simultaneous partial univalent completion, i.e., restricted to h-propositions. More generally, we show that univalence restricted to $(n-1)$-types is consistent with the assumption that all types are $n$-truncated. Moreover we parametrize our construction by a suitably well-behaved container, to abstract from a concrete choice of type formers for the universe.

Univalence for inverse EI diagrams

2017-01-01

Michael Shulman

We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 1)-categories", which contains universe objects that satisfy Voevodsky's univalence axiom.In addition to diagrams on … We construct a new model category presenting the homotopy theory of presheaves on "inverse EI (∞, 1)-categories", which contains universe objects that satisfy Voevodsky's univalence axiom.In addition to diagrams on ordinary inverse categories, as considered in previous work of the author, this includes a new model for equivariant algebraic topology with a compact Lie group of equivariance.Thus, it offers the potential for applications of homotopy type theory to equivariant homotopy theory.

View PDF Chat

The equivalence of the torus and the product of two circles in homotopy type theory

2015-10-13

Kristina Sojakova

On the homotopy groups of spheres in homotopy type theory

2016-06-15

Guillaume Brunerie

The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the … The goal of this thesis is to prove that π4(S3) ≃ Z/2Z in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form πk(Sn) with k < n, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number n such that π4(S3) ≃ Z/nZ. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the n to either 1 or 2. The Hopf invariant also allows us to prove that all the groups of the form π4n−1(S2n) are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of CP2 and to prove that π4(S3) ≃ Z/2Z and that more generally πn+1(Sn) ≃ Z/2Z for every n ≥ 3

Higher Inductive Types as Homotopy-Initial Algebras

2014-02-04

Kristina Sojakova

Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs constructive type theory and abstract homotopy theory. We have a powerful interplay … Homotopy Type Theory is a new field of mathematics based on the surprising and elegant correspondence between Martin-Lofs 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. A crucial ingredient in this new system are higher inductive types, which allow us to represent objects such as spheres, tori, pushouts, and quotients. We investigate a variant of higher inductive types whose computational behavior is determined up to a higher path. We show that in this setting, higher inductive types are characterized by the universal property of being a homotopy-initial algebra.

Connecting Constructive Notions of Ordinals in Homotopy Type Theory

2021-01-01

Nicolai Kraus , Fredrik Nordvall Forsberg , Chuangjie Xu

In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We … In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.

View PDF Chat

Homotopy Type Theory: A Synthetic Approach to Higher Equalities

2018-01-18

Michael Shulman

View PDF Chat

All $(\infty,1)$-toposes have strict univalent universes

2019-04-15

Michael Shulman

We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can … We prove the conjecture that any Grothendieck $(\infty,1)$-topos can be presented by a Quillen model category that interprets homotopy type theory with strict univalent universes. Thus, homotopy type theory can be used as a formal language for reasoning internally to $(\infty,1)$-toposes, just as higher-order logic is used for 1-toposes. As part of the proof, we give a new, more explicit, characterization of the fibrations in injective model structures on presheaf categories. In particular, we show that they generalize the coflexible algebras of 2-monad theory.

On the homotopy groups of spheres in homotopy type theory

2016-01-01

Guillaume Brunerie

The goal of this thesis is to prove that $\pi_4(S^3) \simeq \mathbb{Z}/2\mathbb{Z}$ in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the … The goal of this thesis is to prove that $\pi_4(S^3) \simeq \mathbb{Z}/2\mathbb{Z}$ in homotopy type theory. In particular it is a constructive and purely homotopy-theoretic proof. We first recall the basic concepts of homotopy type theory, and we prove some well-known results about the homotopy groups of spheres: the computation of the homotopy groups of the circle, the triviality of those of the form $\pi_k(S^n)$ with $k < n$, and the construction of the Hopf fibration. We then move to more advanced tools. In particular, we define the James construction which allows us to prove the Freudenthal suspension theorem and the fact that there exists a natural number $n$ such that $\pi_4(S^3) \simeq \mathbb{Z}/n\mathbb{Z}$. Then we study the smash product of spheres, we construct the cohomology ring of a space, and we introduce the Hopf invariant, allowing us to narrow down the $n$ to either $1$ or $2$. The Hopf invariant also allows us to prove that all the groups of the form $\pi_{4n-1}(S^{2n})$ are infinite. Finally we construct the Gysin exact sequence, allowing us to compute the cohomology of $\mathbb{C}P^2$ and to prove that $\pi_4(S^3) \simeq \mathbb{Z}/2\mathbb{Z}$ and that more generally $\pi_{n+1}(S^n) \simeq \mathbb{Z}/2\mathbb{Z}$ for every $n \ge 3$.

View PDF Chat

Univalent Foundations of Mathematics

2011-01-01

Vladimir Voevodsky

View PDF Chat

Weak ω-Categories from Intensional Type Theory

2009-01-01

Peter LeFanu Lumsdaine

Homotopy Theoretic Aspects of Constructive Type Theory

2008-01-01

Michael A. Warren

THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

2014-01-01

Krzysztof Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky

In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique … In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan bration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals.

The identity type weak factorisation system

2008-09-03

Nicola Gambino , Richard Garner

View PDF Chat

Two-dimensional models of type theory

2009-07-02

Richard Garner

We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories. We describe a non-extensional variant of Martin-L\"of type theory which we call two-dimensional type theory, and equip it with a sound and complete semantics valued in 2-categories.

View PDF Chat

Types are weak ω -groupoids

2010-10-12

Benno van den Berg , Richard Garner

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.

View PDF Chat

Homotopy theoretic models of identity types

2008-07-14

Steve Awodey , Michael A. Warren

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.

View PDF Chat