Ulrik Buchholtz

Search for another author

Author Description

Ask a Question About This Mathematician

All published works (37)

Central H-spaces and banded types

2025-04-01

Ulrik Buchholtz , J. Daniel Christensen , Jarl G. Taxerås Flaten +1 more

EPIMORPHISMS AND ACYCLIC TYPES IN UNIVALENT FOUNDATIONS

2025-02-06

Ulrik Buchholtz , Tom de Jong , Egbert Rijke

Abstract We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic … Abstract We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory as developed in univalent foundations. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with 0-connected, pointed 1-types. Many of our results are formalized as part of the agda-unimath library.

The Yoneda embedding in simplicial type theory

2025-01-22

Daniel Gratzer , Jonathan Weinberger , Ulrik Buchholtz

Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category theory. … Riehl and Shulman introduced simplicial type theory (STT), a variant of homotopy type theory which aimed to study not just homotopy theory, but its fusion with category theory: $(\infty,1)$-category theory. While notoriously technical, manipulating $\infty$-categories in simplicial type theory is often easier than working with ordinary categories, with the type theory handling infinite stacks of coherences in the background. We capitalize on recent work by Gratzer et al. defining the $(\infty,1)$-category of $\infty$-groupoids in STT to define presheaf categories within STT and systematically develop their theory. In particular, we construct the Yoneda embedding, prove the universal property of presheaf categories, refine the theory of adjunctions in STT, introduce the theory of Kan extensions, and prove Quillen's Theorem A. In addition to a large amount of category theory in STT, we offer substantial evidence that STT can be used to produce difficult results in $\infty$-category theory at a fraction of the complexity.

Chat View PDF

Directed univalence in simplicial homotopy type theory

2024-07-12

Daniel Gratzer , Jonathan Weinberger , Ulrik Buchholtz

Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics … Simplicial type theory extends homotopy type theory with a directed path type which internalizes the notion of a homomorphism within a type. This concept has significant applications both within mathematics -- where it allows for synthetic (higher) category theory -- and programming languages -- where it leads to a directed version of the structure identity principle. In this work, we construct the first types in simplicial type theory with non-trivial homomorphisms. We extend simplicial type theory with modalities and new reasoning principles to obtain triangulated type theory in order to construct the universe of discrete types $\mathcal{S}$. We prove that homomorphisms in this type correspond to ordinary functions of types i.e., that $\mathcal{S}$ is directed univalent. The construction of $\mathcal{S}$ is foundational for both of the aforementioned applications of simplicial type theory. We are able to define several crucial examples of categories and to recover important results from category theory. Using $\mathcal{S}$, we are also able to define various types whose usage is guaranteed to be functorial. These provide the first complete examples of the proposed directed structure identity principle.

Chat View PDF

On symmetries of spheres in univalent foundations

2024-06-21

Pierre Cagne , Ulrik Buchholtz , Nicolai Kraus +1 more

Chat View PDF

Primitive Recursive Dependent Type Theory

2024-06-21

Ulrik Buchholtz , Johannes Schipp von Branitz

Chat View PDF

Primitive Recursive Dependent Type Theory

2024-04-01

Ulrik Buchholtz , Johannes Schipp von Branitz

We show that restricting the elimination principle of the natural numbers type in Martin-L\"of Type Theory (MLTT) to a universe of types not containing $\Pi$-types ensures that all definable functions … We show that restricting the elimination principle of the natural numbers type in Martin-L\"of Type Theory (MLTT) to a universe of types not containing $\Pi$-types ensures that all definable functions are primitive recursive. This extends the concept of primitive recursiveness to general types. We discuss extensions to univalent type theories and other notions of computability. We are inspired by earlier work by Martin Hofmann, work on Joyal's arithmetic universes, and Hugo Herbelin and Ludovic Patey's sketched Calculus of Primitive Recursive Constructions. We define a theory Tpr that is a subtheory of MLTT with two universes, such that all inductive types are finitary and the lowest universe is restricted to not contain $\Pi$-types. We prove soundness such that all functions $\mathbb{N}\to\mathbb{N}$ are primitive recursive. The proof requires that Tpr satisfies canonicity, which we easily prove using synthetic Tait computability.

Chat View PDF

On symmetries of spheres in univalent foundations

2024-01-26

