The Frobenius condition, right properness, and uniform fibrations
From MaRDI portal
Publication:2013548
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.
Recommendations
Cites work
- A homotopy-theoretic universal property of Leinster's operad for weak ω-categories
- Algebraic weak factorisation systems. I: Accessible AWFS.
- Axioms for modelling cubical type theory in a topos
- Constructions of factorization systems in categories
- Cubical type theory: a constructive interpretation of the univalence axiom
- Homomorphisms of higher categories
- Homotopical algebra
- Homotopy Type Theory
- scientific article; zbMATH DE number 6694181 (Why is no real title available?)
- scientific article; zbMATH DE number 1002289 (Why is no real title available?)
- scientific article; zbMATH DE number 19486 (Why is no real title available?)
- scientific article; zbMATH DE number 1216133 (Why is no real title available?)
- scientific article; zbMATH DE number 1226952 (Why is no real title available?)
- scientific article; zbMATH DE number 1860105 (Why is no real title available?)
- scientific article; zbMATH DE number 2117177 (Why is no real title available?)
- scientific article; zbMATH DE number 825864 (Why is no real title available?)
- scientific article; zbMATH DE number 3297895 (Why is no real title available?)
- scientific article; zbMATH DE number 3370546 (Why is no real title available?)
- Monoidal algebraic model structures
- Multitensor lifting and strictly unital higher category theory
- Natural weak factorization systems.
- Nominal presentation of cubical sets models of type theory
- Non-constructivity in Kan simplicial sets
- On the axioms for adhesive and quasiadhesive categories
- Polynomial functors and polynomial monads
- Presheaves as models for homotopy types
- Reedy categories and the \(\varTheta\)-construction
- Simplicial homotopy theory
- The identity type weak factorisation system
- The simplicial model of univalent foundations (after Voevodsky)
- The theory and practice of Reedy categories
- Topological and simplicial models of identity types
- Understanding the small object argument
Cited in
(34)- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017
- A cubical model of homotopy type theory
- Effective Kan fibrations in simplicial sets
- A characterisation of elementary fibrations
- On bifibrations of model categories
- Equipping weak equivalences with algebraic structure
- An orthogonal approach to algebraic weak factorisation systems
- An algebraic weak factorisation system on 01-substitution sets: a constructive proof
- A homotopy-theoretic model of function extensionality in the effective topos
- scientific article; zbMATH DE number 5504447 (Why is no real title available?)
- Cubical type theory: a constructive interpretation of the univalence axiom
- scientific article; zbMATH DE number 7003193 (Why is no real title available?)
- Internal universes in models of homotopy type theory
- Model structure on the universe of all types in interval type theory
- Syntax and models of Cartesian cubical type theory
- Canonicity and homotopy canonicity for cubical type theory
- Cubical methods in homotopy type theory and univalent foundations
- Homotopy canonicity for cubical type theory
- Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
- Simplicial sets inside cubical sets
- The effective model structure and \(\infty\)-groupoid objects
- MODELS OF MARTIN-LÖF TYPE THEORY FROM ALGEBRAIC WEAK FACTORISATION SYSTEMS
- From cubes to twisted cubes via graph morphisms in type theory
- On the ∞$\infty$‐topos semantics of homotopy type theory
- Towards a constructive simplicial model of Univalent Foundations
- Kripke-Joyal forcing for type theory and uniform fibrations
- A 2-categorical proof of Frobenius for fibrations defined from a generic point
- Examples and cofibrant generation of effective Kan fibrations
- Compatible weak factorization systems and model structures
- Frobenius structure and the Beck-Chevalley condition for algebraic weak factorization systems
- A short proof of the Frobenius property for generic fibrations
- The equivariant model structure on cartesian cubical sets
- Effective Kan fibrations for W-types in homotopy type theory
- Separating path and identity types in presheaf models of univalent type theory
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)
