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

Author Description

Login to generate an author description

Ask a Question About This Mathematician

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01
Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
View PDF Chat

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.

Quipper

2013-06-16
Alexander S. Green , Peter LeFanu Lumsdaine , Neil J. Ross +2 more
The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level … The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and can generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.
View PDF Chat

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.

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

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

An Introduction to Quantum Programming in Quipper

2013-01-01
Alexander S. Green , Peter LeFanu Lumsdaine , Neil J. Ross +2 more
View PDF Chat

Weak ω-Categories from Intensional Type Theory

2009-01-01
Peter LeFanu Lumsdaine

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

The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories

2015-07-04
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

Homotopy limits in type theory

2015-01-19
Jeremy Avigad , Krzysztof Kapulkin , Peter LeFanu Lumsdaine
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed … Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.
View PDF Chat

Weak omega-categories from intensional type theory

2010-09-17
Peter LeFanu Lumsdaine
We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. … We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.
View PDF Chat

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

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

The homotopy theory of type theories

2018-08-30
Krzysztof Kapulkin , Peter LeFanu Lumsdaine
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.

The Local Universes Model

2015-07-04
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

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

Lawvere–Tierney sheaves in Algebraic Set Theory

2009-06-16
Steve Awodey , Nicola Gambino , Peter LeFanu Lumsdaine +1 more
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that … We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.
View PDF Chat

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.

On the Bourbaki–Witt principle in toposes

2013-03-18
Andrej Bauer , Peter LeFanu Lumsdaine
The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and … The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Among other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not imply that fixed points can always be found by transfinite iteration. Meanwhile, on the side of models, we see that the principle fails in realisability toposes, and does not hold in the free topos, but does hold in all cocomplete toposes.
View PDF Chat

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

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

The homotopy theory of type theories

2016-09-30
Chris Kapulkin , Peter LeFanu Lumsdaine
We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is … We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

A general definition of dependent type theories

2020-01-01
Andrej Bauer , Philipp G. Haselwarter , Peter LeFanu Lumsdaine
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing … We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive reading of syntax, yielding the traditional presentations of specific theories as closely as possible. Specifically, we give three main definitions: raw type theories, a minimal setup for discussing dependently typed derivability; acceptable type theories, including extra conditions ensuring well-behavedness; and well-presented type theories, generalising how in traditional presentations, the well-behavedness of a type theory is established step by step as the type theory is built up. Following these, we show that various fundamental fitness-for-purpose metatheorems hold in this generality. Much of the present work has been formalised in the proof assistant Coq.

Displayed Categories

2017-01-01
Benedikt Ahrens , Peter LeFanu Lumsdaine
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but … We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.
View PDF Chat

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.

Categorical structures for type theory in univalent foundations

2017-01-01
Benedikt Ahrens , Peter LeFanu Lumsdaine , Vladimir Voevodsky
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps … In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.
View PDF Chat

A Small Observation on Co-categories

2009-01-01
Peter LeFanu Lumsdaine
Various concerns suggest looking for internal co-categories in categories with strong logical structure. It turns out that in any coherent category, all co-categories are co-equivalence relations. Various concerns suggest looking for internal co-categories in categories with strong logical structure. It turns out that in any coherent category, all co-categories are co-equivalence relations.

Parametricity, automorphisms of the universe, and excluded middle

2017-06-27
Auke Bart Booij , Martı́n Hötzel Escardó , Peter LeFanu Lumsdaine +1 more
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific … It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instan ...

Homotopy limits in Coq

2013-04-02
Jeremy Avigad , Krzysztof Kapulkin , Peter LeFanu Lumsdaine

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

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

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

2020-09-03
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.

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

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

Displayed Categories

2017-09-03
Benedikt Ahrens , Peter LeFanu Lumsdaine
View PDF Chat

Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341).

2018-01-01
Andrej Bauer , Martı́n Hötzel Escardó , Peter LeFanu Lumsdaine +1 more

Parametricity, automorphisms of the universe, and excluded middle

2017-01-01
Auke Bart Booij , Martı́n Hötzel Escardó , Peter LeFanu Lumsdaine +1 more
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific … It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.

Homotopical inverse diagrams in categories with attributes

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

Homotopical inverse diagrams in categories with attributes

2018-01-01
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.

The homotopy theory of type theories

2016-01-01
Chris Kapulkin , Peter LeFanu Lumsdaine
We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is … We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.
View PDF Chat

Constructive reflection principles for regular theories