Pierre Cagne , Ulrik Buchholtz , Nicolai Kraus +1 more

Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form $\mathbb{S}^n = \mathbb{S}^n$. The case of the circle has a slick answer: the symmetries … Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form $\mathbb{S}^n = \mathbb{S}^n$. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has $\mathbb{Z}/2\mathbb{Z}$ as fundamental group. For the latter result, we develop an EHP long exact sequence.

Chat View PDF

Epimorphisms and Acyclic Types in Univalent Mathematics

2024-01-01

Ulrik Buchholtz , Tom de Jong , Egbert Rijke

We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy … We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.

Chat View PDF

The long exact sequence of homotopy n-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.

Central H-spaces and banded types

2023-01-01

Ulrik Buchholtz , J. Daniel Christensen , Jarl G. Taxerås Flaten +1 more

We introduce and study central types, which are generalizations of Eilenberg-Mac Lane spaces. A type is central when it is equivalent to the component of the identity among its own … We introduce and study central types, which are generalizations of Eilenberg-Mac Lane spaces. A type is central when it is equivalent to the component of the identity among its own self-equivalences. From centrality alone we construct an infinite delooping in terms of a tensor product of banded types, which are the appropriate notion of torsor for a central type. Our constructions are carried out in homotopy type theory, and therefore hold in any $\infty$-topos. Even when interpreted into the $\infty$-topos of spaces, our main results and constructions are new. Along the way, we further develop the theory of H-spaces in homotopy type theory, including their relation to evaluation fibrations and Whitehead products. These considerations let us, for example, rule out the existence of H-space structures on the $2n$-sphere for $n > 0$. We also give a novel description of the moduli space of H-space structures on an H-space. Using this description, we generalize a formula of Arkowitz-Curjel and Copeland for counting the number of path components of this moduli space. As an application, we deduce that the moduli space of H-space structures on the $3$-sphere is $\Omega^6 \mathbb{S}^3$.

Chat View PDF

Synthetic fibered $(\infty,1)$-category theory

2021-05-04

Ulrik Buchholtz , Jonathan Weinberger

We study cocartesian fibrations in the setting of the synthetic $(\infty,1)$-category theory developed in the simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma … We study cocartesian fibrations in the setting of the synthetic $(\infty,1)$-category theory developed in the simplicial type theory introduced by Riehl and Shulman. Our development culminates in a Yoneda Lemma for cocartesian fibrations.

Chat View PDF

Construction of the circle in UniMath

2021-01-13

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

We show that the type TZ of 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 TZ of 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

Synthetic fibered $(\infty,1)$-category theory

2021-01-01

Ulrik Buchholtz , Jonathan Weinberger

Chat View PDF

Cellular Cohomology in Homotopy Type Theory

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

Construction of the Circle in UniMath

2019-10-04

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

Higher Structures in Homotopy Type Theory

2019-01-01

Ulrik Buchholtz

Chat View PDF

Construction of the Circle in UniMath

2019-01-01

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

Chat View PDF

The long exact sequence of homotopy $n$-groups

2019-01-01

Ulrik Buchholtz , Egbert Rijke

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 … 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 $\|F\|_{n-1} \to \|E\|_{n-1} \to \|B\|_{n-1}$ 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.

Chat View PDF

The Cayley-Dickson Construction in Homotopy Type Theory

2018-11-08

Egbert Rijke , Ulrik Buchholtz

We define in the setting of homotopy type theory an H-space structure on $\mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $\mathbb S^3\hookrightarrow\mathbb S^7\twoheadrightarrow\mathbb S^4$, using … We define in the setting of homotopy type theory an H-space structure on $\mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $\mathbb S^3\hookrightarrow\mathbb S^7\twoheadrightarrow\mathbb S^4$, using only homotopy invariant tools.

Chat View PDF

Syntactic forcing models for coherent logic

2018-06-28

Marc Bezem , Ulrik Buchholtz , Thierry Coquand

Chat View PDF

Cellular Cohomology in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Kuen-Bang Hou Favonia

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

Higher Groups in Homotopy Type Theory

2018-02-12

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-Lof 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

Cellular Cohomology in Homotopy Type Theory

2018-01-01

Ulrik Buchholtz , Kuen-Bang Hou

Chat View PDF

Higher Structures in Homotopy Type Theory

2018-01-01

Ulrik Buchholtz

