Eilenberg-MacLane spaces in homotopy type theory

Authors

Daniel R. Licata, Eric Finster

Type: Article

Publication Date: 2014-07-14

Citations: 56

DOI: https://doi.org/10.1145/2603088.2603153

Ask PDF

Abstract

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.

Locations

CiteSeer X (The Pennsylvania State University)
View PDF

Ask a Question About This Paper

Summary

Eilenberg-MacLane spaces and stabilisation in homotopy type theory

2023-01-01

David Wärn

In this note, we study the delooping of spaces and maps in homotopy type theory. We show that in some cases, spaces have a unique delooping, and give a simple … In this note, we study the delooping of spaces and maps in homotopy type theory. We show that in some cases, spaces have a unique delooping, and give a simple description of the delooping in these cases. We explain why some maps, such as group homomorphisms, have a unique delooping. We discuss some applications to Eilenberg-MacLane spaces and cohomology.

Chat View PDF

Eilenberg–Maclane spaces and stabilisation in homotopy type theory

2023-09-01

David Wärn

Abstract In this note, we study the delooping of spaces and maps in homotopy type theory. We show that in some cases, spaces have a unique delooping, and give a … Abstract In this note, we study the delooping of spaces and maps in homotopy type theory. We show that in some cases, spaces have a unique delooping, and give a simple description of the delooping in these cases. We explain why some maps, such as group homomorphisms, have a unique delooping. We discuss some applications to Eilenberg–MacLane spaces and cohomology.

Chat View PDF

Cellular Cohomology in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Kuen-Bang Hou Favonia

We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage … We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.

Chat View PDF

Cellular Cohomology in Homotopy Type Theory

2018-01-01

Ulrik Buchholtz , Kuen-Bang Hou

Chat View PDF

Cellular Cohomology in Homotopy Type Theory

2020-06-01

Ulrik Buchholtz , Kuen-Bang Hou

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.

Homotopy Type Theory: The Logic of Space

2021-03-22

Michael Shulman

This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces … This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book New Spaces for Mathematics and Physics (ed. Gabriel Catren and Mathieu Anel).

Chat View PDF

Homotopy type theory: the logic of space

2017-01-01

Michael Shulman

This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book "New Spaces … This is an introduction to type theory, synthetic topology, and homotopy type theory from a category-theoretic and topological point of view, written as a chapter for the book "New Spaces for Mathematics and Physics" (ed. Gabriel Catren and Mathieu Anel).

Chat View PDF

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.

Chat View PDF

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-01-01

Daniel R. Licata , Michael Shulman

Chat View PDF

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-06-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 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.

Chat View PDF

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].

Chat View PDF

Cubical Homotopy Theory

2015-10-05

Brian A. Munson , Ismar Volić

Graduate students and researchers alike will benefit from this treatment of classical and modern topics in homotopy theory of topological spaces with an emphasis on cubical diagrams. The book contains … Graduate students and researchers alike will benefit from this treatment of classical and modern topics in homotopy theory of topological spaces with an emphasis on cubical diagrams. The book contains 300 examples and provides detailed explanations of many fundamental results. Part I focuses on foundational material on homotopy theory, viewed through the lens of cubical diagrams: fibrations and cofibrations, homotopy pullbacks and pushouts, and the Blakers–Massey Theorem. Part II includes a brief example-driven introduction to categories, limits and colimits, an accessible account of homotopy limits and colimits of diagrams of spaces, and a treatment of cosimplicial spaces. The book finishes with applications to some exciting new topics that use cubical diagrams: an overview of two versions of calculus of functors and an account of recent developments in the study of the topology of spaces of knots.

Homotopy Theory and Fundamental Groups in Topological Spaces: Theoretical Foundations and Applications

2024-12-31

Hanwen Zhao

