Re: Globular

[Jamie Vicary <jamie.vicary@cs.ox.ac.uk>]

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:
>
>    - http://globular.science
>
> 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/ ]