Richard Garner (Uppsala)

Factorisation axioms for type theory 

ABSTRACT: Though the type constructors of intensional type theory hint at
the presence of a weak factorisation system on its category of contexts,
they are not sufficiently strong to construct such. This can be fixed by
decree, by adding axioms for a weak factorisation system to our type theory.
We examine the consequences of doing this.