(March 11, 2017 at 6:09 am)Mathilda Wrote: I think this is a new one. No idea if you'll find this useful or not. My maths just isn't that good. Came across it and thought of your thread.
https://ncatlab.org/nlab/show/Globular
Quote:Globular is a web-based proof assistant for finitely-presented semistrict globular 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.
Thank you for your thoughtful post, Mathilda. In addition, I appreciate the time and effort that people have put into this thread. I'm looking forward to giving the suggestions, which have been offered by all of you in this thread, a whirl. Live long and prosper.
