SU\G(𝔸)/K·U
Sign Up for free Log In

The simplicial model of Univalent Foundations (after Voevodsky)

Authors

Krzysztof Kapulkin, Peter LeFanu Lumsdaine
Type: Article
Publication Date: 2021-03-08
Citations: 67
DOI: https://doi.org/10.4171/jems/1050

Abstract

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.

Locations

  • arXiv (Cornell University)
    View PDF
  • Journal of the European Mathematical Society
    View PDF

Ask a Question About This Paper

Summary

Login to see paper summary

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.

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.

THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

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

Towards a constructive simplicial model of Univalent Foundations

2022-02-21
Nicola Gambino , Simon Henry
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results … We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent fibration that classifies small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, Σ $\Sigma$ -types, Π $\Pi$ -types and a univalent universe, leaving only a coherence question to be addressed.
View PDF Chat

Univalence in Simplicial Sets

2012-01-01
Chris Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky
We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations. We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.

Decomposing the Univalence Axiom

2017-01-01
Ian Orton , Andrew M. Pitts
This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, … This paper investigates Voevodsky's univalence axiom in intensional Martin-Löf type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.

Decomposing the Univalence Axiom.

2017-01-01
Ian Orton , Andrew M. Pitts
This paper investigates Voevodsky's univalence axiom in intensional Martin-Lof type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, … This paper investigates Voevodsky's univalence axiom in intensional Martin-Lof type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various published and unpublished sources; we then present a new decomposition of the univalence axiom into simpler axioms. We argue that these axioms are easier to verify in certain potential models of univalent type theory, particularly those models based on cubical sets. Finally we show how this decomposition is relevant to an open problem in type theory.

The Univalence Principle

2025-01-14
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined … The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk’s completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai’s First-Order Logic with Dependent Sorts, but is expressed in Voevodsky’s Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.

The Univalence Principle

2021-01-01
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined … The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai's First-Order Logic with Dependent Sorts, but is expressed in Voevodsky's Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.

Univalent universes for elegant models of homotopy types

2014-01-01
Denis-Charles Cisinski
We construct a univalent universe in the sense of Voevodsky in some suitable model categories for homotopy types (obtained from Grothendieck's theory of test categories). In practice, this means for … We construct a univalent universe in the sense of Voevodsky in some suitable model categories for homotopy types (obtained from Grothendieck's theory of test categories). In practice, this means for instance that, appart from the homotopy theory of simplicial sets, intensional type theory with the univalent axiom can be interpreted in the homotopy theory of cubical sets (with connections or not), or of Joyal's cellular sets.

The Univalence Principle.

2021-02-11
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined … The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk's completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai's First-Order Logic with Dependent Sorts, but is expressed in Voevodsky's Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.

Uniform Fibrations and the Frobenius Condition

2015-10-02
Nicola Gambino , Christian Sattler
We introduce and study the notion of a uniform fibration in categories with a functorial cylinder. In particular, we show that in a wide class of presheaf categories, including simplicial … We introduce and study the notion of a uniform fibration in categories with a functorial cylinder. In particular, we show that in a wide class of presheaf categories, including simplicial sets and cubical sets with connections, uniform fibrations are the right class of a natural weak factorization system and satisfy the Frobenius condition. This implies that pushforward along a uniform fibration preserves uniform fibrations. When instantiated in simplicial sets, this result gives a constructive counterpart of one of the key facts underpinning Voevodsky's simplicial model of univalent foundations, while in cubical sets it extends some of the existing work on cubical models of type theory by Coquand and others.

Introduction to Univalent Foundations of Mathematics with Agda.

2019-11-01
Martı́n Hötzel Escardó
We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Lof type theory. Agda allows us to … We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-Lof type theory. Agda allows us to write mathematical definitions, constructions, theorems and proofs, for example in number theory, analysis, group theory, topology, category theory or programming language theory, checking them for logical and mathematical correctness. Agda is a constructive mathematical system by default, which amounts to saying that it can also be considered as a programming language for manipulating mathematical objects. But we can assume the axiom of choice or the principle of excluded middle for pieces of mathematics that require them, at the cost of losing the implicit programming-language character of the system. For a fully constructive development of univalent mathematics in Agda, we would need to use its new cubical flavour, and we hope these notes provide a base for researchers interested in learning cubical type theory and cubical Agda as the next step. Compared to most expositions of the subject, we work with explicit universe levels.

Univalence and completeness of Segal objects

2022-11-11
Raffael Stenzel
View PDF Chat

Univalence and completeness of Segal objects

2019-01-01
Raffael Stenzel
Univalence, originally a type theoretical notion at the heart of Voevodsky's Univalent Foundations Program, has found general importance as a higher categorical property that characterizes descent and hence classifying maps … Univalence, originally a type theoretical notion at the heart of Voevodsky's Univalent Foundations Program, has found general importance as a higher categorical property that characterizes descent and hence classifying maps in $(\infty,1)$-categories. Completeness is a property of Segal spaces introduced by Rezk that characterizes those Segal spaces which are $(\infty,1)$-categories. In this paper, first, we make rigorous an analogy between univalence and completeness that has found various informal expressions in the higher categorical research community to date, and second, study its ramifications. The core aspect of this analogy can be understood as a translation between internal and external notions, motivated by model categorical considerations of Joyal and Tierney. As a result, we characterize the internal notion of univalence in logical model categories by the external notion of completeness defined as the right Quillen condition of suitably indexed Set-weighted limit functors. Furthermore, we extend the analogy and show that univalent completion in the sense of van den Berg and Moerdijk translates to Rezk-completion of associated Segal objects as well. Motivated by these correspondences, we exhibit univalence as a homotopical locality condition whenever univalent completion exists.
View PDF Chat