This paper explores homotopy groups, a central topic in algebraic topology, and provides a detailed examination of their foundational role in understanding the structure of topological spaces. Beginning with the … This paper explores homotopy groups, a central topic in algebraic topology, and provides a detailed examination of their foundational role in understanding the structure of topological spaces. Beginning with the definitions and operations of homotopy groups, the discussion progresses to the construction of a chain complex and a rigorous proof of its exactness. The paper delves into the application of homotopy theory to fibrations, deriving an exact sequence that elucidates the intricate relationship between loop spaces and the fundamental group in simply connected spaces. This relationship underscores how fundamental groups can be interpreted through the lens of homotopy, particularly in the context of loop spaces. The theoretical results are further applied to algebraic varieties and schemes, highlighting the broader implications of homotopy theory in areas such as algebraic geometry. By investigating how homotopy groups influence the topological structure of algebraic varieties and their associated schemes, the paper demonstrates the significant utility of homotopy theory in connecting abstract topological concepts with concrete algebraic structures. The challenges of working with exact sequences, particularly in the complex landscape of higher homotopy groups, are also addressed, underscoring the mathematical sophistication required to navigate these topics. This exploration provides valuable insights into the role of homotopy theory in modern mathematical analysis, emphasizing its deep and far-reaching impact across various fields.

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.

Chat View PDF

Higher Inductive Types as Homotopy-Initial Algebras

2014-01-01

Kristina Sojakova

Chat View PDF

Higher inductive types in Homotopy Type Theory: applications and theory

2016-04-01

Fredrik Nordvall Forsberg

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.

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.

Chat View PDF

Bimonoidal Categories, $E_n$-Monoidal Categories, and Algebraic $K$-Theory

2021-07-22

Niles Johnson , Donald Yau

Bimonoidal categories are categorical analogues of rings without additive inverses. They have been actively studied in category theory, homotopy theory, and algebraic $K$-theory since around 1970. There is an abundance … Bimonoidal categories are categorical analogues of rings without additive inverses. They have been actively studied in category theory, homotopy theory, and algebraic $K$-theory since around 1970. There is an abundance of new applications and questions of bimonoidal categories in mathematics and other sciences. This work provides a unified treatment of bimonoidal and higher ring-like categories, their connection with algebraic $K$-theory and homotopy theory, and applications to quantum groups and topological quantum computation. With ample background material, extensive coverage, detailed presentation of both well-known and new theorems, and a list of open questions, this work is a user friendly resource for beginners and experts alike.

Chat View PDF

Non-accessible localizations

2021-01-01

J. Daniel Christensen

In a 2005 paper, Casacuberta, Scevenels and Smith construct a homotopy idempotent functor $E$ on the category of simplicial sets with the property that whether it can be expressed as … In a 2005 paper, Casacuberta, Scevenels and Smith construct a homotopy idempotent functor $E$ on the category of simplicial sets with the property that whether it can be expressed as localization with respect to a map $f$ is independent of the ZFC axioms. We show that this construction can be carried out in homotopy type theory. More precisely, we give a general method of associating to a suitable (possibly large) family of maps, a reflective subuniverse of any universe $\mathcal{U}$. When specialized to an appropriate family, this produces a localization which when interpreted in the $\infty$-topos of spaces agrees with the localization corresponding to $E$. Our approach generalizes the approach of [CSS] in two ways. First, by working in homotopy type theory, our construction can be interpreted in any $\infty$-topos. Second, while the local objects produced by [CSS] are always 1-types, our construction can produce $n$-types, for any $n$. This is new, even in the $\infty$-topos of spaces. In addition, by making use of universes, our proof is very direct. Along the way, we prove many results about "small" types that are of independent interest. As an application, we give a new proof that separated localizations exist. We also give results that say when a localization with respect to a family of maps can be presented as localization with respect to a single map, and show that the simplicial model satisfies a strong form of the axiom of choice which implies that sets cover and that the law of excluded middle holds.

Chat View PDF

Non‐accessible localizations

2024-05-23

J. Daniel Christensen

