Constructing the propositional truncation using non-recursive HITs

Authors

Floris van Doorn

Type: Article

Publication Date: 2016-01-12

Citations: 28

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

Ask PDF

Abstract

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.

Locations

arXiv (Cornell University)
View PDF

Ask a Question About This Paper

Summary

Constructing the Propositional Truncation using Non-recursive HITs

2015-01-01

Floris van Doorn

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive … In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.

Chat View PDF

Constructing the Propositional Truncation using Non-recursive HITs

2015-12-07

Floris van Doorn

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive … In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.

Chat View PDF

Constructions with Non-Recursive Higher Inductive Types

2016-07-05

Nicolai Kraus

Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to … Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs.

Chat View PDF

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.

Chat View PDF

Higher inductive types in Homotopy Type Theory: applications and theory

2016-04-01

Fredrik Nordvall Forsberg

Construction of the Circle in UniMath

2019-01-01

Marc Bezem , Ulrik Buchholtz , Daniel R. Grayson +1 more

We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence … We show that the type $\mathrm{T}\mathbb{Z}$ of $\mathbb{Z}$-torsors has the dependent universal property of the circle, which characterizes it up to a unique homotopy equivalence. The construction uses Voevodsky's Univalence Axiom and propositional truncation, yielding a stand-alone construction of the circle not using higher inductive types.

Chat View PDF

Construction of the Circle in UniMath

2019-10-04

Marc Bezem , Ulrik Buchholtz , Daniel R. Grayson +1 more

Chat View PDF

The General Universal Property of the Propositional Truncation

2014-01-01

Nicolai Kraus

In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, Sigma, Pi, and identity types), we define the type of constant … In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least 1, Sigma, Pi, and identity types), we define the type of constant functions from A to B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over omega. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of constant function is equivalent to the type ||A|| -> B. If B is an n-type for a given finite n, the tower of coherence conditions becomes finite and the requirement of nontrivial Reedy limits vanishes. The whole construction can then be carried out in Homotopy Type Theory and generalises the universal property of the truncation. This provides a way to define functions ||A|| -> B if B is not known to be propositional, and it streamlines the common approach of finding a proposition Q with A -> Q and Q -> B.

Chat View PDF

The General Universal Property of the Propositional Truncation

2014-11-11

Nicolai Kraus

The HoTT Library: A formalization of homotopy type theory in Coq

2016-10-14

Andrej Bauer , Jason Gross , Peter LeFanu Lumsdaine +3 more

We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, … We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.

Chat View PDF

The HoTT Library: A formalization of homotopy type theory in Coq

2016-01-01

Andrej Bauer , Jason N. Gross , Peter LeFanu Lumsdaine +3 more

Chat View PDF

The HoTT library: a formalization of homotopy type theory in Coq

2016-12-22

Andrej Bauer , Jason Gross , Peter LeFanu Lumsdaine +3 more

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.

Functions out of Higher Truncations

2015-07-04

Paolo Capriotti , Nicolai Kraus , Andrea Vezzosi

In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of … In homotopy type theory, the truncation operator ||-||n (for a number n greater or equal to -1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B that are constant on all (n+1)-st loop spaces. We give one elementary proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct set-based representations of 1-types, as long as they have braided loop spaces. The main result with one of its proofs and the application have been formalised in Agda.

homotopy.io: a proof assistant for finitely-presented globular $n$-categories

2024-02-20

Nathan Corbyn , Lukas Heidemann , Nick Hu +3 more

We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via … We present the proof assistant homotopy.io for working with finitely-presented semistrict higher categories. The tool runs in the browser with a point-and-click interface, allowing direct manipulation of proof objects via a graphical representation. We describe the user interface and explain how the tool can be used in practice. We also describe the essential subsystems of the tool, including collapse, contraction, expansion, typechecking, and layout, as well as key implementation details including data structure encoding, memoisation, and rendering. These technical innovations have been essential for achieving good performance in a resource-constrained setting.

Chat View PDF

The General Universal Property of the Propositional Truncation

2015-01-01

Nicolai Kraus

In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently … In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently constant functions from A to B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over omega^op. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of coherently constant function is equivalent to the type ||A|| -> B. If B is an n-type for a given finite n, the tower of coherence conditions becomes finite and the requirement of nontrivial Reedy limits vanishes. The whole construction can then be carried out in standard syntactical homotopy type theory and generalises the universal property of the truncation. This provides a way to define functions ||A|| -> B if B is not known to be propositional, and it streamlines the common approach of finding a propositional type Q with A -> Q and Q -> B.

The General Universal Property of the Propositional Truncation

2014-11-01

Nicolai Kraus

Functions out of Higher Truncations

2015-07-04

Paolo Capriotti , Nicolai Kraus , Andrea Vezzosi

In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and … In homotopy type theory, the truncation operator ||-||n (for a number n > -2) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into n-types, which makes it hard to construct functions ||A||n -> B if B is not an n-type. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)-type, then functions ||A||n -> B correspond exactly to functions A -> B which are constant on all (n+1)-st loop spaces. We give one elementary proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct set-based representations of 1-types, as long as they have braided loop spaces. The main result with one of its proofs and the application have been formalised in Agda.

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.