2016-01-01
Henrik Forssell , Peter LeFanu Lumsdaine
Classically, any structure for a signature Σ may be completed to a model of a desired regular theory T by means of the chase construction or small object argument. Moreover, … Classically, any structure for a signature Σ may be completed to a model of a desired regular theory T by means of the chase construction or small object argument. Moreover, this exhibits Mod(T) as weakly reflective in Str(Σ). We investigate this in the constructive setting. The basic construction is unproblematic, however, it is no longer a weak reflection. Indeed, we show that various reflection principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e. set) models. Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations

2018-10-30
Peter LeFanu Lumsdaine , Nicolas Tabareau
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.

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

2016-01-01
Andrej Bauer , Jason N. 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

Special issue on homotopy type theory 2019

2021-11-01
Daniel R. Licata , Peter LeFanu Lumsdaine
An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also … An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also available in through the ‘Save PDF’ action button.
View PDF Chat

Special issue on homotopy type theory 2019 vol. 2

2023-09-01
Daniel R. Licata , Peter LeFanu Lumsdaine
An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also … An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also available in through the ‘Save PDF’ action button.
View PDF Chat

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

2024-10-28
Benedikt Ahrens , Peter LeFanu Lumsdaine , Paige Randall North
View PDF Chat

Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

2024-10-28
Benedikt Ahrens , Peter LeFanu Lumsdaine , Paige Randall North
View PDF Chat

Special issue on homotopy type theory 2019 vol. 2

2023-09-01
Daniel R. Licata , Peter LeFanu Lumsdaine
An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also … An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also available in through the ‘Save PDF’ action button.
View PDF Chat

Special issue on homotopy type theory 2019

2021-11-01
Daniel R. Licata , Peter LeFanu Lumsdaine
An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also … An abstract is not available for this content. As you have access to this content, full HTML content is provided on this page. A PDF of this content is also available in through the ‘Save PDF’ action button.
View PDF Chat

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

Homotopical inverse diagrams in categories with attributes

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

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

2020-09-03
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.

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.

A general definition of dependent type theories

2020-01-01
Andrej Bauer , Philipp G. Haselwarter , Peter LeFanu Lumsdaine
We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing … We define a general class of dependent type theories, encompassing Martin-Löf's intuitionistic type theories and variants and extensions. The primary aim is pragmatic: to unify and organise their study, allowing results and constructions to be given in reasonable generality, rather than just for specific theories. Compared to other approaches, our definition stays closer to the direct or naive reading of syntax, yielding the traditional presentations of specific theories as closely as possible. Specifically, we give three main definitions: raw type theories, a minimal setup for discussing dependently typed derivability; acceptable type theories, including extra conditions ensuring well-behavedness; and well-presented type theories, generalising how in traditional presentations, the well-behavedness of a type theory is established step by step as the type theory is built up. Following these, we show that various fundamental fitness-for-purpose metatheorems hold in this generality. Much of the present work has been formalised in the proof assistant Coq.

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

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

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

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations

2018-10-30
Peter LeFanu Lumsdaine , Nicolas Tabareau
View PDF Chat

The homotopy theory of type theories

2018-08-30
Krzysztof Kapulkin , Peter LeFanu Lumsdaine
View PDF Chat

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.

Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341).

2018-01-01
Andrej Bauer , Martı́n Hötzel Escardó , Peter LeFanu Lumsdaine +1 more

Homotopical inverse diagrams in categories with attributes

2018-01-01
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.

Displayed Categories

2017-09-03
Benedikt Ahrens , Peter LeFanu Lumsdaine
View PDF Chat

Parametricity, automorphisms of the universe, and excluded middle

2017-06-27
Auke Bart Booij , Martı́n Hötzel Escardó , Peter LeFanu Lumsdaine +1 more
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific … It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instan ...

Displayed Categories

2017-01-01
Benedikt Ahrens , Peter LeFanu Lumsdaine
We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but … We introduce and develop the notion of *displayed categories*. A displayed category over a category C is equivalent to "a category D and functor F : D --> C", but instead of having a single collection of "objects of D" with a map to the objects of C, the objects are given as a family indexed by objects of C, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.
View PDF Chat

Categorical structures for type theory in univalent foundations

2017-01-01
Benedikt Ahrens , Peter LeFanu Lumsdaine , Vladimir Voevodsky
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps … In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.
View PDF Chat

Parametricity, automorphisms of the universe, and excluded middle

