Krzysztof Kapulkin

Search for another author

Author Description

Ask a Question About This Mathematician

All published works (24)

Synthetic approach to the Quillen model structure on topological spaces

2025-05-16

Sterling Ebel , Krzysztof Kapulkin

The fundamental group in discrete homotopy theory

2025-01-06

Krzysztof Kapulkin , Udit Mavinkurve

Extensional concepts in intensional type theory, revisited

2025-01-01

Krzysztof Kapulkin , Yufeng Li

Chat View PDF

Cubical Models of (∞,1)-Categories

2024-05-01

Brandon Doherty , Krzysztof Kapulkin , Zachery Lindsey +1 more

We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with … We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We show that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor. As an application, we show that cubical quasicategories admit a convenient notion of a mapping space, which we use to characterize the weak equivalences between fibrant objects in our model structure as DK-equivalences.

Cofibration category of digraphs for path homology

2024-04-29

Daniel Carranza , Brandon Doherty , Krzysztof Kapulkin +3 more

We prove that the category of directed graphs and graph maps carries a cofibration category structure in which the weak equivalences are the graph maps inducing isomorphisms on path homology. We prove that the category of directed graphs and graph maps carries a cofibration category structure in which the weak equivalences are the graph maps inducing isomorphisms on path homology.

Chat View PDF

The Hurewicz theorem for cubical homology

2023-10-30

Daniel Carranza , Krzysztof Kapulkin , Andrew Tonks

Chat View PDF

Homotopy groups of cubical sets

2023-10-07

Daniel Carranza , Krzysztof Kapulkin

Chat View PDF

Nonexistence of Colimits in Naive Discrete Homotopy Theory

2023-09-27

Daniel Carranza , Krzysztof Kapulkin , Jinho Kim

Equivalence of cubical and simplicial approaches to (∞,n)-categories

2023-02-09

Brandon Doherty , Krzysztof Kapulkin , Yuki Maehara

Extensional Concepts in Intensional Type Theory, Revisited

2023-01-01

Krzysztof Kapulkin , Yufeng Li

Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory … Revisiting a classic result from M. Hofmann's dissertation, we give a direct proof of Morita equivalence, in the sense of V. Isaev, between extensional type theory and intensional type theory extended by the principles of functional extensionality and of uniqueness of identity proofs.

Chat View PDF

The simplicial model of Univalent Foundations (after Voevodsky)

2021-03-08

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky’s construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky’s construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Löf type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

Chat View PDF

A cubical approach to straightening

2020-10-23

Krzysztof Kapulkin , Vladimir Voevodsky

