Open jamievicary opened 8 years ago
Another motivation for incorporating functors in Globular would be to easily define natural transformations, modifications of natural transformations, etc. At the moment, one has to input naturality equations by hand as and when required, a lengthy process that creates a big signature.It would be helpful if there were some process that automatically generated all naturality equations.
Given two workspaces, representing two n-categories, Globular will help you to define functors between them, and equivalence of functors, etc.
An immediate reason to want this is when using Globular to prove that two n-categories are equivalent. There is a lot of manual labour involved which Globular does not yet help very much with.