2017-01-01
Auke Bart Booij , Martı́n Hötzel Escardó , Peter LeFanu Lumsdaine +1 more
It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific … It is known that one can construct non-parametric functions by assuming classical axioms. Our work is a converse to that: we prove classical axioms in dependent type theory assuming specific instances of non-parametricity. We also address the interaction between classical axioms and the existence of automorphisms of a type universe. We work over intensional Martin-Löf dependent type theory, and in some results assume further principles including function extensionality, propositional extensionality, propositional truncation, and the univalence axiom.

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

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

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

The homotopy theory of type theories

2016-09-30
Chris Kapulkin , Peter LeFanu Lumsdaine
We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is … We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.

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

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

Constructive reflection principles for regular theories

2016-01-01
Henrik Forssell , Peter LeFanu Lumsdaine
Classically, any structure for a signature Σ may be completed to a model of a desired regular theory T by means of the chase construction or small object argument. Moreover, … Classically, any structure for a signature Σ may be completed to a model of a desired regular theory T by means of the chase construction or small object argument. Moreover, this exhibits Mod(T) as weakly reflective in Str(Σ). We investigate this in the constructive setting. The basic construction is unproblematic, however, it is no longer a weak reflection. Indeed, we show that various reflection principles for models of regular theories are equivalent to choice principles in the ambient set theory. However, the embedding of a structure into its chase-completion still satisfies a conservativity property, which suffices for applications such as the completeness of regular logic with respect to Tarski (i.e. set) models. Unlike most constructive developments of predicate logic, we do not assume that equality between symbols in the signature is decidable. While in this setting, we also give a version of one classical lemma which is trivial over discrete signatures but more interesting here: the abstraction of constants in a proof to variables.

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

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

The homotopy theory of type theories

2016-01-01
Chris Kapulkin , Peter LeFanu Lumsdaine
We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is … We construct a left semi-model structure on the category of intensional type theories (precisely, on $\mathrm{CxlCat_{Id,1,\Sigma(,\Pi_{ext})}}$). This presents an $\infty$-category of such type theories; we show moreover that there is an $\infty$-functor $\mathrm{Cl}_\infty$ from there to the $\infty$-category of suitably structured quasi-categories. This allows a precise formulation of the conjectures that intensional type theory gives internal languages for higher categories, and provides a framework and toolbox for further progress on these conjectures.
View PDF Chat

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

2016-01-01
Andrej Bauer , Jason N. 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

The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories

2015-07-04
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

The Local Universes Model

2015-07-04
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

Homotopy limits in type theory

2015-01-19
Jeremy Avigad , Krzysztof Kapulkin , Peter LeFanu Lumsdaine
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed … Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.
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

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.

Quipper

2013-06-16
Alexander S. Green , Peter LeFanu Lumsdaine , Neil J. Ross +2 more
The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level … The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and can generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.
View PDF Chat

Homotopy limits in Coq

2013-04-02
Jeremy Avigad , Krzysztof Kapulkin , Peter LeFanu Lumsdaine

On the Bourbaki–Witt principle in toposes

2013-03-18
Andrej Bauer , Peter LeFanu Lumsdaine
The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and … The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Among other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not imply that fixed points can always be found by transfinite iteration. Meanwhile, on the side of models, we see that the principle fails in realisability toposes, and does not hold in the free topos, but does hold in all cocomplete toposes.
View PDF Chat

An Introduction to Quantum Programming in Quipper

2013-01-01
Alexander S. Green , Peter LeFanu Lumsdaine , Neil J. Ross +2 more
View PDF Chat

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01
Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
View PDF Chat

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.

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.

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.

Weak omega-categories from intensional type theory

2010-09-17
Peter LeFanu Lumsdaine
We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. … We show that for any type in Martin-L\"of Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.
View PDF Chat

Lawvere–Tierney sheaves in Algebraic Set Theory

2009-06-16
Steve Awodey , Nicola Gambino , Peter LeFanu Lumsdaine +1 more
We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that … We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.
View PDF Chat

A Small Observation on Co-categories

2009-01-01
Peter LeFanu Lumsdaine
Various concerns suggest looking for internal co-categories in categories with strong logical structure. It turns out that in any coherent category, all co-categories are co-equivalence relations. Various concerns suggest looking for internal co-categories in categories with strong logical structure. It turns out that in any coherent category, all co-categories are co-equivalence relations.

Weak ω-Categories from Intensional Type Theory

