Abstract Andrew Swan

Title: An Algebraic Weak Factorisation System on 01-Substitution Sets


Bezem, Coquand and Huber introduced the category of cubical sets as a
new model of homotopy type theory, which unlike simplicial sets can be
carried out in constructive mathematics.

Pitts then showed that the category of cubical sets is equivalent to
another category based on nominal sets; that of 01-substitution
sets. He also showed how the Bezem-Coquand-Huber definitions of Kan
fibration can be stated naturally in 01-substitution sets.

Algebraic weak factorisation systems (awfs's) are a variation of weak
factorisation system due to Grandis and Tholen. Whereas Kan fibrations
in simplicial sets are right maps in a wfs (cofibrantly generated by
horn inclusions), it is much more natural to view Kan fibrations in
01-substitution sets as right maps in an algebraic wfs, due to the
extra "uniformity conditions" in the definition of Kan fibration.

I will give a quick introduction to Pitt's category of 01-substitution
sets, including the definitions of nominal set, 01-substitution set
and Kan fibration. I will then give the definition of algebraic weak
factorisation system (awfs) and show how to define the awfs on
01-substitution sets as a cofibrantly generated awfs. Time permitting
I will sketch a proof that the special case of Garner's small object
argument for 01-substitution sets works constructively (whereas it is
unclear whether the general case of Garner's small object argument can
be made constructive). I will then use the awfs to give an explanation
why the computation rule for identity is absent in the original
cubical set model: there is no constructive proof that the
"reflexivity'' maps in the path objects are left maps in the awfs.

Share this page:

Contact details

Department of Mathematics
University of Leicester
University Road
Leicester LE1 7RH
United Kingdom

Tel.: +44 (0)116 229 7407

Campus Based Courses

Undergraduate: mathsug@le.ac.uk
Postgraduate Taught: mathspg@le.ac.uk

Postgraduate Research: pgrmaths@le.ac.uk

Distance Learning Course  

Actuarial Science:

DL Study

Student complaints procedure

DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has detailed accessibility guides for College House and the Michael Atiyah Building.