Stream: Beginner Questions

Topic: how to define a category using the category theory library

view this post on Zulip ee (Feb 01 2024 at 13:50):

If I am trying to define a specific instance of a category, how do I go about it? Do I define a locale like "locale cat = Category + "(which also throws an error saying Category isn't defined, I only imported Main, maybe I need to iport something else, I triied Category2 and Category3 but failed), should I write a definition using "MakeCat " or "('o,'m,'a) Category_scheme ", if so, how? Or should I do something entirely different? If there are resources I can use to mimic the style of such a constructipon, I'd highly appreciate it! Sorry for the dumb question lol.

view this post on Zulip Mathias Fleury (Feb 01 2024 at 13:53):

  1. See the instruction from the AFP https://www.isa-afp.org/help/

view this post on Zulip Mathias Fleury (Feb 01 2024 at 13:55):

  1. I am not sure if you want to extend the category locale (then you have the right syntax) or want to instantiate it (interpretation). In both cases, a look at the https://isabelle.in.tum.de/dist/Isabelle2023/doc/locales.pdf tutorial is a good start.

view this post on Zulip ee (Feb 01 2024 at 14:32):

Thank you! Appreciate it!

Last updated: Apr 27 2024 at 12:25 UTC