The intended model of the homotopy type theories used in Univalent Foundations is the infinity-category of homotopy types, also known as infinity-groupoids. The problem of higher structures is that of … The intended model of the homotopy type theories used in Univalent Foundations is the infinity-category of homotopy types, also known as infinity-groupoids. The problem of higher structures is that of constructing the homotopy types needed for mathematics, especially those that aren't sets. The current repertoire of constructions, including the usual type formers and higher inductive types, suffice for many but not all of these. We discuss the problematic cases, typically those involving an infinite hierarchy of coherence data such as semi-simplicial types, as well as the problem of developing the meta-theory of homotopy type theories in Univalent Foundations. We also discuss some proposed solutions.

Chat View PDF

Higher Groups in Homotopy Type Theory

2018-01-01

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\"of 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

Syntactic Forcing Models for Coherent Logic

2017-12-20

Marc Bezem , Ulrik Buchholtz , Thierry Coquand

We present three syntactic forcing models for coherent logic. These are based on sites whose underlying category only depends on the signature of the coherent theory, and they do not … We present three syntactic forcing models for coherent logic. These are based on sites whose underlying category only depends on the signature of the coherent theory, and they do not presuppose that the logic has equality. As an application we give a coherent theory T and a sentence {\psi} which is T-redundant (for any geometric implication {\phi}, possibly with equality, if T + {\psi} proves {\phi}, then T proves {\phi}), yet false in the generic model of T. This answers in the negative a question by Wraith.

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.

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

Varieties of Cubical Sets

2017-01-27

Ulrik Buchholtz , Edward Morehouse

We define a variety of notions of cubical sets, based on sites organized using substructural algebraic theories presenting PRO(P)s or Lawvere theories. We prove that all our sites are test … We define a variety of notions of cubical sets, based on sites organized using substructural algebraic theories presenting PRO(P)s or Lawvere theories. We prove that all our sites are test categories in the sense of Grothendieck, meaning that the corresponding presheaf categories of cubical sets model classical homotopy theory. We delineate exactly which ones are even strict test categories, meaning that products of cubical sets correspond to products of homotopy types.

Chat View PDF

Varieties of Cubical Sets

2017-01-01

Ulrik Buchholtz , Edward Morehouse

Homotopy Type Theory in Lean

2017-01-01

Floris van Doorn , Jakob von Raumer , Ulrik Buchholtz

Chat View PDF

Varieties of Cubical Sets

2017-01-01

Ulrik Buchholtz , Edward Morehouse

Chat View PDF

The real projective spaces in homotopy type theory

2017-01-01

Ulrik Buchholtz , Egbert Rijke

Homotopy type theory is a version of Martin-L\"of 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\"of 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 RP(n), as the quotient space identifying antipodal points of the n-sphere, does not translate directly to homotopy type theory. Instead, we define RP(n) 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 RP(n+1) to be the mapping cone of the projection map of the tautological bundle of RP(n), and we use its universal property and the univalence axiom to define the tautological bundle on RP(n+1). By showing that the total space of the tautological bundle of RP(n) is the n-sphere, we retrieve the classical description of RP(n+1) as RP(n) with an (n+1)-cell attached to it. The infinite dimensional real projective space, defined as the sequential colimit of the RP(n) 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.

Chat View PDF

Syntactic Forcing Models for Coherent Logic

2017-01-01

Marc Bezem , Ulrik Buchholtz , Thierry Coquand

Chat View PDF

The Cayley-Dickson Construction in Homotopy Type Theory

2016-01-01

Ulrik Buchholtz , Egbert Rijke

Chat View PDF

Common Coauthors

Coauthor	Papers Together
Egbert Rijke	14
Marc Bezem	8
Floris van Doorn	4
Thierry Coquand	3
Jonathan Weinberger	3
Edward Morehouse	3
Michael Shulman	3
Daniel R. Grayson	3
Kuen-Bang Hou	2
Nicolai Kraus	2
Tom de Jong	2
Johannes Schipp von Branitz	2
Jarl G. Taxerås Flaten	2
Pierre Cagne	2
J. Daniel Christensen	2
Daniel Gratzer	2
Kuen-Bang Hou Favonia	1
Jonathan Weinberger	1
Jakob von Raumer	1

Commonly Cited References

Cubical Type Theory: a constructive interpretation of the univalence axiom

2015-05-18

Cyril Cohen , Thierry Coquand , Simon Huber +1 more

This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in … This paper presents a type theory in which it is possible to directly manipulate n-dimensional cubes (points, lines, squares, cubes, etc.) based on an interpretation of dependent type theory in a cubical set model. This enables new ways to reason about identity types, for instance, function extensionality is directly provable in the system. Further, Voevodsky's univalence axiom is provable in this system. We also explain an extension with some higher inductive types like the circle and propositional truncation. Finally we provide semantics for this cubical type theory in a constructive meta-theory.

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