Abstract In a 2005 paper, Casacuberta, Scevenels, and Smith construct a homotopy idempotent functor on the category of simplicial sets with the property that whether it can be expressed as … Abstract In a 2005 paper, Casacuberta, Scevenels, and Smith construct a homotopy idempotent functor on the category of simplicial sets with the property that whether it can be expressed as localization with respect to a map is independent of the ZFC axioms. We show that this construction can be carried out in homotopy type theory. More precisely, we give a general method of associating to a suitable (possibly large) family of maps, a reflective subuniverse of any universe . When specialized to an appropriate family, this produces a localization which when interpreted in the ‐topos of spaces agrees with the localization corresponding to . Our approach generalizes the approach of Casacuberta et al. (Adv. Math. 197 (2005), no. 1, 120–139) in two ways. First, by working in homotopy type theory, our construction can be interpreted in any ‐topos. Second, while the local objects produced by Casacuberta et al. are always 1‐types, our construction can produce ‐types, for any . This is new, even in the ‐topos of spaces. In addition, by making use of universes, our proof is very direct. Along the way, we prove many results about “small” types that are of independent interest. As an application, we give a new proof that separated localizations exist. We also give results that say when a localization with respect to a family of maps can be presented as localization with respect to a single map, and show that the simplicial model satisfies a strong form of the axiom of choice that implies that sets cover and that the law of excluded middle holds.

Chat View PDF

The Structuralist Mathematical Style: Bourbaki as a Case Study

2012-02-24

Jean‐Pierre Marquis

Chat View PDF

Localization in Homotopy Type Theory

2020-02-11

Egbert Rijke , J. Daniel Christensen , Luis Scoccola +1 more

We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected type $X$, the natural … We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected type $X$, the natural map $X \to X_{(p)}$ induces algebraic localizations on all homotopy groups. In order to prove this, we further develop the theory of reflective subuniverses. In particular, we show that for any reflective subuniverse $L$, the subuniverse of $L$-separated types is again a reflective subuniverse, which we call $L'$. Furthermore, we prove results establishing that $L'$ is almost left exact. We next focus on localization with respect to a map, giving results on preservation of coproducts and connectivity. We also study how such localizations interact with other reflective subuniverses and orthogonal factorization systems. As key steps towards proving the main theorem, we show that localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space $K(G,n)$ with $G$ abelian. We also include a partial converse to the main theorem.

Chat View PDF

Synthetic G-jet-structures in modal homotopy type theory

2024-12-04

Felix Cherubini

Abstract This article constructs the moduli stack of torsion-free $G$ -jet-structures in homotopy type theory with one monadic modality. This yields a construction of this moduli stack for any $\infty$ … Abstract This article constructs the moduli stack of torsion-free $G$ -jet-structures in homotopy type theory with one monadic modality. This yields a construction of this moduli stack for any $\infty$ -topos equipped with any stable factorization systems. In the intended applications of this theory, the factorization systems are given by the deRham-Stack construction. Homotopy type theory allows a formulation of this abstract theory with surprisingly low complexity. This is witnessed by the accompanying formalization of large parts of this work.

Chat View PDF

Modal descent

2020-10-26

Felix Cherubini , Egbert Rijke

Abstract Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second … Abstract Any modality in homotopy type theory gives rise to an orthogonal factorization system of which the left class is stable under pullbacks. We show that there is a second orthogonal factorization system associated with any modality, of which the left class is the class of ○-equivalences and the right class is the class of ○-étale maps. This factorization system is called the modal reflective factorization system of a modality, and we give a precise characterization of the orthogonal factorization systems that arise as the modal reflective factorization system of a modality. In the special case of the n -truncation, the modal reflective factorization system has a simple description: we show that the n -étale maps are the maps that are right orthogonal to the map $${\rm{1}} \to {\rm{ }}{{\rm{S}}^{n + 1}}$$ . We use the ○-étale maps to prove a modal descent theorem: a map with modal fibers into ○ X is the same thing as a ○-étale map into a type X . We conclude with an application to real-cohesive homotopy type theory and remark how ○-étale maps relate to the formally etale maps from algebraic geometry.

