Vicary abstract and references

We propose a new definition of quasistrict 4-category, and use it to prove that every weak adjunction of 1-morphisms in a semistrict 4-category can be promoted to a strong adjunction satisfying the butterfly equations (formalized proof available at We believe this to be the first nontrivial proof to be formulated in an algebraic 4-category. Our definition is simpler than some previous definitions, with many standard axioms of higher categories emerging instead as properties. Our definition is also amenable to computer formalization, and we introduce our new web-based proof assistant, GLOBULAR, which aims to make compositional proofs in higher category theory easy to construct and visualize.


Krzysztof Bar and Jamie Vicary (2016), "Data structures for quasistrict higher categories",


Krzysztof Bar, Aleks Kissinger and Jamie Vicary (2016), "Globular: an online proof assistant for higher-dimensional rewriting",

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

Postgraduate Taught:

Postgraduate Research:

Distance Learning Course  

Actuarial Science:

DL Study

Student complaints procedure

AccessAble 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.