Constructing the propositional truncation using non-recursive HITs

2016-01-12

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

The real projective spaces in homotopy type theory

2017-06-01

Ulrik Buchholtz , Egbert Rijke

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

Higher Groups in Homotopy Type Theory

2018-06-27

Ulrik Buchholtz , Floris van Doorn , Egbert Rijke

Chat View PDF

Eilenberg-MacLane spaces in homotopy type theory

2014-07-14

Daniel R. Licata , Eric Finster

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

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 Cayley-Dickson Construction in Homotopy Type Theory

2018-11-08

Egbert Rijke , Ulrik Buchholtz

Chat View PDF

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 (after Voevodsky)

2021-03-08

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky’s construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky’s construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, 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 Martin-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

Chat View PDF

Homotopy Type Theory in Lean

2017-01-01

Floris van Doorn , Jakob von Raumer , Ulrik Buchholtz

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

The univalence axiom for elegant Reedy presheaves

2015-01-01

Michael Shulman

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

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

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

Sheaves in Geometry and Logic

1994-01-01

Saunders Mac Lane , Ieke Moerdijk

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

Exact completions and small sheaves

2012-01-01

Michael Shulman

We prove a general theorem which includes most notions of "exact completion". The theorem is that "k-ary exact categories" are a reflective sub-2-category of "k-ary sites", for any regular cardinal … We prove a general theorem which includes most notions of "exact completion". The theorem is that "k-ary exact categories" are a reflective sub-2-category of "k-ary sites", for any regular cardinal k. A k-ary exact category is an exact category with disjoint and universal k-small coproducts, and a k-ary site is a site whose covering sieves are generated by k-small families and which satisfies a weak size condition. For different values of k, this includes the exact completions of a regular category or a category with (weak) finite limits; the pretopos completion of a coherent category; and the category of sheaves on a small site. For a large site with k the size of the universe, it gives a well-behaved "category of small sheaves". Along the way, we define a slightly generalized notion of "morphism of sites", and show that k-ary sites are equivalent to a type of "enhanced allegory".

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

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-01-01

Chris Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, 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 Martin-L\"of type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

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

Higher algebraic K-theory: I

1973-01-01

Daniel Quillen

Modalities in homotopy type theory

2017-06-22

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.

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

2015-01-01

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 "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

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 Structures in Homotopy Type Theory

2019-01-01

Ulrik Buchholtz

Chat View PDF

π n (S n ) in Homotopy Type Theory

2013-01-01

Daniel R. Licata , Guillaume Brunerie

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

Two-Level Type Theory and Applications.

2017-05-09

Danil Annenkov , Paolo Capriotti , Nicolai Kraus

We define and develop two-level type theory (2LTT), a version of Martin-Lof type theory which combines two different type theories. We refer to them as the inner and the outer … We define and develop two-level type theory (2LTT), a version of Martin-Lof type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory. There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level $n$ can be constructed in HoTT for any externally fixed natural number $n$. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where $n$ will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models. Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky's Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be stated simply be asking the inner and outer natural numbers to be isomorphic. After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of (infinity,1)-category and give some examples.

Chat View PDF

Quasi-categories and Kan complexes

2002-11-01

André Joyal

Computational Higher Type Theory III: Univalent Universes and Exact Equality

2017-01-01

Carlo Angiuli , Kuen-Bang Hou , Robert Harper

This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend … This is the third in a series of papers extending Martin-Löf's meaning explanations of dependent type theory to a Cartesian cubical realizability framework that accounts for higher-dimensional types. We extend this framework to include a cumulative hierarchy of univalent Kan universes of Kan types, exact equality and other pretypes lacking Kan structure, and a cumulative hierarchy of pretype universes. As in Parts I and II, the main result is a canonicity theorem stating that closed terms of boolean type evaluate to either true or false. This establishes the computational interpretation of Cartesian cubical higher type theory based on cubical programs equipped with a deterministic operational semantics.

Chat View PDF

Computational Higher Type Theory II: Dependent Cubical Realizability

2016-01-01

Carlo Angiuli , Robert Harper