Chat View PDF

A foundation for synthetic algebraic geometry

2024-12-04

Felix Cherubini , Thierry Coquand , Matthias Hutzler

Abstract This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (Kock (2006) [I.12], Blechschmidt (2017)). The Zariski topos … Abstract This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (Kock (2006) [I.12], Blechschmidt (2017)). The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, that is, generating covers are given by localization maps for finitely many elements $f_1,\dots, f_n$ that generate the ideal $(1)=A\subseteq A$ . We use homotopy-type theory together with three axioms as the internal language of a (higher) Zariski topos. One of our main contributions is the use of higher types – in the homotopical sense – to define and reason about cohomology. Actually computing cohomology groups seems to need a principle along the lines of our “Zariski local choice” axiom, which we justify as well as the other axioms using a cubical model of homotopy-type theory.

Chat View PDF

Homotopy Type Theory: The Logic of Space

2021-03-22

Michael Shulman

Chat View PDF

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.

Chat View PDF

The long exact sequence of homotopy <i>n</i>-groups

2023-09-01

Ulrik Buchholtz , Egbert Rijke

Abstract Working in homotopy type theory, we introduce the notion of n -exactness for a short sequence $F\to E\to B$ of pointed types and show that any fiber sequence $F\hookrightarrow … Abstract Working in homotopy type theory, we introduce the notion of n -exactness for a short sequence $F\to E\to B$ of pointed types and show that any fiber sequence $F\hookrightarrow E \twoheadrightarrow B$ of arbitrary types induces a short sequence that is n -exact at $\| E\|_{n-1}$ . We explain how the indexing makes sense when interpreted in terms of n -groups, and we compare our definition to the existing definitions of an exact sequence of n -groups for $n=1,2$ . As the main application, we obtain the long n -exact sequence of homotopy n -groups of a fiber sequence.

Higher Structures in Homotopy Type Theory

2019-01-01

Ulrik Buchholtz

Chat View PDF

On the Nielsen-Schreier Theorem in Homotopy Type Theory

2022-01-20

Andrew Swan

We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show … We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show the special case of finite index subgroups holds constructively and the full theorem follows from the axiom of choice. We give an example of a boolean infinity topos where our formulation of the theorem does not hold and show a stronger "untruncated" version of the theorem is provably false in homotopy type theory.

Chat View PDF

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.

Chat View PDF

Delooping cyclic groups with lens spaces in homotopy type theory

2024-06-21

Samuel Mimram , Émile Oleon

Chat View PDF

On symmetries of spheres in univalent foundations

2024-06-21

Pierre Cagne , Ulrik Buchholtz , Nicolai Kraus +1 more

Chat View PDF

Nilpotent types and fracture squares in homotopy type theory

2020-05-01

Luis Scoccola

Abstract We develop the basic theory of nilpotent types and their localizations away from sets of numbers in Homotopy Type Theory. For this, general results about the classifying spaces of … Abstract We develop the basic theory of nilpotent types and their localizations away from sets of numbers in Homotopy Type Theory. For this, general results about the classifying spaces of fibrations with fiber an Eilenberg–Mac Lane space are proven. We also construct fracture squares for localizations away from sets of numbers. All of our proofs are constructive.

Chat View PDF

Brouwer's fixed-point theorem in real-cohesive homotopy type theory

2017-08-17

Michael Shulman

We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental … We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental ∞-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.

Chat View PDF

Higher Groups in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Floris van Doorn , Egbert Rijke

We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, … We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an n-type can be delooped n + 2 times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.

Chat View PDF

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.

Chat View PDF

Topological Quantum Gates in Homotopy Type Theory

2024-07-01

