Exact completion of path categories and algebraic set theory. I: Exact completion of path categories

DOI10.1016/J.JPAA.2017.11.017zbMATH Open1420.18034arXiv1603.02456OpenAlexW2962800673MaRDI QIDQ1748403FDOQ1748403

Authors: Benno van den Berg, Ieke Moerdijk 

Publication date: 11 May 2018

Published in: Journal of Pure and Applied Algebra (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1603.02456

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

zbMATH Keywords

exact completionhomotopy theorypath objectconstructive set theorycategory with fibrant objects

Mathematics Subject Classification ID

Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Regular and exact completions
• Homotopical algebra
• Rational homotopy theory
• Setoids in type theory
• Title not available (Why is that?)
• Univalence in locally Cartesian closed categories
• Introduction to extensive and distributive categories
• Homotopy theoretic models of identity types
• The identity type weak factorisation system
• Title not available (Why is that?)
• Abstract homotopy theory and generalized sheaf cohomology
• Locally cartesian closed exact completions
• Some free constructions in realizability and proof theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• Quasicategories of frames of cofibration categories
• Extensional Constructs in Intensional Type Theory
• Univalence for inverse diagrams and homotopy canonicity
• The univalence axiom for elegant Reedy presheaves
• When do completion processes give rise to extensive categories?
• Title not available (Why is that?)
• Homotopy limits in type theory
• Path Categories and Propositional Identity Types

Cited In (10)

• Homotopy theory of cofibration categories
• A characterisation of elementary fibrations
• The effective model structure and -groupoid objects
• Quotients, pure existential completions and arithmetic universes
• The derivator of setoids
• EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS
• Title not available (Why is that?)
• W-types in setoids
• Univalent polymorphism
• The two out of three property in ind-categories and a convenient model category of spaces

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)