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

DOI10.4115/jla.2016.8.1zbMath1403.03124arXiv1409.1829OpenAlexW3105622746MaRDI QIDQ2974664

Andrew Swan

Publication date: 10 April 2017

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

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

zbMATH Keywords

constructive mathematicstype theorynominal setscubical setsalgebraic weak factorisation systems

Mathematics Subject Classification ID

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

Related Items (10)

Canonicity and homotopy canonicity for cubical type theory ⋮ Unnamed Item ⋮ Cubical Type Theory: a constructive interpretation of the univalence axiom ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Free functor from the category of \(G\)-nominal sets to that of 01-\(G\)-nominal sets ⋮ The univalence axiom in cubical sets ⋮ Unnamed Item ⋮ Model structure on the universe of all types in interval type theory ⋮ Syntax and models of Cartesian cubical type theory

Cites Work

• Understanding the small object argument
• Unnamed Item

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