2009-01-01
Peter LeFanu Lumsdaine
Coauthor Papers Together
Chris Kapulkin 11
Andrej Bauer 7
Krzysztof Kapulkin 6
Michael Shulman 5
Daniel R. Licata 5
Benedikt Ahrens 5
Vladimir Voevodsky 4
Matthieu Sozeau 4
Bas Spitters 4
Martı́n Hötzel Escardó 4
Michael A. Warren 4
Kuen-Bang Hou 3
Jeremy Avigad 3
Eric Finster 3
Assia Mahboubi 2
Steve Awodey 2
Nicola Gambino 2
Auke Bart Booij 2
Alexander S. Green 2
Jason Gross 2
Neil J. Ross 2
Benoît Valiron 2
Peter Selinger 2
Michael Nahas 1
Hugo Herbelin 1
Philip Scott 1
Bruno Barras 1
Álvaro Pelayo 1
Henrik Forssell 1
André Joyal 1
Paige Randall North 1
Georges Gonthier 1
Guillaume Brunerie 1
Carlo Angiuli 1
Kristina Sojakova 1
Egbert Rijke 1
Thierry Coquand 1
Zhaohui Luo 1
Nuo Li 1
Martin Hofmann 1
Robert L. Constable 1
Cyril Cohen 1
Dana Scott 1
M.A. Warren 1
Sergei Soloviev 1
Pierre-Louis Curien 1
Thomas Hales 1
Mike Shulman 1
Per Martin-Löf 1
Marc Bezem 1

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

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 identity type weak factorisation system

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

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.

Types are weak <i>ω</i> -groupoids

2010-10-12
Benno van den Berg , Richard Garner
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower … We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.
View PDF Chat

Comprehension categories and the semantics of type dependency

1993-01-01
Bart Jacobs

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.

Two-dimensional models of type theory

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

The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories

2015-07-04
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

Abstract homotopy theory and generalized sheaf cohomology

1973-01-01
Kenneth S. Brown
Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kan’s category of spectra. These groups generalize the ordinary … Cohomology groups ${H^q}(X,E)$ are defined, where X is a topological space and E is a sheaf on X with values in Kan’s category of spectra. These groups generalize the ordinary cohomology groups of X with coefficients in an abelian sheaf, as well as the generalized cohomology of X in the usual sense. The groups are defined by means of the “homotopical algebra” of Quillen applied to suitable categories of sheaves. The study of the homotopy category of sheaves of spectra requires an abstract homotopy theory more general than Quillen’s, and this is developed in Part I of the paper. Finally, the basic cohomological properties are proved, including a spectral sequence which generalizes the Atiyah-Hirzebruch spectral sequence (in generalized cohomology theory) and the “local to global” spectral sequence (in sheaf cohomology theory).
View PDF Chat

On the strength of dependent products in the type theory of Martin-Löf

2009-02-02
Richard Garner
View PDF Chat

Topological and Simplicial Models of Identity Types

2012-01-01
Benno van den Berg , Richard Garner
In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do … In this paper we construct new categorical models for the identity types of Martin-Löf type theory, in the categories Top of topological spaces and SSet of simplicial sets. We do so building on earlier work of Awodey and Warren [2009], which has suggested that a suitable environment for the interpretation of identity types should be a category equipped with a weak factorization system in the sense of Bousfield--Quillen. It turns out that this is not quite enough for a sound model, due to some subtle coherence issues concerned with stability under substitution; and so our first task is to introduce a slightly richer structure, which we call a homotopy-theoretic model of identity types , and to prove that this is sufficient for a sound interpretation. Now, although both Top and SSet are categories endowed with a weak factorization system---and indeed, an entire Quillen model structure---exhibiting the additional structure required for a homotopy-theoretic model is quite hard to do. However, the categories we are interested in share a number of common features, and abstracting these leads us to introduce the notion of a path object category . This is a relatively simple axiomatic framework, which is nonetheless sufficiently strong to allow the construction of homotopy-theoretic models. Now by exhibiting suitable path object structures on Top and SSet , we endow those categories with the structure of a homotopy-theoretic model and, in this way, obtain the desired topological and simplicial models of identity types.
View PDF Chat

On the interpretation of type theory in locally cartesian closed categories

1995-01-01
Martin Hofmann

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 .

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

Revisiting the categorical interpretation of dependent type theory

2014-03-06
Pierre-Louis Curien , Richard Garner , Martin Hofmann
We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian … We show that Hofmann's and Curien's interpretations of Martin-Löf's type theory, which were both designed to cure a mismatch between syntax and semantics in Seely's original interpretation in locally cartesian closed categories, are related via a natural isomorphism. As an outcome, we obtain a new proof of the coherence theorem needed to show the soundness after all of Seely's interpretation.

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

