An algebraic weak factorisation system on 01-substitution sets: a constructive proof

DOI10.4115/JLA.2016.8.1MaRDI QIDQ2974664zbMATH OpenOpenAlexFDO

Authors Andrew Swan

Publication date 10 April 2017

Published in Journal of Logic and Analysis (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

algebraic weak factorisation systemsconstructive mathematicscubical setsnominal setstype theory

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55) Constructive and recursive analysis (03F60) Factorization systems, substructures, quotient structures, congruences, amalgams (18A32) Eilenberg-Moore and Kleisli constructions for monads (18C20) Abstract and axiomatic homotopy theory in algebraic topology (55U35)

Abstract: We will construct an algebraic weak factorisation system on the category of 01 substitution sets such that the R-algebras are precisely the Kan fibrations together with a choice of Kan filling operation. The proof is based on Garner's small object argument for algebraic weak factorization systems. In order to ensure the proof is valid constructively, rather than applying the general small object argument, we give a direct proof based on the same ideas. We use this us to give an explanation why the J computation rule is absent from the original cubical set model and suggest a way to fix this.

Recommendations

• A cubical model of homotopy type theory
• An orthogonal approach to algebraic weak factorisation systems
• Algebraic weak factorisation systems. I: Accessible AWFS.
• The Frobenius condition, right properness, and uniform fibrations
• Algebraic weak factorisation systems. II: Categories of weak maps.

Cites work

• Natural weak factorization systems.
• Understanding the small object argument

Cited in

(16)

• Free functor from the category of G-nominal sets to that of 01-G-nominal sets
• A cubical model of homotopy type theory
• The Frobenius condition, right properness, and uniform fibrations
• The univalence axiom in cubical sets
• Cubical type theory: a constructive interpretation of the univalence axiom
• scientific article; zbMATH DE number 7003193 (Why is no real title available?)
• 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
• Homotopy canonicity for cubical type theory
• Cubical assemblies, a univalent and impredicative universe and a failure of propositional resizing
• scientific article; zbMATH DE number 7756115 (Why is no real title available?)
• Kripke-Joyal forcing for type theory and uniform fibrations
• The equivariant model structure on cartesian cubical sets
• Separating path and identity types in presheaf models of univalent type theory
• Algebraic weak factorisation systems. I: Accessible AWFS.

This page was built for publication: An algebraic weak factorisation system on 01-substitution sets: a constructive proof

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