Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
From MaRDI portal
Publication:1748403
Abstract: We introduce the notion of a "category with path objects", as a slight strengthening of Kenneth Brown's classic notion of a "category of fibrant objects". We develop the basic properties of such a category and its associated homotopy category. Subsequently, we show how the exact completion of this homotopy category can be obtained as the homotopy category associated to a larger category with path objects, obtained by freely adjoining certain homotopy quotients. In a second part of this paper, we will present an application to models of constructive set theory. Although our work is partly motivated by recent developments in homotopy type theory, this paper is written purely in the language of homotopy theory and category theory, and we do not presuppose any familiarity with type theory on the side of the reader.
Recommendations
- The exact completion for regular categories enriched in posets
- The fullness axiom and exact completion of homotopy categories
- scientific article; zbMATH DE number 19484
- scientific article; zbMATH DE number 1247371
- scientific article; zbMATH DE number 1251511
- scientific article; zbMATH DE number 4138013
- The category of complete lattices as a category of algebras
- scientific article; zbMATH DE number 177183
- Exact completion and representations in abelian categories
- Idempotent completion of extriangulated categories
Cites work
- scientific article; zbMATH DE number 3927168 (Why is no real title available?)
- scientific article; zbMATH DE number 3754682 (Why is no real title available?)
- scientific article; zbMATH DE number 194040 (Why is no real title available?)
- scientific article; zbMATH DE number 1226952 (Why is no real title available?)
- scientific article; zbMATH DE number 1251511 (Why is no real title available?)
- scientific article; zbMATH DE number 3794304 (Why is no real title available?)
- scientific article; zbMATH DE number 2117177 (Why is no real title available?)
- Abstract homotopy theory and generalized sheaf cohomology
- Extensional Constructs in Intensional Type Theory
- Homotopical algebra
- Homotopy limits in type theory
- Homotopy theoretic models of identity types
- Introduction to extensive and distributive categories
- Locally cartesian closed exact completions
- Path categories and propositional identity types
- Quasicategories of frames of cofibration categories
- Rational homotopy theory
- Regular and exact completions
- Setoids in type theory
- Some free constructions in realizability and proof theory
- The identity type weak factorisation system
- The univalence axiom for elegant Reedy presheaves
- Univalence for inverse diagrams and homotopy canonicity
- Univalence in locally Cartesian closed categories
- When do completion processes give rise to extensive categories?
Cited in
(11)- Exact completion and constructive theories of sets
- The derivator of setoids
- The two out of three property in ind-categories and a convenient model category of spaces
- A characterisation of elementary fibrations
- On the homotopy hypothesis for 3-groupoids
- Univalent polymorphism
- Quotients, pure existential completions and arithmetic universes
- The effective model structure and \(\infty\)-groupoid objects
- The fullness axiom and exact completion of homotopy categories
- W-types in setoids
- Homotopy theory of cofibration categories
This page was built for publication: Exact completion of path categories and algebraic set theory. I: Exact completion of path categories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1748403)
