[isabelle] locales & category theory
I am an Isabelle beginner and interested in the development on category
My long term goal is to extend this library a bit.
The code is more or less self-explaining, but I have one question:
What does the keyword "structure" in parentheses in the following code
excerpt mean? I looked for it in the Isabelle tutorial (which does not
cover locales, unfortunately) as well as in "Locales - a sectioning
concept..." but could not find it.
locale category =
fixes CC (structure)
assumes dom_object [intro]:
"f : Ar ==> Dom f : Ob"
When you answer, please put me in CC, since I haven't subscribed to the
Thanks a lot in advance,
This archive was generated by a fusion of
Pipermail (Mailman edition) and