The Frobenius condition, right properness, and uniform fibrations

DOI10.1016/J.JPAA.2017.02.013zbMATH Open1378.18002arXiv1510.00669OpenAlexW2528548943WikidataQ59886272 ScholiaQ59886272MaRDI QIDQ2013548FDOQ2013548

Nicola Gambino, Christian Sattler

Publication date: 8 August 2017

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

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

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

Recommendations

• Effective Kan fibrations in simplicial sets
• Weak model categories in classical and constructive mathematics
• An algebraic weak factorisation system on 01-substitution sets: a constructive proof
• Bifibrations and weak factorisation systems
• A cubical model of homotopy type theory

Mathematics Subject Classification ID

Factorization systems, substructures, quotient structures, congruences, amalgams (18A32) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Homotopical algebra
• Understanding the small object argument
• Simplicial homotopy theory
• Topological and Simplicial Models of Identity Types
• The identity type weak factorisation system
• Title not available (Why is that?)
• Title not available (Why is that?)
• Algebraic weak factorisation systems. I: Accessible AWFS.
• Title not available (Why is that?)
• Title not available (Why is that?)
• The theory and practice of Reedy categories
• Reedy categories and the \(\varTheta\)-construction
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the axioms for adhesive and quasiadhesive categories
• The simplicial model of univalent foundations (after Voevodsky)
• Polynomial functors and polynomial monads
• Monoidal algebraic model structures
• Constructions of factorization systems in categories
• Title not available (Why is that?)
• Multitensor lifting and strictly unital higher category theory
• A homotopy-theoretic universal property of Leinster's operad for weak ω-categories
• Homomorphisms of higher categories
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Title not available (Why is that?)
• Homotopy Type Theory
• Title not available (Why is that?)

Cited In (27)

• Title not available (Why is that?)
• A characterisation of elementary fibrations
• MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
• Model structure on the universe of all types in interval type theory
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
• Canonicity and homotopy canonicity for cubical type theory
• On the ∞$\infty$‐topos semantics of homotopy type theory
• Equipping weak equivalences with algebraic structure
• Title not available (Why is that?)
• Kripke-Joyal forcing for type theory and uniform fibrations
• The effective model structure and -groupoid objects
• A homotopy-theoretic model of function extensionality in the effective topos
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Title not available (Why is that?)
• Title not available (Why is that?)
• A 2-categorical proof of Frobenius for fibrations defined from a generic point
• Title not available (Why is that?)
• Cubical methods in homotopy type theory and univalent foundations
• Title not available (Why is that?)
• Simplicial sets inside cubical sets
• A cubical model of homotopy type theory
• Towards a constructive simplicial model of Univalent Foundations
• Compatible weak factorization systems and model structures
• Examples and cofibrant generation of effective Kan fibrations
• On bifibrations of model categories
• Syntax and models of Cartesian cubical type theory
• An orthogonal approach to algebraic weak factorisation systems

Uses Software

• cubicaltt

This page was built for publication: The Frobenius condition, right properness, and uniform fibrations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2013548)