David Jaz Myers , Hisham Sati , Urs Schreiber

A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory

2021-12-27

Eric Finster , Samuel Mimram , Maxime Lucas +1 more

Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a … Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.

Chat View PDF

Quotient Inductive-Inductive Types

2018-01-01

Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more

Chat View PDF

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

Chat View PDF

Eilenberg–Maclane spaces and stabilisation in homotopy type theory

2023-09-01

David Wärn

Chat View PDF

Path Spaces of Higher Inductive Types in Homotopy Type Theory

2019-01-17

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.

Chat View PDF

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.

Chat View PDF

Homotopy type theory

2015-01-28

Steve Awodey , Robert Harper

Chat View PDF

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.

Chat View PDF

Modalities in homotopy type theory

2017-01-01

Egbert Rijke , Michael Shulman , Bas Spitters

Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal … Univalent homotopy type theory (HoTT) may be seen as a language for the category of $\infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of factorization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a "localization" higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.

Chat View PDF

Idempotents in intensional type theory

2017-04-27

Michael Shulman

We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's … We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.

Chat View PDF

Synthetic Homology in Homotopy Type Theory

2017-06-05

R. L. Graham

This paper defines homology in homotopy type theory, in the process stable homotopy groups are also defined. Previous research in synthetic homotopy theory is relied on, in particular the definition … This paper defines homology in homotopy type theory, in the process stable homotopy groups are also defined. Previous research in synthetic homotopy theory is relied on, in particular the definition of cohomology. This work lays the foundation for a computer checked construction of homology.

Chat View PDF

Computing Cohomology Rings in Cubical Agda

2023-01-11

Thomas Lamiaux , Axel Ljungström , Anders Mörtberg

In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. … In Homotopy Type Theory, cohomology theories are studied synthetically using higher inductive types and univalence. This paper extends previous developments by providing the first fully mechanized definition of cohomology rings. These rings may be defined as direct sums of cohomology groups together with a multiplication induced by the cup product, and can in many cases be characterized as quotients of multivariate polynomial rings. To this end, we introduce appropriate definitions of direct sums and graded rings, which we then use to define both cohomology rings and multivariate polynomial rings. Using this, we compute the cohomology rings of some classical spaces, such as the spheres and the Klein bottle. The formalization is constructive so that it can be used to do concrete computations, and it relies on the Cubical Agda system which natively supports higher inductive types and computational univalence.

Chat View PDF

Adjoint Logic with a 2-Category of Modes

2015-12-09

Daniel R. Licata , Michael Shulman

Univalence for inverse EI diagrams

2015-08-10

Michael Shulman

We construct a new model category presenting the homotopy theory of presheaves on EI $(\infty,1)$-categories, which contains universe objects that satisfy Voevodsky's univalence axiom. In addition to diagrams on ordinary … We construct a new model category presenting the homotopy theory of presheaves on EI $(\infty,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.

Chat View PDF

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.

Chat View PDF

Truncation levels in homotopy type theory

2015-07-15

Nicolai Kraus