For a suitable choice of the cube category, we construct a Grothendieck topology on it such that sheaves with respect to this topology are exactly simplicial sets (thus establishing simplicial … For a suitable choice of the cube category, we construct a Grothendieck topology on it such that sheaves with respect to this topology are exactly simplicial sets (thus establishing simplicial sets as a reflective subcategory of cubical sets). We then extend the construction of the homotopy coherent nerve to cubical categories and establish an analogue of Lurie's straightening–unstraightening construction.

Homotopical inverse diagrams in categories with attributes

2020-09-09

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

Internal languages of finitely complete $$(\infty , 1)$$ ( ∞ , 1 ) -categories

2019-04-27

Krzysztof Kapulkin , Karol Szumiło

Chat View PDF

The homotopy theory of type theories

2018-08-30

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

Threshold Properties of Prime Power Subgroups with Application to Secure Integer Comparisons.

2018-01-01

Rhys Carlton , Aleksander Essex , Krzysztof Kapulkin

We present a semantically secure somewhat homomorphic public-key cryptosystem working in sub-groups of $\mathbb {Z}_{n}^{*}$ of prime power order. Our scheme introduces a novel threshold homomorphic property, which we use … We present a semantically secure somewhat homomorphic public-key cryptosystem working in sub-groups of $\mathbb {Z}_{n}^{*}$ of prime power order. Our scheme introduces a novel threshold homomorphic property, which we use to build a two-party protocol for secure integer comparison. In contrast to related work which encrypts and acts on each bit of the input separately, our protocol compares multiple input bits simultaneously within a single ciphertext. Compared to the related protocol of Damgard et al. [9, 10] we present results showing this approach to be both several times faster in computation and lower in communication complexity.

Locally cartesian closed quasi‐categories from type theory

2017-11-06

Krzysztof Kapulkin

We prove that the quasi-categories arising from models of Martin-Löf type theory via simplicial localization are locally cartesian closed. We prove that the quasi-categories arising from models of Martin-Löf type theory via simplicial localization are locally cartesian closed.

Chat View PDF

Quasicategories of Frames of Cofibration Categories

2016-02-20

Krzysztof Kapulkin , Karol Szumiło

Chat View PDF

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

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

Chat View PDF

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.

Chat View PDF

Univalent Categories and the Rezk Completion

2015-01-01

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

Chat View PDF

THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

2014-01-01

Krzysztof Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky

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

Chat View PDF

Homotopy limits in Coq

2013-04-02

Jeremy Avigad , Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

Homotopy-Theoretic Models of Type Theory

2011-01-01

Peter Arndt , Krzysztof Kapulkin

Chat View PDF

Common Coauthors

Coauthor	Papers Together
Peter LeFanu Lumsdaine	6
Daniel Carranza	4
Brandon Doherty	3
Michael Shulman	2
Benedikt Ahrens	2
Vladimir Voevodsky	2
Karol Szumiło	2
Jeremy Avigad	2
Yufeng Li	2
Christian Sattler	1
Morgan Opie	1
Peter Arndt	1
Maru Sarazola	1
Udit Mavinkurve	1
Zachery Lindsey	1
Liang Ze Wong	1
Sterling Ebel	1
Jinho Kim	1
Aleksander Essex	1
Rhys Carlton	1
Andrew Tonks	1
Yuki Maehara	1

Commonly Cited References

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

Chat View PDF

Homotopy limits in type theory

2015-01-19

Jeremy Avigad , Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

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.

Chat View PDF

The identity type weak factorisation system

2008-09-03

Nicola Gambino , Richard Garner

Chat View PDF

Univalence for inverse diagrams and homotopy canonicity

2014-11-24

Michael Shulman

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

Chat View PDF

Two-dimensional models of type theory

2009-07-02

Richard Garner

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

Chat View PDF

Homotopy theoretic models of identity types

2008-07-14

Steve Awodey , Michael A. Warren

This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing … This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.

Chat View PDF

Quasicategories of Frames of Cofibration Categories

2016-02-20

Krzysztof Kapulkin , Karol Szumiło

Chat View PDF

Types are weak ω -groupoids

2010-10-12

Benno van den Berg , Richard Garner

We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower … We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.

Chat View PDF

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

Chat View PDF

Homotopy theory of graphs

2006-07-01

Eric Babson , Hélène Barcelo , Mark de Longueville +1 more

Chat View PDF

Simplicial Homotopy Theory

1999-01-01

Paul G. Goerss , John F. Jardine

Chat View PDF

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.

Chat View PDF

Homotopical Algebra

1967-01-01

Daniel Quillen

Chat View PDF

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.

Chat View PDF

Two Models for the Homotopy Theory of Cocomplete Homotopy Theories

2014-01-01

Karol Szumiło

Chat View PDF

The homotopy theory of type theories

2018-08-30

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

Higher Topos Theory (AM-170)

2009-12-31

Jacob Lurie

Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are … Higher category theory is generally regarded as technical and forbidding, but part of it is considerably more tractable: the theory of infinity-categories, higher categories in which all higher morphisms are assumed to be invertible. In Higher Topos Theory , Jacob Lurie presents the foundations of this theory, using the language of weak Kan complexes introduced by Boardman and Vogt, and shows how existing theorems in algebraic topology can be reformulated and generalized in the theory's new language. The result is a powerful theory with applications in many areas of mathematics. The book's first five chapters give an exposition of the theory of infinity-categories that emphasizes their role as a generalization of ordinary categories. Many of the fundamental ideas from classical category theory are generalized to the infinity-categorical setting, such as limits and colimits, adjoint functors, ind-objects and pro-objects, locally accessible and presentable categories, Grothendieck fibrations, presheaves, and Yoneda's lemma. A sixth chapter presents an infinity-categorical version of the theory of Grothendieck topoi, introducing the notion of an infinity-topos, an infinity-category that resembles the infinity-category of topological spaces in the sense that it satisfies certain axioms that codify some of the basic principles of algebraic topology. A seventh and final chapter presents applications that illustrate connections between the theory of higher topoi and ideas from classical topology.

Homotopy Type Theory: Univalent Foundations of Mathematics

2013-01-01

Peter Aczel , Benedikt Ahrens , Thorsten Altenkirch +7 more

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

Chat View PDF

The Simplicial Model of Univalent Foundations (after Voevodsky)

2012-11-12

Chris Kapulkin , Peter LeFanu Lumsdaine

We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models … We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in our model. As a corollary, we conclude that Martin-Lof type theory with one univalent universe (formulated in terms of contextual categories) is at least as consistent as ZFC with two inaccessible cardinals.

Chat View PDF

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

2009-01-01

Georges Maltsiniotis

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

Chat View PDF

A model for the homotopy theory of homotopy theory

2000-06-20

Charles Rezk

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

Calculus of Fractions and Homotopy Theory

1967-01-01

Peter Gabriel , Michel Zisman

Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory

2011-09-04

Steve Awodey , Richard Garner , Per Martin-Löf +1 more

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

Chat View PDF

THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS

2014-01-01

Krzysztof Kapulkin , Peter LeFanu Lumsdaine , Vladimir Voevodsky

Chat View PDF

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

2009-02-02

Richard Garner

Chat View PDF

Frames in cofibration categories

2016-07-13

Karol Szumiło

Chat View PDF

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.

Chat View PDF

Hom complexes and homotopy theory in the category of graphs

2008-06-26

Anton Dochtermann

Chat View PDF

Pull-Backs in Homotopy Theory

1976-04-01

Michael Mather

The (based) homotopy category consists of (based) topological spaces and (based) homotopy classes of maps. In these categories, pull-backs and push-outs do not generally exist. For example, no essential map … The (based) homotopy category consists of (based) topological spaces and (based) homotopy classes of maps. In these categories, pull-backs and push-outs do not generally exist. For example, no essential map between Eilenberg-MacLane spaces of different dimensions has a kernel. In this paper we define homotopy pull-backs and push-outs, which do exist and which behave like pull-backs and push-outs, and we give some of their properties. Applications may be found in [ 3 ; 5 ; 6 and 14 ].

Chat View PDF

Comprehension categories and the semantics of type dependency

1993-01-01

Bart Jacobs

Categorical homotopy theory

2006-01-01

John F. Jardine

This paper is an exposition of the ideas and methods of Cisinksi, in the context of A-presheaves on a small Grothendieck site, where A is an arbitrary test category in … This paper is an exposition of the ideas and methods of Cisinksi, in the context of A-presheaves on a small Grothendieck site, where A is an arbitrary test category in the sense of Grothendieck.The homotopy theory for the category of simplicial presheaves and each of its localizations can be modelled by A-presheaves in the sense that there is a corresponding model structure for A-presheaves with an equivalent homotopy category.The theory specializes, for example, to the homotopy theories of cubical sets and cubical presheaves, and gives a cubical model for motivic homotopy theory.The applications of Cisinski's ideas are explained in some detail for cubical sets.

Chat View PDF

Locally cartesian closed quasi‐categories from type theory

2017-11-06

Krzysztof Kapulkin

Chat View PDF

The simplicial model of Univalent Foundations (after Voevodsky)

2021-03-08

Krzysztof Kapulkin , Peter LeFanu Lumsdaine

Chat View PDF

Homotopy type theory and Voevodsky’s univalent foundations

2014-05-09

Álvaro Pelayo , Michael A. Warren

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

Chat View PDF

Univalent categories and the Rezk completion

2015-01-19

Benedikt Ahrens , Krzysztof Kapulkin , Michael Shulman

Chat View PDF

A co-reflection of cubical sets into simplicial sets with applications to model structures

2019-01-01

Chris Kapulkin , Zachery Lindsey , Liang Ze Wong

We show that the category of simplicial sets is a co-reflective subcategory of the category of cubical sets with connections, with the inclusion given by a version of the straightening … We show that the category of simplicial sets is a co-reflective subcategory of the category of cubical sets with connections, with the inclusion given by a version of the straightening functor. We show that using the co-reflector, one can transfer any cofibrantly generated model structure in which cofibrations are monomorphisms to cubical sets, thus obtaining cubical analogues of the Quillen and Joyal model structures.

Chat View PDF

A cubical approach to straightening

2020-10-23

Krzysztof Kapulkin , Vladimir Voevodsky

Vers une Axiomatisation de la Théorie des Catégories Supérieures

2005-03-01

Bertrand Toën

Chat View PDF

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.

Chat View PDF

Model Categories and Their Localizations

2009-08-24

Philip Hirschhorn

Localization of model category structures: Summary of part 1 Local spaces and localization The localization model category for spaces Localization of model categories Existence of left Bousfield localizations Existence of … Localization of model category structures: Summary of part 1 Local spaces and localization The localization model category for spaces Localization of model categories Existence of left Bousfield localizations Existence of right Bousfield localizations Fiberwise localization Homotopy theory in model categories: Summary of part 2 Model categories Fibrant and cofibrant approximations Simplicial model categories Ordinals, cardinals, and transfinite composition Cofibrantly generated model categories Cellular model categories Proper model categories The classifying space of a small category The Reedy model category structure Cosimplicial and simplicial resolutions Homotopy function complexes Homotopy limits in simplicial model categories Homotopy limits in general model categories Index Bibliography.

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

2012-01-28

Clark Barwick , D Kan

Foundations of a Connectivity Theory for Simplicial Complexes

2001-02-01

Hélène Barcelo , Xenia Kramer , Reinhard Laubenbacher +1 more

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 .

Quasi-categories vs Segal spaces

2007-01-01

André Joyal , Myles Tierney

We show that complete Segal spaces and Segal categories are Quillen equivalent to quasi-categories. We show that complete Segal spaces and Segal categories are Quillen equivalent to quasi-categories.

Chat View PDF

Cubical setting for discrete homotopy theory, revisited

2022-01-01

Daniel Carranza , Chris Kapulkin

We construct a functor associating a cubical set to a (simple) graph. We show that cubical sets arising in this way are Kan complexes, and that the A-groups of a … We construct a functor associating a cubical set to a (simple) graph. We show that cubical sets arising in this way are Kan complexes, and that the A-groups of a graph coincide with the homotopy groups of the associated Kan complex. We use this to prove a conjecture of Babson, Barcelo, de Longueville, and Laubenbacher from 2006, and a strong version of the Hurewicz theorem in discrete homotopy theory.

Chat View PDF

On the algebraicK-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.

Chat View PDF

On Semisimplicial Fibre-Bundles

1959-07-01

M. G. Barratt , V. K. A. M. Gugenheim , John C. Moore

Invariance de laK-Théorie par équivalences dérivées

2009-11-13

Denis-Charles Cisinski

Résumé Ces notes ont pour but de démontrer que tout foncteur exact à droite entre catégories de Waldhausen raisonnables, induisant une équivalence au niveau des catégories homotopiques, définit une équivalence … Résumé Ces notes ont pour but de démontrer que tout foncteur exact à droite entre catégories de Waldhausen raisonnables, induisant une équivalence au niveau des catégories homotopiques, définit une équivalence d'homotopie entre les spectres de K -théorie correspondants. Cela généralise un résultat bien connu de Thomason et Trobaugh. Les ingrédients de démonstration sont une généralisation du théorème d'approximation de Waldhausen et une caractérisation combinatoire simple des équivalences dérivées. On étudie par ailleurs la localisation simpliciale des catégories de Waldhausen. On démontre qu'un foncteur (homotopiquement) exact à droite induit une équivalence de catégories homotopiques si et seulement s'il induit une équivalence au niveau des localisations simpliciales. Cela permet de faire le lien avec la K -théorie des catégories simpliciales introduite par Toën et Vezzosi.

Chat View PDF

Perspectives on A-homotopy theory and its applications

2005-07-28

Hélène Barcelo , Reinhard Laubenbacher