Cofibrations in Homotopy Theory

2006-01-01
Andrei Rădulescu-Banu
We define Anderson-Brown-Cisinski (ABC) cofibration categories, and construct homotopy colimits of diagrams of objects in ABC cofibration categories. Homotopy colimits for Quillen model categories are obtained as a particular case. … We define Anderson-Brown-Cisinski (ABC) cofibration categories, and construct homotopy colimits of diagrams of objects in ABC cofibration categories. Homotopy colimits for Quillen model categories are obtained as a particular case. We attach to each ABC cofibration category a left Heller derivator. A dual theory is developed for homotopy limits in ABC fibration categories and for right Heller derivators. These constructions provide a natural framework for 'doing homotopy theory' in ABC (co)fibration categories.

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01
Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of … Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
View PDF Chat

Quantum Gauge Field Theory in Cohesive Homotopy Type Theory

2014-07-29
Urs Schreiber , Michael Shulman
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as … We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theory. This is a brief survey of work by the authors developed in detail elsewhere.
View PDF Chat

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

Homotopy limits in type theory

2015-01-19
Jeremy Avigad , Krzysztof Kapulkin , Peter LeFanu Lumsdaine
Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed … Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to the formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories.
View PDF Chat

Weak ω-Categories from Intensional Type Theory

2009-01-01
Peter LeFanu Lumsdaine

Two Models for the Homotopy Theory of Cocomplete Homotopy Theories

2014-08-06
Karol Szumiło
We prove that the homotopy theory of cofibration categories is equivalent to the homotopy theory of cocomplete quasicategories. This is achieved by presenting both homotopy theories as fibration categories and … We prove that the homotopy theory of cofibration categories is equivalent to the homotopy theory of cocomplete quasicategories. This is achieved by presenting both homotopy theories as fibration categories and constructing an explicit equivalence between them.

Homotopy Limit Functors on Model Categories and Homotopical Categories

2005-08-22
William Dwyer , Philip Hirschhorn , Daniel M. Kan +1 more
Model categories: An overview Model categories and their homotopy categories Quillen functors Homotopical cocompleteness and completeness of model categories Homotopical categories: Summary of part II Homotopical categories and homotopical functors … Model categories: An overview Model categories and their homotopy categories Quillen functors Homotopical cocompleteness and completeness of model categories Homotopical categories: Summary of part II Homotopical categories and homotopical functors Deformable functors and their approximations Homotopy colimit and limit functors and homotopical ones Index Bibliography.
View PDF Chat

Eilenberg-MacLane spaces in homotopy type theory

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

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.

Simplicial Homotopy Theory

2009-01-01
Paul G. Goerss , John F. Jardine
Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c
View PDF Chat

Wellfounded trees in categories

2000-07-01
Ieke Moerdijk , Erik Palmgren

Inductive Types in Homotopy Type Theory

2012-06-01
Steve Awodey , Nicola Gambino , Kristina Sojakova
Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional … Homotopy type theory is an interpretation of Martin-Lof's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.
View PDF Chat

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

2013-06-01
Daniel R. Licata , Michael Shulman
Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new … Recent work on homotopy type theory exploits an exciting new correspondence between Martin-Lof's dependent type theory and the mathematical disciplines of category theory and homotopy theory. The mathematics suggests new principles to add to type theory, while the type theory can be used in novel ways to do computer-checked proofs in a proof assistant. In this paper, we formalize a basic result in algebraic topology, that the fundamental group of the circle is the integers. Our proof illustrates the new features of homotopy type theory, such as higher inductive types and Voevodsky's univalence axiom. It also introduces a new method for calculating the path space of a type, which has proved useful in many other examples.
View PDF Chat

Strong stacks and classifying spaces

1991-01-01
André Joyal , Myles Tierney

Univalence for inverse EI diagrams

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

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

Homotopy-Theoretic Models of Type Theory

2011-01-01
Peter Arndt , Krzysztof Kapulkin
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

The biequivalence of locally cartesian closed categories and Martin-Löf type theories

2014-04-29
Pierre Clairambault , Peter Dybjer
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category … Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L\"of type theories with Pi-types, Sigma-types and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the B\'enabou-Hofmann interpretation of Martin-L\"of type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-L\"of type theories. As a second result we prove that if we remove Pi-types the resulting categories with families are biequivalent to left exact categories.
View PDF Chat

Homomorphisms of higher categories