Homotopy type theory (HoTT) is a branch of mathematics that combines and benefits from a variety of fields, most importantly homotopy theory, higher dimensional category theory, and, of course, type … Homotopy type theory (HoTT) is a branch of mathematics that combines and benefits from a variety of fields, most importantly homotopy theory, higher dimensional category theory, and, of course, type theory. We present several original results in homotopy type theory which are related to the truncation level of types, a concept due to Voevodsky. To begin, we give a few simple criteria for determining whether a type is 0-truncated (a set), inspired by a well-known theorem by Hedberg, and these criteria are then generalised to arbitrary n. This naturally leads to a discussion of functions that are weakly constant, i.e. map any two inputs to equal outputs. A weakly constant function does in general not factor through the propositional truncation of its domain, something that one could expect if the function really did not depend on its input. However, the factorisation is always possible for weakly constant endofunctions, which makes it possible to define a propositional notion of anonymous existence. We additionally find a few other non-trivial special cases in which the factorisation works. Further, we present a couple of constructions which are only possible with the judgmental computation rule for the truncation. Among these is an invertibility puzzle that seemingly inverts the canonical map from Nat to the truncation of Nat, which is perhaps surprising as the latter type is equivalent to the unit type. A further result is the construction of strict n-types in Martin-Lof type theory with a hierarchy of univalent universes (and without higher inductive types), and a proof that the universe U(n) is not n-truncated. This solves a hitherto open problem of the 2012/13 special year program on Univalent Foundations at the Institute for Advanced Study (Princeton). The main result of this thesis is a generalised universal property of the propositional truncation, using a construction of coherently constant functions. We show that the type of such coherently constant functions between types A and B, which can be seen as the type of natural transformations between two diagrams over the simplex category without degeneracies (i.e. finite non-empty sets and strictly increasing functions), is equivalent to the type of functions with the truncation of A as domain and B as codomain. In the general case, the definition of natural transformations between such diagrams requires an infinite tower of conditions, which exists if the type theory has Reedy limits of diagrams over the ordinal omega. If B is an n-type for some given finite n, (non-trivial) Reedy limits are unnecessary, allowing us to construct functions from the truncation of A to B in homotopy type theory without further assumptions. To obtain these results, we develop some theory on equality diagrams, especially equality semi-simplicial types. In particular, we show that the semi-simplicial equality type over any type satisfies the Kan condition, which can be seen as the simplicial version of the fundamental result by Lumsdaine, and by van den Berg and Garner, that types are weak omega-groupoids. Finally, we present some results related to formalisations of infinite structures that seem to be impossible to express internally. To give an example, we show how the simplex category can be implemented so that the categorical laws hold strictly. In the presence of very dependent types, we speculate that this makes the Reedy approach for the famous open problem of defining semi-simplicial types work.

Higher Lenses

2021-06-29

Paolo Capriotti , Nils Anders Danielsson , Andrea Vezzosi

We show that total, very well-behaved lenses are not very well-behaved when treated proof-relevantly in the setting of homotopy type theory/univalent foundations. In their place we propose something more well-behaved: … We show that total, very well-behaved lenses are not very well-behaved when treated proof-relevantly in the setting of homotopy type theory/univalent foundations. In their place we propose something more well-behaved: higher lenses. Such a lens contains an equivalence between the lens's source type and the product of its view type and a remainder type, plus a function from the remainder type to the propositional truncation of the view type. It can equivalently be formulated as a getter function and a proof that its family of fibres is coherently constant, i.e. factors through propositional truncation.We explore the properties of higher lenses. For instance, we prove that higher lenses are equivalent to traditional ones for types that satisfy the principle of uniqueness of identity proofs. We also prove that higher lenses are n-truncated for n-truncated types, using a coinductive characterisation of coherently constant functions.

On the Nielsen-Schreier Theorem in Homotopy Type Theory.

2020-10-02

Andrew Swan

We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show … We give a formulation of the Nielsen-Schreier theorem (subgroups of free groups are free) in homotopy type theory using the presentation of groups as pointed connected 1-truncated types. We show the special case of finite index subgroups holds constructively and the full theorem follows from the axiom of choice. We give an example of a boolean infinity topos where our formulation of the theorem does not hold and show a stronger untruncated version of the theorem is provably false in homotopy type theory.

Chat View PDF

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.

Chat View PDF

Brouwer's fixed-point theorem in real-cohesive homotopy type theory

2015-09-25

Michael Shulman

We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental … We combine Homotopy Type Theory with axiomatic cohesion, expressing the latter internally with a version of adjoint logic in which the discretization and codiscretization modalities are characterized using a judgmental formalism of crisp variables. This yields type theories that we call spatial and cohesive, in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the fundamental $\infty$-groupoid or shape), disentangling the identifications of Homotopy Type Theory from the paths of topology. In a further refinement called real-cohesion, the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.