Generating Higher Identity Proofs in Homotopy Type Theory

2024-12-02

Thibaut Benjamin

Finster and Mimram have defined a dependent type theory called CaTT, which describes the structure of omega-categories. Types in homotopy type theory with their higher identity types form weak omega-groupoids, … Finster and Mimram have defined a dependent type theory called CaTT, which describes the structure of omega-categories. Types in homotopy type theory with their higher identity types form weak omega-groupoids, so they are in particular weak omega-categories. In this article, we show that this principle makes homotopy type theory into a model of CaTT, by defining a translation principle that interprets an operation on the cell of an omega-category as an operation on higher identity types. We then illustrate how this translation allows to leverage several mechanisation principles that are available in CaTT, to reduce the proof effort required to derive results about the structure of identity types, such as the existence of an Eckmann-Hilton cell.

Chat View PDF

Cellular Cohomology in Homotopy Type Theory

2018-01-01

Ulrik Buchholtz , Kuen-Bang Hou

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

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

Higher Structures in Homotopy Type Theory

2019-01-01

Ulrik Buchholtz

Chat View PDF

Computational Higher Type Theory IV: Inductive Types

2018-01-01

Evan Cavallo , Robert Harper

This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type … This is the fourth in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to higher-dimensional types. In this installment, we show how to define cubical type systems supporting a general schema of indexed cubical inductive types whose constructors may take dimension parameters and have a specified boundary. Using this schema, we are able to specify and implement many of the higher inductive types which have been postulated in homotopy type theory, including homotopy pushouts, the torus, $W$-quotients, truncations, arbitrary localizations. By including indexed inductive types, we enable the definition of identity types. The addition of higher inductive types makes computational higher type theory a model of homotopy type theory, capable of interpreting almost all of the constructions in the HoTT Book (with the exception of inductive-inductive types). This is the first such model with an explicit canonicity theorem, which specifies the canonical values of higher inductive types and confirms that every term in an inductive type evaluates to such a value.

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

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

Quotient Inductive-Inductive Types

2018-01-01

Thorsten Altenkirch , Paolo Capriotti , Gabe Dijkstra +2 more

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

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

Constructions with Non-Recursive Higher Inductive Types

2016-07-05

Nicolai Kraus

Chat View PDF

Semantics of higher inductive types

2019-06-17

Peter LeFanu Lumsdaine , Michael Shulman

Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development … Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the "synthetic" development of homotopy theory within type theory, as well as in formalizing ordinary set-level mathematics in type theory. In this article, we construct models of a wide range of higher inductive types in a fairly wide range of settings. We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has *weakly stable typal initial algebras* for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specializes to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction, and general localisations. Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed $(\infty,1)$-category is presented by some model category to which our results apply.

Chat View PDF

The real projective spaces in homotopy type theory

2017-06-01