This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for … This is the second in a series of papers extending Martin-Löf's meaning explanation of dependent type theory to account for higher-dimensional types. We build on the cubical realizability framework for simple types developed in Part I, and extend it to a meaning explanation of dependent higher-dimensional type theory. This extension requires generalizing the computational Kan condition given in Part I, and considering the action of type families on paths. We define identification types, which classify identifications (paths) in a type, and dependent function and pair types. The main result is a canonicity theorem, which states that a closed term of boolean type evaluates to either true or false. This result establishes the first computational interpretation of higher dependent type theory by giving a deterministic operational semantics for its programs, including operations that realize the Kan condition.

Chat View PDF

Computational Higher Type Theory I: Abstract Cubical Realizability

2016-01-01

Carlo Angiuli , Robert Harper , Todd M. Wilson

Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf's meaning explanations for constructive type theory define the concept of a … Brouwer's constructivist foundations of mathematics is based on an intuitively meaningful notion of computation shared by all mathematicians. Martin-Löf's meaning explanations for constructive type theory define the concept of a type in terms of computation. Briefly, a type is a complete (closed) program that evaluates to a canonical type whose members are complete programs that evaluate to canonical elements of that type. The explanation is extended to incomplete (open) programs by functionality: types and elements must respect equality in their free variables. Equality is evidence-free---two types or elements are at most equal---and equal things are implicitly interchangeable in all contexts. Higher-dimensional type theory extends type theory to account for identifications of types and elements. An identification witnesses that two types or elements are explicitly interchangeable in all contexts by an explicit transport, or coercion, operation. There must be sufficiently many identifications, which is ensured by imposing a generalized form of the Kan condition from homotopy theory. Here we provide a Martin-Löf-style meaning explanation of simple higher-dimensional type theory based on a programming language that includes Kan-like constructs witnessing the computational meaning of the higher structure of types. The treatment includes an example of a higher inductive type (namely, the 1-dimensional sphere) and an example of Voevodsky's univalence principle, which identifies equivalent types. The main result is a computational canonicity theorem that validates the computational interpretation: a closed boolean expression must always evaluate to a boolean value, even in the presence of higher-dimensional structure. This provides the first fully computational formulation of higher-dimensional type theory.

Chat View PDF

Open maps of toposes

1980-03-01

Peter Johnstone

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition … We develop category theory within Univalent Foundations, which is a foundational system for mathematics based on a homotopical interpretation of dependent type theory. In this system, we propose a definition of ‘category’ for which equality and equivalence of categories agree. Such categories satisfy a version of the univalence axiom, saying that the type of isomorphisms between any two objects is equivalent to the identity type between these objects; we call them ‘saturated’ or ‘univalent’ categories. Moreover, we show that any category is weakly equivalent to a univalent one in a universal way. In homotopical and higher-categorical semantics, this construction corresponds to a truncated version of the Rezk completion for Segal spaces, and also to the stack completion of a prestack.

Chat View PDF

Higher Inductive Types as Homotopy-Initial Algebras

2014-12-19

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.

Chat View PDF

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-11-12

Chris Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, 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 Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

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

On the rules of proof in the pure functional calculus of the first order

1951-06-01

Andrzej Mostowski

We consider here the pure functional calculus of first order as formulated by Church. Church, l.c., p. 79, gives the definition of the validity of a formula in a given … We consider here the pure functional calculus of first order as formulated by Church. Church, l.c., p. 79, gives the definition of the validity of a formula in a given set I of individuals and shows that a formula is provable in if and only if it is valid in every non-empty set I . The definition of validity is preceded by the definition of a value of a formula; the notion of a value is the basic “semantical” notion in terms of which all other semantical notions are definable. The notion of a value of a formula retains its meaning also in the case when the set I is empty. We have only to remember that if I is empty, then an m -ary propositional function (i.e. a function from the m -th cartesian power I m to the set { f, t }) is the empty set. It then follows easily that the value of each well-formed formula with free individual variables is the empty set. The values of wffs without free variables are on the contrary either f or t . Indeed, if B has the unique free variable c and ϕ is the value of B , then the value of (c)B according to the definition given by Church is the propositional constant f or t according as ϕ(j) is f for at least one j in I or not. Since, however, there is no j in I , the condition ϕ(j) = t for all j in I is vacuously satisfied and hence the value of (c)B is t .

A C-system defined by a universe category

2014-09-28

Vladimir Voevodsky