Simplicial sets inside cubical sets

2019-11-21
Thomas Streicher , Jonathan Weinberger
As observed recently by various people the topos $\mathbf{sSet}$ of simplicial sets appears as essential subtopos of a topos $\mathbf{cSet}$ of cubical sets, namely presheaves over the category $\mathbf{FL}$ of … As observed recently by various people the topos $\mathbf{sSet}$ of simplicial sets appears as essential subtopos of a topos $\mathbf{cSet}$ of cubical sets, namely presheaves over the category $\mathbf{FL}$ of finite lattices and monotone maps between them. The latter is a variant of the cubical model of type theory due to Cohen et al. for the purpose of providing a model for a variant of type theory which validates Voevodsky's Univalence Axiom and has computational meaning. Our contribution consists in constructing in $\mathbf{cSet}$ a fibrant univalent universe for those types that are sheaves. This makes it possible to consider $\mathbf{sSet}$ as a submodel of $\mathbf{cSet}$ for univalent Martin-Lof type theory. Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on $\mathbf{cSet}$ coincides with the test model structure, the latter of which models the homotopy theory of spaces. We do not provide an answer to this open problem, but instead give a reformulation in terms of the adjoint functors at hand.

Simplicial sets inside cubical sets

2019-11-01
Thomas Streicher , Jonathan Weinberger
As observed recently by various people the topos $\mathbf{sSet}$ of simplicial sets appears as essential subtopos of a topos $\mathbf{cSet}$ of cubical sets, namely presheaves over the category $\mathbf{FL}$ of … As observed recently by various people the topos $\mathbf{sSet}$ of simplicial sets appears as essential subtopos of a topos $\mathbf{cSet}$ of cubical sets, namely presheaves over the category $\mathbf{FL}$ of finite lattices and monotone maps between them. The latter is a variant of the cubical model of type theory due to Cohen et al. for the purpose of providing a model for a variant of type theory which validates Voevodsky's Univalence Axiom and has computational meaning. Our contribution consists in constructing in $\mathbf{cSet}$ a fibrant univalent universe for those types that are sheaves. This makes it possible to consider $\mathbf{sSet}$ as a submodel of $\mathbf{cSet}$ for univalent Martin-Lof type theory. Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on $\mathbf{cSet}$ coincides with the test model structure, the latter of which models the homotopy theory of spaces. We do not provide an answer to this open problem, but instead give a reformulation in terms of the adjoint functors at hand.

Univalent Foundations of Mathematics

2011-01-01
Vladimir Voevodsky
View PDF Chat

Homotopy type theory and Voevodsky's univalent foundations

2012-10-20
Álvaro Pelayo , Michael A. Warren
Recent discoveries have been made connecting abstract theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has … Recent discoveries have been made connecting abstract theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened homotopy type theory. In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property, called the Univalence Axiom, which has a number of striking consequences. He has subsequently advocated a program, which he calls univalent foundations, of developing mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model. Because type theory possesses good computational properties, this program can be carried out in a computer proof assistant. In this paper we give an introduction to type theory in Voevodsky's setting, paying attention to both theoretical and practical issues. In particular, the paper serves as an introduction to both the general ideas of type theory as well as to some of the concrete details of Voevodsky's work using the well-known proof assistant Coq. The paper is written for a general audience of mathematicians with basic knowledge of algebraic topology; the paper does not assume any preliminary knowledge of type theory, logic, or computer science.

Introduction to Univalent Foundations of Mathematics with Agda

2019-01-01
Martı́n Hötzel Escardó
We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-L\"of type theory. Agda allows us to … We introduce Voevodsky's univalent foundations and univalent mathematics, and explain how to develop them with the computer system Agda, which is based on Martin-L\"of type theory. Agda allows us to write mathematical definitions, constructions, theorems and proofs, for example in number theory, analysis, group theory, topology, category theory or programming language theory, checking them for logical and mathematical correctness. Agda is a constructive mathematical system by default, which amounts to saying that it can also be considered as a programming language for manipulating mathematical objects. But we can assume the axiom of choice or the principle of excluded middle for pieces of mathematics that require them, at the cost of losing the implicit programming-language character of the system. For a fully constructive development of univalent mathematics in Agda, we would need to use its new cubical flavour, and we hope these notes provide a base for researchers interested in learning cubical type theory and cubical Agda as the next step. Compared to most expositions of the subject, we work with explicit universe levels.
View PDF Chat

Syntax and models of Cartesian cubical type theory

2021-04-01
Carlo Angiuli , Guillaume Brunerie , Thierry Coquand +3 more
Abstract We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, … Abstract We present a cubical type theory based on the Cartesian cube category (faces, degeneracies, symmetries, diagonals, but no connections or reversal) with univalent universes, each containing Π, Σ, path, identity, natural number, boolean, suspension, and glue (equivalence extension) types. The type theory includes a syntactic description of a uniform Kan operation, along with judgmental equality rules defining the Kan operation on each type. The Kan operation uses both a different set of generating trivial cofibrations and a different set of generating cofibrations than the Cohen, Coquand, Huber, and Mörtberg (CCHM) model. Next, we describe a constructive model of this type theory in Cartesian cubical sets. We give a mechanized proof, using Agda as the internal language of cubical sets in the style introduced by Orton and Pitts, that glue, Π, Σ, path, identity, boolean, natural number, suspension types, and the universe itself are Kan in this model, and that the universe is univalent. An advantage of this formal approach is that our construction can also be interpreted in a range of other models, including cubical sets on the connections cube category and the De Morgan cube category, as used in the CCHM model, and bicubical sets, as used in directed type theory.
View PDF Chat

Homotopical inverse diagrams in categories with attributes

2020-09-09
Krzysztof Kapulkin , Peter LeFanu Lumsdaine
View PDF Chat