Ulrik Buchholtz , Egbert Rijke

Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about … Homotopy type theory is a version of Martin-Löf type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of ℝP n , as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define ℝP n by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take ℝP -1 to be the empty type. In the inductive step, we take ℝP n+1 to be the mapping cone of the projection map of the tautological bundle of ℝP n , and we use its universal property and the univalence axiom to define the tautological bundle on ℝP n+1 . By showing that the total space of the tautological bundle of ℝP n is the n-sphere S n , we retrieve the classical description of ℝP n+1 as ℝP n with an (n + 1)-disk attached to it. The infinite dimensional real projective space ℝP ∞ , defined as the sequential colimit of ℝP n with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(ℤ/2ℤ, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles. These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.

Chat View PDF

Cellular Cohomology in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Kuen-Bang Hou Favonia

Chat View PDF

Finite sets in homotopy type theory

2017-12-22

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

Chat View PDF

Sequential Colimits in Homotopy Type Theory

2020-05-25

Kristina Sojakova , Floris van Doorn , Egbert Rijke

Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute … Sequential colimits are an important class of higher inductive types. We present a self-contained and fully formalized proof of the conjecture that in homotopy type theory sequential colimits appropriately commute with Σ-types. This result allows us to give short proofs of a number of useful corollaries, some of which were conjectured in other works: the commutativity of sequential colimits with identity types, with homotopy fibers, loop spaces, and truncations, and the preservation of the properties of truncatedness and connectedness under sequential colimits. Our entire development carries over to (∞, 1)-toposes using Shulman's recent interpretation of homotopy type theory into these structures.

Higher Lenses

2021-06-29

Paolo Capriotti , Nils Anders Danielsson , Andrea Vezzosi

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

The join construction

2017-01-26

Egbert Rijke

In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map … In homotopy type theory we can define the join of maps as a binary operation on maps with a common co-domain. This operation is commutative, associative, and the unique map from the empty type into the common codomain is a neutral element. Moreover, we show that the idempotents of the join of maps are precisely the embeddings, and we prove the `join connectivity theorem', which states that the connectivity of the join of maps equals the join of the connectivities of the individual maps. We define the image of a map $f:A\to X$ in $U$ via the join construction, as the colimit of the finite join powers of $f$. The join powers therefore provide approximations of the image inclusion, and the join connectivity theorem implies that the approximating maps into the image increase in connectivity. A modified version of the join construction can be used to show that for any map $f:A\to X$ in which $X$ is only assumed to be locally small, the image is a small type. We use the modified join construction to give an alternative construction of set-quotients, the Rezk completion of a precategory, and we define the $n$-truncation for any $n:\mathbb{N}$. Thus we see that each of these are definable operations on a univalent universe for Martin-Lof type theory with a natural numbers object, that is moreover closed under homotopy coequalizers.

Chat View PDF

Higher inductive types in cubical computational type theory

2019-01-02

Evan Cavallo , Robert Harper

Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory … Homotopy type theory proposes higher inductive types (HITs) as a means of defining and reasoning about inductively-generated objects with higher-dimensional structure. As with the univalence axiom, however, homotopy type theory does not specify the computational behavior of HITs. Computational interpretations have now been provided for univalence and specific HITs by way of cubical type theories, which use a judgmental infrastructure of dimension variables. We extend the cartesian cubical computational type theory introduced by Angiuli et al. with a schema for indexed cubical inductive types (CITs), an adaptation of higher inductive types to the cubical setting. In doing so, we isolate the canonical values of a cubical inductive type and prove a canonicity theorem with respect to these values.

Chat View PDF

On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory.

2018-08-31

Floris van Doorn

The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction … The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant.

Chat View PDF

The real projective spaces in homotopy type theory

2017-06-20

Ulrik Buchholtz , Egbert Rijke

Homotopy type theory is a version of Martin-Lof type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about … Homotopy type theory is a version of Martin-Lof type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we construct the real projective spaces, key players in homotopy theory, as certain higher inductive types in homotopy type theory. The classical definition of RPn, as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define RPn by induction on n simultaneously with its tautological bundle of 2-element sets. As the base case, we take RP-1 to be the empty type. In the inductive step, we take RPn+1 to be the mapping cone of the projection map of the tautological bundle of RPn, and we use its universal property and the univalence axiom to define the tautological bundle on RPn+1.By showing that the total space of the tautological bundle of RPn is the n-sphere Sn, we retrieve the classical description of RPn+1 as RPn with an (n + 1)-disk attached to it. The infinite dimensional real projective space RP∞, defined as the sequential colimit of RPn with the canonical inclusion maps, is equivalent to the Eilenberg-MacLane space K(Z/2Z, 1), which here arises as the subtype of the universe consisting of 2-element types. Indeed, the infinite dimensional projective space classifies the 0-sphere bundles, which one can think of as synthetic line bundles.These constructions in homotopy type theory further illustrate the utility of homotopy type theory, including the interplay of type theoretic and homotopy theoretic ideas.

On Higher Inductive Types in Cubical Type Theory

2018-06-27

Thierry Coquand , Simon Huber , Anders Mörtberg

Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly … Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.

Chat View PDF

Signatures and Induction Principles for Higher Inductive-Inductive Types

2019-01-01

Ambrus Kaposi , András Kovács

Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed … Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.

Chat View PDF

Homotopy Type Theory in Lean

2017-01-01

Floris van Doorn , Jakob von Raumer , Ulrik Buchholtz

Chat View PDF

Constructing Higher Inductive Types as Groupoid Quotients

2020-05-26

Niels van der Weide

In this paper, we show that all finitary 1-truncated higher inductive types (HITs) can be constructed from the groupoid quotient. We start by defining internally a notion of signatures for … In this paper, we show that all finitary 1-truncated higher inductive types (HITs) can be constructed from the groupoid quotient. We start by defining internally a 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. We finish by constructing a biinitial object in the bicategory of algebras in groupoids. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

Chat View PDF

Elaboration in Dependent Type Theory

2015-05-16

Leonardo Mendonça de Moura , Jeremy Avigad , Soonho Kong +1 more

To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit … To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean's elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved.

Chat View PDF

Classifying Types.

2019-06-22

Egbert Rijke

The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many … The study of homotopy theoretic phenomena in the language of type theory is sometimes loosely called `synthetic homotopy theory'. Homotopy theory in type theory is only one of the many aspects of homotopy type theory, which also includes the study of the set theoretic semantics (models of homotopy type theory and univalence in a meta-theory of sets or categories), type theoretic semantics (internal models of homotopy type theory), and computational semantics, as well as the study of various questions in the internal language of homotopy type theory which are not necessarily motivated by homotopy theory, or questions related to the development of formalized libraries of mathematics based on homotopy type theory. This thesis concerns the development of synthetic homotopy theory.

Chat View PDF

Higher Inductive Types as Homotopy-Initial Algebras

2014-12-19

Kristina Sojakova

Chat View PDF

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.

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

The General Universal Property of the Propositional Truncation

2015-01-01

Nicolai Kraus