PS: For now, we recommend you try it in Chrome, as for now there are some bugs when you use other browsers. On Sat, Dec 5, 2015 at 11:23 PM, Jamie Vicary <jamie.vicary@cs.ox.ac.uk> wrote:
Dear category theorists,
We're pleased to announce the launch of Globular, a web-based proof assistant for higher categories. It allows one to formalize higher-categorical proofs in finitely-presented n-categories, visualize them as string diagrams, and share them with collaborators, or with the world. It is available at this address:
Documentation is being developed here:
- http://ncatlab.org/nlab/show/Globular
There are already several examples of formalized proofs available, which give an idea of what Globular can be used for:
- Frobenius implies associative: http://globular.science/1512.004. (In a monoidal category, if multiplication and comultiplication morphisms are unital, counital and Frobenius, then they are associative and coassociative.)
- Strengthening an equivalence: http://globular.science/1512.007. (In a 2-category, an equivalence gives rise to an adjoint equivalence.)
- Swallowtail comes for free: http://globular.science/1512.006. (In a monoidal 2-category, a weakly-dual pair of objects gives rise to a strongly-dual pair, satisfying the swallowtail equations.)
- Pentagon and triangle implies $\lambda_I = \rho_I$: http://globular.science/1512.002. (In a monoidal 2-category, if a pseudomonoid object satisfies pentagon and triangle equations, then it satisfies $\lambda_I = \rho_I$.)
The project is open source (or at least will be very soon), and we hope it will prove useful to many in the community.
Best wishes, The Globular Team Krzysztof Bar, Aleks Kissinger and Jamie Vicary
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]