Chat View PDF

Univalent Foundations of Mathematics

2011-01-01

Vladimir Voevodsky

Chat View PDF

Weak ω-Categories from Intensional Type Theory

2009-01-01

Peter LeFanu Lumsdaine

A generalization of the Takeuti–Gandy interpretation

2015-02-20

Bruno Barras , Thierry Coquand , Simon Huber

We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar … We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Löf type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.

Chat View PDF

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-06-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 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.

Chat View PDF

Homotopy Theoretic Aspects of Constructive Type Theory

2008-01-01

Michael A. Warren

A model of type theory in cubical sets

2014-01-01

M Bezem , Thierry Coquand , Simon Huber

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.

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.

Chat View PDF

Stable homotopy and generalised homology

1974-01-01

J. F. Adams

Preface Pt. I: S.P. Novikov's Work on Operations on Complex Cobordism 2: Cobordism groups 3: Homology 4: The Conner-Floyd Chern classes 5: The Novikov operations 6: The algebra of all … Preface Pt. I: S.P. Novikov's Work on Operations on Complex Cobordism 2: Cobordism groups 3: Homology 4: The Conner-Floyd Chern classes 5: The Novikov operations 6: The algebra of all operations 7: Scholium on Novikov's exposition 8: Complex manifolds Pt. II: Quillen's Work on Formal Groups and Complex Cobordism 1: Formal groups 2: Examples from algebraic topology 3: Reformulation 4: Calculations in E-homology and cohomology 5: Lazard's universal ring 6: More calculations in E-homology 7: The structure of Lazard's universal ring L 8: Quillen's theorem 9: Corollaries 10: Various formulae in [pi][subscript *](MU) 11: MU[subscript *](MU) 12: Behaviour of the Bott map 13: K[subscript *](K) 14: The Hattori-Stong theorem 15: Quillen's idempotent cohomology operations 16: The Brown-Peterson spectrum 17: KO[subscript *](KO) Pt. III: Stable Homotopy and Generalised Homology 2: Spectra 3: Elementary properties of the category of CW-spectra 4: Smash products 5: Spanier-Whitehead duality 6: Homology and cohomology 7: The Atiyah-Hirzebruch spectral sequence 8: The inverse limit and its derived functors 9: Products 10: Duality in manifolds 11: Applications in K-theory 12: The Steenrod algebra and its dual 13: A universal coefficient theorem 14: A category of fractions 15: The Adams spectral sequence 16: Applications to [pi][subscript *](bu[actual symbol not reproducible]X): modules over K[x, y] 17: Structure of [pi][subscript *](bu[actual symbol not reproducible]bu)~

The identity type weak factorisation system

2008-09-03

Nicola Gambino , Richard Garner

Chat View PDF

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.

Chat View PDF

Types are weak <i>ω</i> -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.

Chat View PDF

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.

Chat View PDF

Univalence for inverse diagrams and homotopy canonicity

2014-11-24

Michael Shulman

We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory … We describe a homotopical version of the relational and gluing models of type theory, and generalize it to inverse diagrams and oplax limits. Our method uses the Reedy homotopy theory on inverse diagrams, and relies on the fact that Reedy fibrant diagrams correspond to contexts of a certain shape in type theory. This has two main applications. First, by considering inverse diagrams in Voevodsky's univalent model in simplicial sets, we obtain new models of univalence in a number of (∞, 1)-toposes; this answers a question raised at the Oberwolfach workshop on homotopical type theory. Second, by gluing the syntactic category of univalent type theory along its global sections functor to groupoids, we obtain a partial answer to Voevodsky's homotopy-canonicity conjecture: in 1-truncated type theory with one univalent universe of sets, any closed term of natural number type is homotopic to a numeral.

Chat View PDF

π n (S n ) in Homotopy Type Theory

2013-01-01

Daniel R. Licata , Guillaume Brunerie