From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/8753 Path: news.gmane.org!not-for-mail From: Jamie Vicary Newsgroups: gmane.science.mathematics.categories Subject: Re: Globular Date: Sat, 5 Dec 2015 23:47:15 +0000 Message-ID: Reply-To: Jamie Vicary NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Trace: ger.gmane.org 1449495716 32309 80.91.229.3 (7 Dec 2015 13:41:56 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 7 Dec 2015 13:41:56 +0000 (UTC) To: Categories list Original-X-From: majordomo@mlist.mta.ca Mon Dec 07 14:41:45 2015 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp3.mta.ca ([138.73.7.22]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1a5w2y-0003kP-WF for gsmc-categories@m.gmane.org; Mon, 07 Dec 2015 14:41:45 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:43233) by smtp3.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1a5w1y-000722-JD; Mon, 07 Dec 2015 09:40:42 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1a5w1w-0004NG-OZ for categories-list@mlist.mta.ca; Mon, 07 Dec 2015 09:40:40 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:8753 Archived-At: 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 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/ ]