On Small Types in Univalent Foundations

2023-05-04
Tom de Jong , Martı́n Hötzel Escardó
We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements … We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. Moreover, we prove that locally small, nontrivial (directed or bounded) complete posets necessarily lack decidable equality. We prove our results for a general class of posets, which includes e.g. directed complete posets, bounded complete posets, sup-lattices and frames. Secondly, the fact that these nontrivial posets are necessarily large has the important consequence that Tarski's theorem (and similar results) cannot be applied in nontrivial instances. Furthermore, we explain that generalizations of Tarski's theorem that allow for large structures are provably false by showing that the ordinal of ordinals in a univalent universe has small suprema in the presence of set quotients. The latter also leads us to investigate the inter-definability and interaction of type universes of propositional truncations and set quotients, as well as a set replacement principle. Thirdly, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.
View PDF Chat

Non-accessible localizations

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

Non‐accessible localizations

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

A Cubical Language for Bishop Sets

2022-03-29
Jonathan Sterling , Carlo Angiuli , Daniel Gratzer
We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity … We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets \`a la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.
View PDF Chat

A Higher Structure Identity Principle

2020-05-25
Benedikt Ahrens , Paige Randall North , Michael Shulman +1 more
The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures … The ordinary Structure Identity Principle states that any property of set-level structures (e.g., posets, groups, rings, fields) definable in Univalent Foundations is invariant under isomorphism: more specifically, identifications of structures coincide with isomorphisms. We prove a version of this principle for a wide range of higher-categorical structures, adapting FOLDS-signatures to specify a general class of structures, and using two-level type theory to treat all categorical dimensions uniformly. As in the previously known case of 1-categories (which is an instance of our theory), the structures themselves must satisfy a local univalence principle, stating that identifications coincide with "isomorphisms" between elements of the structure. Our main technical achievement is a definition of such isomorphisms, which we call "indiscernibilities," using only the dependency structure rather than any notion of composition.
View PDF Chat

The Frobenius condition, right properness, and uniform fibrations

2017-03-01
Nicola Gambino , Christian Sattler
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can … We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform) fibrations and that satisfy the (functorial) Frobenius condition. As applications, we obtain a new proof that the Quillen model structure for Kan complexes is right proper, avoiding entirely the use of topological realization and minimal fibrations, and we solve an open problem in the study of Voevodsky's simplicial model of type theory, proving a constructive version of the preservation of Kan fibrations by pushforward along Kan fibrations. Our results also subsume and extend work by Coquand and others on cubical sets.
View PDF Chat

Extensional Concepts in Intensional Type Theory, Revisited

2023-01-01
Krzysztof Kapulkin , Yufeng Li
Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory … Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory extended by the principles of functional extensionality and of uniqueness of identity proofs.
View PDF Chat

The Hurewicz theorem in homotopy type theory

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

Two-sided cartesian fibrations of synthetic $$(\infty ,1)$$-categories

2024-06-21
Jonathan Weinberger

Delooping cyclic groups with lens spaces in homotopy type theory

2024-06-21
Samuel Mimram , Émile Oleon
View PDF Chat

On symmetries of spheres in univalent foundations

2024-06-21
Pierre Cagne , Ulrik Buchholtz , Nicolai Kraus +1 more
View PDF Chat

Syllepsis in Homotopy Type Theory

2022-08-02
Kristina Sojakova , G. A. Kavvos
The Eckmann-Hilton argument shows that any two monoid structures on the same set satisfying the interchange law are in fact the same operation, which is moreover commutative. When the monoids … The Eckmann-Hilton argument shows that any two monoid structures on the same set satisfying the interchange law are in fact the same operation, which is moreover commutative. When the monoids correspond to the vertical and horizontal composition of a sufficiently higher-dimensional category, the Eckmann-Hilton argument itself appears as a higher cell. This cell is often required to satisfy an additional piece of coherence, which is known as the syllepsis. We show that the syllepsis can be constructed from the elimination rule of intensional identity types in Martin-Löf type theory.
View PDF Chat

The effective model structure and -groupoid objects

2022-01-01
Nicola Gambino , Simon Henry , Christian Sattler +1 more
Abstract For a category $\mathcal {E}$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in … Abstract For a category $\mathcal {E}$ with finite limits and well-behaved countable coproducts, we construct a model structure, called the effective model structure, on the category of simplicial objects in $\mathcal {E}$ , generalising the Kan–Quillen model structure on simplicial sets. We then prove that the effective model structure is left and right proper and satisfies descent in the sense of Rezk. As a consequence, we obtain that the associated $\infty $ -category has finite limits, colimits satisfying descent, and is locally Cartesian closed when $\mathcal {E}$ is but is not a higher topos in general. We also characterise the $\infty $ -category presented by the effective model structure, showing that it is the full sub-category of presheaves on $\mathcal {E}$ spanned by Kan complexes in $\mathcal {E}$ , a result that suggests a close analogy with the theory of exact completions.
View PDF Chat

Abstraction, equality and univalence

2023-07-30
Gabriel Catren
We shall propose a conceptual-oriented discussion of the so-called Univalent Foundations Program, that is, of Martin-Löf type theory enriched with a homotopic interpretation, together with the univalence axiom proposed by … We shall propose a conceptual-oriented discussion of the so-called Univalent Foundations Program, that is, of Martin-Löf type theory enriched with a homotopic interpretation, together with the univalence axiom proposed by Voevodsky. We shall argue that the type-theoretic notion of propositional equality encodes the notion of indiscernibility, we shall address the homotopic interpretation of Martin-Löf type theory, and we shall analyse whether Leibniz's principle of the identity of indiscernibles holds or not in Univalent Foundations. We shall finally argue that univalence can be understood as a particular implementation of a constructive notion of abstraction that resolves Fregean abstraction. This article is part of the theme issue 'Identity, individuality and indistinguishability in physics and mathematics'.
View PDF Chat

C-system of a module over a Jf-relative monad

2022-11-24
Vladimir Voevodsky
View PDF Chat

A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory

2022-01-01
Mitchell Vern Riley
Homotopy type theory allows for a synthetic formulation of homotopy theory, where arguments can be checked by computer and automatically apply in many semantic settings.Modern homotopy theory makes essential use … Homotopy type theory allows for a synthetic formulation of homotopy theory, where arguments can be checked by computer and automatically apply in many semantic settings.Modern homotopy theory makes essential use of the category of spectra, the natural setting in which to investigate 'stable' phenomena: the suspension and loop space operations become inverses.One can define a version of spectra internally to type theory, but this definition can be quite difficult to work with.In particular, there is not presently a convenient way to construct and manipulate the smash product and internal hom of such spectra.This thesis describes an extension of Martin-L öf Type Theory that is suitable for working with these constructions synthetically.There is an ∞-topos of parameterised spectra, whose objects are an index space with a family of spectra over it, so standard homotopy type theory can be interpreted in this setting.To isolate the spaces (as objects with the trivial family of spectra) and the spectra (as objects with trivial indexing space), we extend type theory with a novel modality ♮ that is simultaneously a monad and a comonad.Intuitively, this modality keeps the base of an object the same but replaces the spectrum over each point with a trivial one.The system is further extended with a monoidal tensor ⊗, unit S and internal hom ⊸, which capture abstractly the constructions on spectra mentioned above.We are lead naturally to consider a 'bunched' type theory, where the contexts have a tree-like structure.The modality is crucial for making dependency in these linear type formers work correctly: dependency between ⊗ 'bunches' is mediated by ♮.To demonstrate that this type theory is usable in practice, we prove some basic synthetic results in this new system.For example, externally, any map of spaces induces a 'six-functor formalism' between the categories of parameterised spectra over those spaces, and this structure can be reconstructed internal to the type theory.We additionally investigate an axiom asserting that the internal category of spectra is semiadditive; we show that in the presence of univalence this in fact implies that the category of spectra is stable.This thesis could not have been written without the limitless type-theoretic wisdom and equally limitless patience and kindness of my advisor Dan Licata.His support made it possible to persist past the many syntactic dead ends that I walked myself down, and he has my deepest gratitude.I am grateful to the members of the HoTT community for countless enlightening conversations, particularly Eric Finster, Mike Shulman, Mathieu Anel, David Jaz Myers, and all of the HoTT MURI Team.I owe a particular debt to Eric, for putting forward what has proven to be a fruitful avenue for research.
View PDF Chat

Topological Quantum Gates in Homotopy Type Theory

2024-07-01
David Jaz Myers , Hisham Sati , Urs Schreiber

Towards a constructive simplicial model of Univalent Foundations

2022-02-21
Nicola Gambino , Simon Henry
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results … We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of Univalent Foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory, building on the constructive version of the Kan-Quillen model structure established by the second-named author. In particular, we show that dependent products along fibrations with cofibrant domains preserve fibrations, establish the weak equivalence extension property for weak equivalences between fibrations with cofibrant domain and define a univalent fibration that classifies small fibrations between bifibrant objects. These results allow us to define a comprehension category supporting identity types, Σ $\Sigma$ -types, Π $\Pi$ -types and a univalent universe, leaving only a coherence question to be addressed.
View PDF Chat

Polynomials in homotopy type theory as a Kleisli category

2024-12-11
Elies Harington , Samuel Mimram
Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type … Polynomials in a category have been studied as a generalization of the traditional notion in mathematics. Their construction has recently been extended to higher groupoids, as formalized in homotopy type theory, by Finster, Mimram, Lucas and Seiller, thus resulting in a cartesian closed bicategory. We refine and extend their work in multiple directions. We begin by generalizing the construction of the free symmetric monoid monad on types in order to handle arities in an arbitrary universe. Then, we extend this monad to the (wild) category of spans of types, and thus to a comonad by self-duality. Finally, we show that the resulting Kleisli category is equivalent to the traditional category of polynomials. This thus establishes polynomials as a (homotopical) model of linear logic. In fact, we explain that it is closely related to a bicategorical model of differential linear logic introduced by Melli\`es.
View PDF Chat

The law of excluded middle in the simplicial model of type theory

2020-06-10
Chris Kapulkin , Peter LeFanu Lumsdaine
We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence. We show that the law of excluded middle holds in Voevodsky's simplicial model of type theory. As a corollary, excluded middle is compatible with univalence.

Homotopical inverse diagrams in categories with attributes

2018-08-06
Chris Kapulkin , Peter LeFanu Lumsdaine
We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct … We define and develop the infrastructure of homotopical inverse diagrams in categories with attributes. Specifically, given a category with attributes $C$ and an ordered homotopical inverse category $I$, we construct the category with attributes $C^I$ of homotopical diagrams of shape $I$ in $C$ and Reedy types over these; and we show how various logical structure ($\Pi$-types, identity types, and so on) lifts from $C$ to $C^I$. This may be seen as providing a general class of diagram models of type theory. In a companion paper The homotopy theory of type theories (arXiv:1610.00037), we apply the present results to construct semi-model structures on categories of contextual categories.

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.
View PDF Chat

Univalent categories of modules

2023-02-01
Jarl G. Taxerås Flaten
Abstract We show that categories of modules over a ring in homotopy type theory (HoTT) satisfy the internal versions of the AB axioms from homological algebra. The main subtlety lies … Abstract We show that categories of modules over a ring in homotopy type theory (HoTT) satisfy the internal versions of the AB axioms from homological algebra. The main subtlety lies in proving AB4, which is that coproducts indexed by arbitrary sets are left-exact. To prove this, we replace a set X with the strict category of lists of elements in X . From showing that the latter is filtered, we deduce left-exactness of the coproduct. More generally, we show that exactness of filtered colimits (AB5) implies AB4 for any abelian category in HoTT. Our approach is heavily inspired by Roswitha Harting’s construction of the internal coproduct of abelian groups in an elementary topos with a natural numbers object. To state the AB axioms, we define and study filtered (and sifted) precategories in HoTT. A key result needed is that filtered colimits commute with finite limits of sets. This is a familiar classical result but has not previously been checked in our setting. Finally, we interpret our most central results into an $\infty$ -topos $ {\mathscr{X}} $ . Given a ring R in $ {\tau_{\leq 0}({{\mathscr{X}}})} $ – for example, an ordinary sheaf of rings – we show that the internal category of R -modules in $ {\mathscr{X}} $ represents the presheaf which sends an object $ X \in {\mathscr{X}} $ to the category of $ (X{\times}R) $ -modules in ${\mathscr{X}} / X$ . In general, our results yield a product-preserving left adjoint to base change of modules over X . When X is 0-truncated, this left adjoint is the internal coproduct. By an internalisation procedure, we deduce left-exactness of the internal coproduct as an ordinary functor from its internal left-exactness coming from HoTT.
View PDF Chat

The category of iterative sets in homotopy type theory and univalent foundations

2024-11-19
Daniel Gratzer , Håkon Robbestad Gylterud , Anders Mörtberg +1 more
Abstract When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathcal{Set}$ , is replaced by the category $\mathcal{hSet}$ of homotopy sets (h-sets); … Abstract When working in homotopy type theory and univalent foundations, the traditional role of the category of sets, $\mathcal{Set}$ , is replaced by the category $\mathcal{hSet}$ of homotopy sets (h-sets); types with h-propositional identity types. Many of the properties of $\mathcal{Set}$ hold for $\mathcal{hSet}$ ((co)completeness, exactness, local cartesian closure, etc.). Notably, however, the univalence axiom implies that $\mathsf{Ob}\,\mathcal{hSet}$ is not itself an h-set, but an h-groupoid. This is expected in univalent foundations, but it is sometimes useful to also have a stricter universe of sets, for example, when constructing internal models of type theory. In this work, we equip the type of iterative sets $\mathsf{V}^0$ , due to Gylterud ((2018). The Journal of Symbolic Logic 83 (3) 1132–1146) as a refinement of the pioneering work of Aczel ((1978). Logic Colloquium’77 , Studies in Logic and the Foundations of Mathematics, vol. 96, Elsevier, 55–66.) on universes of sets in type theory, with the structure of a Tarski universe and show that it satisfies many of the good properties of h-sets. In particular, we organize $\mathsf{V}^0$ into a (non-univalent strict) category and prove that it is locally cartesian closed. This enables us to organize it into a category with families with the structure necessary to model extensional type theory internally in HoTT/UF. We do this in a rather minimal univalent type theory with W-types, in particular we do not rely on any HITs, or other complex extensions of type theory. Furthermore, the construction of $\mathsf{V}^0$ and the model is fully constructive and predicative, while still being very convenient to work with as the decoding from $\mathsf{V}^0$ into h-sets commutes definitionally for all type constructors. Almost all of the paper has been formalized in $\texttt{Agda}$ using the $\texttt{agda}$ - $\texttt{unimath}$ library of univalent mathematics.
View PDF Chat

Simplicial sets inside cubical sets

2019-11-21
Thomas Streicher , Jonathan Weinberger
As observed recently by various people the topos $\mathbf{sSet}$ of simplicial sets appears as essential subtopos of a topos $\mathbf{cSet}$ of cubical sets, namely presheaves over the category $\mathbf{FL}$ of … As observed recently by various people the topos $\mathbf{sSet}$ of simplicial sets appears as essential subtopos of a topos $\mathbf{cSet}$ of cubical sets, namely presheaves over the category $\mathbf{FL}$ of finite lattices and monotone maps between them. The latter is a variant of the cubical model of type theory due to Cohen et al. for the purpose of providing a model for a variant of type theory which validates Voevodsky's Univalence Axiom and has computational meaning. Our contribution consists in constructing in $\mathbf{cSet}$ a fibrant univalent universe for those types that are sheaves. This makes it possible to consider $\mathbf{sSet}$ as a submodel of $\mathbf{cSet}$ for univalent Martin-Lof type theory. Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on $\mathbf{cSet}$ coincides with the test model structure, the latter of which models the homotopy theory of spaces. We do not provide an answer to this open problem, but instead give a reformulation in terms of the adjoint functors at hand.

Constructing Higher Inductive Types as Groupoid Quotients

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

On Small Types in Univalent Foundations

2021-01-01
Tom de Jong , Martı́n Hötzel Escardó
We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements … We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. Moreover, we prove that locally small, nontrivial (directed or bounded) complete posets necessarily lack decidable equality. We prove our results for a general class of posets, which includes e.g. directed complete posets, bounded complete posets, sup-lattices and frames. Secondly, the fact that these nontrivial posets are necessarily large has the important consequence that Tarski's theorem (and similar results) cannot be applied in nontrivial instances. Furthermore, we explain that generalizations of Tarski's theorem that allow for large structures are provably false by showing that the ordinal of ordinals in a univalent universe has small suprema in the presence of set quotients. The latter also leads us to investigate the inter-definability and interaction of type universes of propositional truncations and set quotients, as well as a set replacement principle. Thirdly, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.
View PDF Chat

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.
View PDF Chat

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.

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.
View PDF Chat

Towards a Directed Homotopy Type Theory

2019-11-01
Paige Randall North
In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type … In this paper, we present a directed homotopy type theory for reasoning synthetically about (higher) categories and directed homotopy theory. We specify a new 'homomorphism' type former for Martin-Löf type theory which is roughly analogous to the identity type former originally introduced by Martin-Löf. The homomorphism type former is meant to capture the notions of morphism (from the theory of categories) and directed path (from directed homotopy theory) just as the identity type former is known to capture the notions of isomorphism (from the theory of groupoids) and path (from homotopy theory). Our main result is an interpretation of these homomorphism types into Cat, the category of small categories. There, the interpretation of each homomorphism type homC(a,b) is indeed the set of morphisms between the objects a and b of the category C. We end the paper with an analysis of the interpretation in Cat with which we argue that our homomorphism types are indeed the directed version of Martin-Löf's identity types
View PDF Chat

Stefania Centrone, Deborah Kant, and Deniz Sarikaya, eds, <i>Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory, and General Thoughts</i>

2021-09-08
Hans-Christoph Kotzsch
The advent of Homotopy Type Theory/Univalent Foundations (HoTT/UF) in recent years has given a new impetus to the ever ongoing philosophical discussion about foundations of mathematics. What does foundation mean … The advent of Homotopy Type Theory/Univalent Foundations (HoTT/UF) in recent years has given a new impetus to the ever ongoing philosophical discussion about foundations of mathematics. What does foundation mean in the first place, what is it to achieve, how does it relate to every-day mathematical practice? Set theory as embodied by ZFC was widely deemed throughout the twentieth century to be the most natural and successful approach to foundations of mathematics. Although discussion as to its conceptual and foundational status steadily accompanied its development, and alternative approaches have been present throughout, foundation was to a large part synonymous with classical set theory. Alternative approaches, from around 1950 onward, included those that prioritized category-theoretic intuitions and ideas, as later studied, e.g., in topos theory. Others proceeded directly from constructivist principles, such as constructive set theory and Martin-Löf Type Theory, which were developed since the 1970s. While the first stayed...

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.

Bicategories in univalent foundations

2021-11-01
Benedikt Ahrens , Dan Frumin , Marco Maggesi +2 more
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples … We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.
View PDF Chat

Semantics for two-dimensional type theory

2022-08-02
Benedikt Ahrens , Paige Randall North , Niels van der Weide
We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory … We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature.
View PDF Chat

What should a generic object be?

2023-01-01
Jonathan Sterling
Abstract Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important fibrational … Abstract Jacobs has proposed definitions for (weak, strong, split) generic objects for a fibered category; building on his definition of (split) generic objects, Jacobs develops a menagerie of important fibrational structures with applications to categorical logic and computer science, including higher order fibrations , polymorphic fibrations , $\lambda2$ - fibrations , triposes , and others. We observe that a split generic object need not in particular be a generic object under the given definitions, and that the definitions of polymorphic fibrations, triposes, etc. are strict enough to rule out some fundamental examples: for instance, the fibered preorder induced by a partial combinatory algebra in realizability is not a tripos in this sense. We propose a new alignment of terminology that emphasizes the forms of generic object appearing most commonly in nature, i.e. in the study of internal categories, triposes, and the denotational semantics of polymorphism. In addition, we propose a new class of acyclic generic objects inspired by recent developments in higher category theory and the semantics of homotopy type theory, generalizing the realignment property of universes to the setting of an arbitrary fibration.
View PDF Chat

Modal fracture of higher groups

2024-08-20
David Jaz Myers
View PDF Chat

Canonicity and homotopy canonicity for cubical type theory

2022-02-03
Thierry Coquand , Simon Huber , Christian Sattler
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on … Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.
View PDF Chat

Locally Presentable and Accessible Categories

1994-03-10
J. Adámek , J. Rosicky
The concepts of a locally presentable category and an accessible category have turned out to be useful in formulating connections between universal algebra, model theory, logic and computer science. The … The concepts of a locally presentable category and an accessible category have turned out to be useful in formulating connections between universal algebra, model theory, logic and computer science. The aim of this book is to provide an exposition of both the theory and the applications of these categories at a level accessible to graduate students. Firstly the properties of l-presentable objects, locally l-presentable categories, and l-accessible categories are discussed in detail, and the equivalence of accessible and sketchable categories is proved. The authors go on to study categories of algebras and prove that Freyd's essentially algebraic categories are precisely the locally presentable categories. In the final chapters they treat some topics in model theory and some set theoretical aspects. For researchers in category theory, algebra, computer science, and model theory, this book will be a necessary purchase.

Subsystems and regular quotients of C-systems

2016-01-01
Vladimir Voevodsky
C-systems were introduced by J. Cartmell under the name contextual categories. In this note we study sub-objects and quotient-objects of C-systems. In the case of the sub-objects we consider all … C-systems were introduced by J. Cartmell under the name contextual categories. In this note we study sub-objects and quotient-objects of C-systems. In the case of the sub-objects we consider all sub-objects while in the case of the quotient-objects only {\em regular} quotients that in particular have the property that the corresponding projection morphism is surjective both on objects and on morphisms. It is one of several short papers based on the material of the Notes on Type Systems by the same author. This version is essentially identical with the version published in Contemporary Mathematics n.658.
View PDF Chat

A C-system defined by a universe category

2014-01-01
Vladimir Voevodsky
This is a major update of the previous version. The methods of the paper are now fully constructive and the style is "formalization ready" with the emphasis on the possibility … This is a major update of the previous version. The methods of the paper are now fully constructive and the style is "formalization 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$.

Extensional concepts in intensional type theory

1995-01-01
Martin Hofmann

On the interpretation of type theory in locally cartesian closed categories

1995-01-01
Martin Hofmann

Wellfounded Trees and Dependent Polynomial Functors

2004-01-01
Nicola Gambino , Martin Hyland
View PDF Chat

C-system of a module over a monad on sets 1

2014-07-12
Vladimir Voevodsky
AbstractThis is the second paper in a series started in [13] which aims to provide mathematicaldescriptions of objects and constructions related to the rst few steps of the semantical theoryof … AbstractThis is the second paper in a series started in [13] which aims to provide mathematicaldescriptions of objects and constructions related to the rst few steps of the semantical theoryof dependent type systems.We construct for any pair ( M;LM ), where M is a monad on sets and LM is a left moduleover M , a C-system (\contextual category) CC ( M;LM ) and describe, using the results of [13]a class of sub-quotients of CC ( M;LM ) in terms of objects directly constructed from M and LM . In the special case of the monads of expressions associated with nominal signatures thisconstruction gives the C-systems of general dependent type theories when they are speci ed bycollections of judgements of the four standard kinds. 1 Introduction The rst few steps in all approaches to the semantics of dependent type theories remain ffitlyunderstood. The constructions which have been worked out in detail in the case of a few particulartype systems by dedicated authors are being extended to the wide variety of type systems underconsideration today by analogy. This is not acceptable in mathematics. Instead we should be ableto obtain the required results for new type systems by

Wellfounded trees in categories

2000-07-01
Ieke Moerdijk , Erik Palmgren

Comprehension categories and the semantics of type dependency

1993-01-01
Bart Jacobs

Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

2011-09-04
Steve Awodey , Richard Garner , Per Martin-Löf +1 more
Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in … Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in the form of an interpretation of the dependent type theory of Per Martin-Löf into classical homotopy theory. The interpretation results in a bridge between the worlds of constructive and classical mathematics which promises to shed new light on both. This mini-workshop brought together researchers in logic, topology, and cognate fields in order to explore both theoretical and practical ramifications of this discovery.
View PDF Chat

Locally cartesian closed categories and type theory

1984-01-01
R. A. G. Seely
It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/ A are cartesian … It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/ A are cartesian closed. In such a category, the notion of a ‘generalized set’, for example an ‘ A -indexed set’, is represented by a morphism B → A of C, i.e. by an object of C/ A . The point about such a category C is that C is a C-indexed category, and more, is a hyper-doctrine, so that it has a full first order logic associated with it. This logic has some peculiar aspects. For instance, the types are the objects of C and the terms are the morphisms of C. For a given type A , the predicates with a free variable of type A are morphisms into A , and ‘proofs’ are morphisms over A . We see here a certain ‘ambiguity’ between the notions of type, predicate, and term, of object and proof: a term of type A is a morphism into A , which is a predicate over A ; a morphism 1 → A can be viewed either as an object of type A or as a proof of the proposition A .

Homotopy Theoretic Aspects of Constructive Type Theory

2008-01-01
Michael A. Warren

Homotopy-Theoretic Models of Type Theory

2011-01-01
Peter Arndt , Krzysztof Kapulkin
View PDF Chat

Simplicial objects in algebraic topology

1993-01-15
J. P. May
Since it was first published in 1967, Objects in Algebraic Topology has been the standard reference for the theory of simplicial sets and their relationship to the homotopy theory of … Since it was first published in 1967, Objects in Algebraic Topology has been the standard reference for the theory of simplicial sets and their relationship to the homotopy theory of topological spaces. J. Peter May gives a lucid account of the basic homotopy theory of simplicial sets (discrete analogs of topological spaces) which have played a central role in algebraic topology ever since their introduction in the late 1940s. Simplicial Objects in Algebraic Topology presents much of the elementary material of algebraic topology from the semi-simplicial viewpoint. It should prove very valuable to anyone wishing to learn semi-simplicial topology. [May] has included detailed proofs, and he has succeeded very well in the task of organizing a large body of previously scattered material.--Mathematical Review

Martin-Lof identity types in the C-systems defined by a universe category

2015-01-01
Vladimir Voevodsky
This paper continues the series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the … This paper continues the series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the identity types in the intensional Martin-Lof type theories on the C-systems that arise from universe categories. In the first part of the paper we develop constructions that produce interpretations of these rules from certain structures on universe categories while in the second we study the functoriality of these constructions with respect to functors of universe categories. The results of the first part of the paper play a crucial role in the construction of the univalent model of type theory in simplicial sets.

An experimental library of formalized Mathematics based on the univalent foundations

2015-01-20
Vladimir Voevodsky
This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started … This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).
View PDF Chat

The identity type weak factorisation system

2008-09-03
Nicola Gambino , Richard Garner
View PDF Chat

On Semisimplicial Fibre-Bundles

1959-07-01
M. G. Barratt , V. K. A. M. Gugenheim , John C. Moore

W-types in homotopy-type theory – CORRIGENDUM

2016-04-05
Benno van den Berg , Ieke Moerdijk
In the article below, Theorem 3.4 requires the additional assumption that A is Kan as well. Indeed, the inductive proof as given only shows that if W ( f ) … In the article below, Theorem 3.4 requires the additional assumption that A is Kan as well. Indeed, the inductive proof as given only shows that if W ( f ) &lt;α is a Kan complex, then W ( f ) &lt;α+1 → A is a Kan fibration.
View PDF Chat

Univalence in locally cartesian closed ∞-categories

2016-11-06
David Gepner , Joachim Kock
Abstract After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories, we establish the representability of equivalences and show that … Abstract After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories, we establish the representability of equivalences and show that univalent families, in the sense of Voevodsky, form a poset isomorphic to the poset of bounded local classes, in the sense of Lurie. It follows that every <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -topos has a hierarchy of “universal” univalent families, indexed by regular cardinals, and that n -topoi have univalent families classifying <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mo>(</m:mo> <m:mrow> <m:mi>n</m:mi> <m:mo>-</m:mo> <m:mn>2</m:mn> </m:mrow> <m:mo>)</m:mo> </m:mrow> </m:math> ${(n-2)}$ -truncated maps. We show that univalent families are preserved (and detected) by right adjoints to locally cartesian localizations, and use this to exhibit certain canonical univalent families in <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> $\infty$ -quasitopoi (certain <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories of “separated presheaves”, introduced here). We also exhibit some more exotic examples of univalent families, illustrating that a univalent family in an n -topos need not be <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mo>(</m:mo> <m:mrow> <m:mi>n</m:mi> <m:mo>-</m:mo> <m:mn>2</m:mn> </m:mrow> <m:mo>)</m:mo> </m:mrow> </m:math> ${(n-2)}$ -truncated, as well as some univalent families in the Morel–Voevodsky <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category of motivic spaces, an instance of a locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category which is not an n -topos for any <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mn>0</m:mn> <m:mo>≤</m:mo> <m:mi>n</m:mi> <m:mo>≤</m:mo> <m:mi>∞</m:mi> </m:mrow> </m:math> ${0\leq n\leq\infty}$ . Lastly, we show that any presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category is modeled by a combinatorial type-theoretic model category, and conversely that the <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -category underlying a combinatorial type-theoretic model category is presentable and locally cartesian closed. Under this correspondence, univalent families in presentable locally cartesian closed <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mi>∞</m:mi> </m:math> ${\infty}$ -categories correspond to univalent fibrations in combinatorial type-theoretic model categories.

An introduction to univalent foundations for mathematicians

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

Homotopy type theory and Voevodsky’s univalent foundations

2014-05-09
Álvaro Pelayo , Michael A. Warren
Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which … Recent discoveries have been made connecting abstract homotopy theory and the field of type theory from logic and theoretical computer science. This has given rise to a new field, which has been christened <italic>homotopy type theory</italic>. In this direction, Vladimir Voevodsky observed that it is possible to model type theory using simplicial sets and that this model satisfies an additional property, called the <italic>Univalence Axiom</italic>, which has a number of striking consequences. He has subsequently advocated a program, which he calls <italic>univalent foundations</italic>, of developing mathematics in the setting of type theory with the Univalence Axiom and possibly other additional axioms motivated by the simplicial set model. Because type theory possesses good computational properties, this program can be carried out in a computer proof assistant. In this paper we give an introduction to homotopy type theory in Voevodsky’s setting, paying attention to both theoretical and practical issues. In particular, the paper serves as an introduction to both the general ideas of homotopy type theory as well as to some of the concrete details of Voevodsky’s work using the well-known proof assistant Coq. The paper is written for a general audience of mathematicians with basic knowledge of algebraic topology; the paper does not assume any preliminary knowledge of type theory, logic, or computer science. Because a defining characteristic of Voevodsky’s program is that the Coq code has fundamental mathematical content, and many of the mathematical concepts which are efficiently captured in the code cannot be explained in standard mathematical English without a lengthy detour through type theory, the later sections of this paper (beginning with Section \ref{sec2}) make use of code; however, all notions are introduced from the beginning and in a self-contained fashion.
View PDF Chat

W-types in homotopy type theory

2014-11-24
Benno van den Berg , Ieke Moerdijk
We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories … We will give a detailed account of why the simplicial sets model of the univalence axiom due to Voevodsky also models W-types. In addition, we will discuss W-types in categories of simplicial presheaves and an application to models of set theory.
View PDF Chat

Homotopy theoretic models of identity types

2008-07-14
Steve Awodey , Michael A. Warren
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
View PDF Chat

A Survey of Graphical Languages for Monoidal Categories

2010-01-01
Peter Selinger
View PDF Chat

Univalence for inverse diagrams and homotopy canonicity

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

The local universes model: an overlooked coherence construction for dependent type theories

2014-11-06
Peter LeFanu Lumsdaine , Michael A. Warren
We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive … We present a new coherence theorem for comprehension categories, providing strict models of dependent type theory with all standard constructors, including dependent products, dependent sums, identity types, and other inductive types. Precisely, we take as input a weak model: a comprehension category, equipped with structure corresponding to the desired logical constructions. We assume throughout that the base category is close to locally Cartesian closed: specifically, that products and certain exponentials exist. Beyond this, we require only that the logical structure should be *weakly stable* --- a pure existence statement, not involving any specific choice of structure, weaker than standard categorical Beck--Chevalley conditions, and holding in the now standard homotopy-theoretic models of type theory. Given such a comprehension category, we construct an equivalent split one, whose logical structure is strictly stable under reindexing. This yields an interpretation of type theory with the chosen constructors. The model is adapted from Voevodsky's use of universes for coherence, and at the level of fibrations is a classical construction of Giraud. It may be viewed in terms of local universes or delayed substitutions.
View PDF Chat

Simplicial Homotopy Theory

1999-01-01
Paul G. Goerss , John F. Jardine
View PDF Chat

A formal proof of the four color theorem

2009-01-01
Limin Xiang
A formal proof has not been found for the four color theorem since 1852 when Francis Guthrie first conjectured the four color theorem. Why? A bad idea, we think, directed … A formal proof has not been found for the four color theorem since 1852 when Francis Guthrie first conjectured the four color theorem. Why? A bad idea, we think, directed people to a rough road. Using a similar method to that for the formal proof of the five color theorem, a formal proof is proposed in this paper of the four color theorem, namely, every planar graph is four-colorable. The formal proof proposed can also be regarded as an algorithm to color a planar graph using four colors so that no two adjacent vertices receive the same color.

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

2016-12-22
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.
View PDF Chat