2010-03-05
Richard Garner
View PDF Chat

A Cubical Approach to Synthetic Homotopy Theory

2015-07-01
Daniel R. Licata , Guillaume Brunerie
Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe … Homotopy theory can be developed synthetically in homotopy type theory, using types to describe spaces, the identity type to describe paths in a space, and iterated identity types to describe higher-dimensional paths.While some aspects of homotopy theory have been developed synthetically and formalized in proof assistants, some seemingly easy examples have proved difficult because the required manipulations of paths becomes complicated.In this paper, we describe a cubical approach to developing homotopy theory within type theory.The identity type is complemented with higher-dimensional cube types, such as a type of squares, dependent on four points and four lines, and a type of three-dimensional cubes, dependent on the boundary of a cube.Path-over-a-path types and higher generalizations are used to describe cubes in a fibration over a cube in the base.These higher-dimensional cube and path-over types can be defined from the usual identity type, but isolating them as independent conceptual abstractions has allowed for the formalization of some previously difficult examples.
View PDF Chat

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

Type theories, toposes and constructive set theory: predicative aspects of AST

2002-04-01
Ieke Moerdijk , Erik Palmgren
View PDF Chat

Univalence in locally cartesian closed infinity-categories

2012-01-01
David Gepner , Joachim Kock
After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed infinity-categories, we establish the representability of equivalences and show that univalent families, in the sense of … After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed infinity-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 infinity-topos has a hierarchy of "universal" univalent families, indexed by regular cardinals, and that n-topoi have univalent families classifying (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 infinity-quasitopoi (certain infinity-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 (n-2)-truncated, as well as some univalent families in the Morel--Voevodsky infinity-category of motivic spaces, an instance of a locally cartesian closed infinity-category which is not an n-topos for any $0\leq n\leq\infty$. Lastly, we show that any presentable locally cartesian closed infinity-category is modeled by a combinatorial type-theoretic model category, and conversely that the infinity-category underlying a combinatorial type-theoretic model category is presentable and locally cartesian closed. Under this correspondence, univalent families in presentable locally cartesian closed infinity-categories correspond to univalent fibrations in combinatorial type-theoretic model categories.

Higher Operads, Higher Categories

2004-07-22
Tom Leinster
Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical … Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. The heart of this book is the language of generalized operads. This is as natural and transparent a language for higher category theory as the language of sheaves is for algebraic geometry, or vector spaces for linear algebra. It is introduced carefully, then used to give simple descriptions of a variety of higher categorical structures. In particular, one possible definition of n-category is discussed in detail, and some common aspects of other possible definitions are established. This is the first book on the subject and lays its foundations. It will appeal to both graduate students and established researchers who wish to become acquainted with this modern branch of mathematics.
View PDF Chat

Categories for the Working Mathematician

1971-01-01
Saunders Mac Lane
View PDF Chat

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

Operads, Algebras and Modules in General Model Categories

2001-01-01
Markus Spitzweck
In this paper we develop the theory of operads, algebras and modules in cofibrantly generated symmetric monoidal model categories. We give J-semi model strucures, which are a slightly weaker version … In this paper we develop the theory of operads, algebras and modules in cofibrantly generated symmetric monoidal model categories. We give J-semi model strucures, which are a slightly weaker version of model structures, for operads and algebras and model structures for modules. In a second part we develop the thoery of S-modules of [EKMM]., which allows a general homotopy theory for commutative algebras and pseudo unital symmetric monoidal categories of modules over them. Finally we prove a base change and projection formula.

Some free constructions in realizability and proof theory

1995-09-01
A. Carboni

The petit topos of globular sets

2000-12-01
Ross Street

A characterization of simplicial localization functors and a discussion of DK equivalences

2012-01-28
Clark Barwick , D Kan

On the algebraic<i>K</i>-theory of higher categories

2016-01-12
Clark Barwick
We prove that Waldhausen K-theory, when extended to a very general class of quasicategories, can be described as a Goodwillie differential. In particular, K-theory spaces admit canonical (connective) deloopings, and … We prove that Waldhausen K-theory, when extended to a very general class of quasicategories, can be described as a Goodwillie differential. In particular, K-theory spaces admit canonical (connective) deloopings, and the K-theory functor enjoys a simple universal property. Using this, we give new, higher categorical proofs of the approximation, additivity, and fibration theorems of Waldhausen in this article. As applications of this technology, we study the algebraic K-theory of associative rings in a wide range of homotopical contexts and of spectral Deligne–Mumford stacks.
View PDF Chat