This is a major update of the previous version. The methods of the paper are now fully constructive and the style is ready with the emphasis on the possibility of … This is a major update of the previous version. The methods of the paper are now fully constructive and the style is ready with the emphasis on the possibility of formalization both in type theory and in constructive set theory without the axiom of choice. This is the third paper in a series started in 1406.7413. In it we construct a C-system $CC({\cal C},p)$ starting from a category $\cal C$ together with a morphism $p:\widetilde{U}\rightarrow U$, a choice of pull-back squares based on $p$ for all morphisms to $U$ and a choice of a final object of $\cal C$. Such a quadruple is called a universe category. We then define universe category functors and construct homomorphisms of C-systems $CC({\cal C},p)$ defined by universe category functors. As a corollary of this construction and its properties we show that the C-systems corresponding to different choices of pull-backs and final objects are constructively isomorphic. In the second part of the paper we provide for any C-system CC three constructions of pairs $(({\cal C},p),H)$ where $({\cal C},p)$ is a universe category and $H:CC\rightarrow CC({\cal C},p)$ is an isomorphism. In the third part we define, using the constructions of the previous parts, for any category $C$ with a final object and fiber products a C-system $CC(C)$ and an equivalence $(J^*,J_*):C \rightarrow CC$.

Chat View PDF

Stack semantics of type theory

2017-06-01

Thierry Coquand , Bassel Mannaa , Fabian Ruch

We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an … We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalizing the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.

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

On a Topological Topos

1979-03-01

Peter Johnstone

Proceedings of the London Mathematical SocietyVolume s3-38, Issue 2 p. 237-271 Articles On a Topological Topos P. T. Johnstone, P. T. Johnstone Department of Pure Mathematics, University of Cambridge, 16 … Proceedings of the London Mathematical SocietyVolume s3-38, Issue 2 p. 237-271 Articles On a Topological Topos P. T. Johnstone, P. T. Johnstone Department of Pure Mathematics, University of Cambridge, 16 Mill Lane, Cambridge CB2 1SBSearch for more papers by this author P. T. Johnstone, P. T. Johnstone Department of Pure Mathematics, University of Cambridge, 16 Mill Lane, Cambridge CB2 1SBSearch for more papers by this author First published: March 1979 https://doi.org/10.1112/plms/s3-38.2.237Citations: 26AboutPDF ToolsRequest permissionExport citationAdd to favoritesTrack citation ShareShare Give accessShare full text accessShare full-text accessPlease review our Terms and Conditions of Use and check box below to share full-text version of article.I have read and accept the Wiley Online Library Terms and Conditions of UseShareable LinkUse the link below to share a full-text version of this article with your friends and colleagues. Learn more.Copy URL Share a linkShare onFacebookTwitterLinked InRedditWechat Citing Literature Volumes3-38, Issue2March 1979Pages 237-271 RelatedInformation

Acyclic groups of automorphisms

1983-12-01

Pierre de la Harpe , Dusa McDuff

Some two-generator one-relator non-Hopfian groups

1962-01-01

Gilbert Baumslag , D. Solitar

Chat View PDF

The Homotopy Groups of a Space of Maps between Oriented Closed Surfaces

1983-07-01

Vagn Lundsgaard Hansen

Fibrations that are cofibrations

1983-04-01

Juan Alonso

We give necessary and sufficient conditions for a homotopy cartesian square to be homotopy cocartesian. Specializing, we obtain a necessary and sufficient condition for a fibration to be a cofibration. … We give necessary and sufficient conditions for a homotopy cartesian square to be homotopy cocartesian. Specializing, we obtain a necessary and sufficient condition for a fibration to be a cofibration. We apply the above to localization of spaces and to acyclic maps.

Chat View PDF

A model for the homotopy theory of homotopy theory

2000-06-20

Charles Rezk

We describe a category, the objects of which may be viewed as models for homotopy theories. We show that for such models, “functors between two homotopy theories form a homotopy … We describe a category, the objects of which may be viewed as models for homotopy theories. We show that for such models, “functors between two homotopy theories form a homotopy theory”, or more precisely that the category of such models has a well-behaved internal hom-object.

La catégorie cubique avec connexions est une catégorie test stricte

2009-01-01

Georges Maltsiniotis

The aim of this paper is to prove that the category of cubes with connections, introduced by R. Brown and Ph.J. Higgins, is a strict test category in Grothendieck's sense.In … The aim of this paper is to prove that the category of cubes with connections, introduced by R. Brown and Ph.J. Higgins, is a strict test category in Grothendieck's sense.In particular this implies that cubical sets with connections are models for homotopy types in a very precise sense, in a way that is compatible with the cartesian product.

Chat View PDF