Email Gateway (Aug 22 2022 at 10:41): Email Gateway (Aug 22 2022 at 10:41):From: Marco Maggesi <maggesi@math.unifi.it>
Hi,
I'm new to Isabelle and I need help with a problem regarding implicit
structure arguments.
To learn Isabelle and since I would be interested in developing some
category theory in Isabelle, I'm trying to make some modifications to Greg
O'Keefe's AFP entry "Category theory using Isar and Locales" (the one
called "Category", not "Category2").
The essential modifications so far are related to two locales:
one_cat (in Functor.thy) and
into_set (in HomFunctor.thy).
In the original O'Keefe's code, these two locales introduce some kind of
"artificial" equations. E.g., the locale "one_cat" is obtained from
"two_cat" by adding an equation "BB = AA":
locale one_cat = two_cats +
assumes endo: "BB = AA"
I suspect that this approach was the only one available with some old
implementation of the locales machineries, but now we can do something
better by passing the appropriate parameters to the locale. This is what I
did
locale one_cat =
endo: two_cats AA AA
for AA :: "('o1,'a1,'m1) category_scheme" (structure)
Of course, the rest of the code has to be modified accordingly. I did part
of the work, but I'm now blocked by the following problem.
In the locale Yoneda (Yoneda.thy) the implicit structure argument is not
recognised anymore. For instance, I have to write Ob⇘AA⇙ instead of simply
Ob. I do not understand why.
My code is available here
https://www.dropbox.com/s/pp3jdd45checg27/Category.tar.gz?dl=0
Thank you for you help,
Marco
Last updated: Apr 26 2024 at 20:16 UTC