Re: [isabelle] locales & category theory



On Thu, 16 Apr 2009, Benedikt.AHRENS at unice.fr wrote:

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.

This is briefly covered in the section on "Mixfix annotations" in the isar-ref manual, see http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf

locale category =
 fixes CC (structure)
 assumes dom_object [intro]:
 "f : Ar ==> Dom f : Ob"

Declaring CC as "structure" makes it an implicit argument for "indexed syntax", cf. the definition of hom with syntax Hom in the same theory. Thus you can refer to "hom CC A B" as "Hom A B" in that context.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.