You're making a mistake in your treatment of functions. A function is not a formula. It is an association of a value in the codomain to each value in the domain, and if two functions have all of the same associations (which forces them to have the same domain), then they are identical. Therefore >: and 1: with domain {0} are the same function. Consequently there is only one identity function on each set because the term "identity function" uniquely identifies where each point is sent to, namely, itself.
The distinction between large and small categories is that in a small category all the objects form a single set and all the arrows form another one. In a large category, the objects are members of a collection, which can be "bigger" than a set in an informal sense; in particular, all the sets form a collection but not a set, because a set cannot contain itself. The distinction is necessary from a formal perspective but is irrelevant to category theory as used in programming. Marshall On Fri, Apr 13, 2012 at 2:18 PM, Raul Miller <rauldmil...@gmail.com> wrote: > Ok, this helps a great deal. > > That said, I am dismayed by the english language the authors use to > describe arrows. There's an important distinction which exists in the > mathematical framework they construct, and while they are careful > about distinguishing analogous ambiguities in other contexts they > never directly mentions the existence of what I feel is a significant > ambiguity involving the ways that arrows can be functions. > > Here's an implementation of arrow, in J, which corresponds with their > initial construction of the theory in terms of a multigraph: > > arrow=: 2 :0 > assert. n -: y > u y > ) > > For example, a category with objects 0 and 1 could have arrows: > > >: arrow 0 > <: arrow 1 > 0: arrow 0 > 1: arrow 0 > > In other words, here an arrow is a constant function with a single > element domain. And, you can have different arrows that produce the > same result for a given domain. > > Relevant operations on these kinds of arrows include: > > source=: 1 :0 > ('';1;1;1) {:: 5!:1 <'u' > ) > > target=: 1 :0 > u u source > ) > > idArrow=: 1 :0 > (m"_) arrow m > ) > > isIdArrow=: 1 :0 > -:/ u`(u source idArrow) > ) > > label=: 1 :0 > ({.('';1) {:: 5!:1 <'u')`:6 > ) > > compose=: 2 :0 > if. u isIdArrow do. v return. end. > if. v isIdArrow do. u return. end. > u@v arrow (v source) > ) > > Here are some examples of these operations: > > (>: arrow 0) source > 0 > (>: arrow 0) target > 1 > (>: arrow 0) label > >: > > Note that the parenthesis here are not necessary, I have only included > them for emphasis. Note that the function which defines the target in > terms of the source is the label for the arrow, and different arrows > can have the same label. (I want arrows to have labels so that I have > some way of distinguishing between different arrows that connect the > same nodes in the underlying multigraph.) > > >: arrow 1 label > >: > >: arrow 2 label > >: > +&1 arrow 2 label > +&1 > > Note that arrows are functions: > (+&1 arrow 2) 2 > 3 > but they have restricted domains > (+&1 arrow 2) 3 > |assertion failure > > Also, note that we can have an arbitrary number of arrows connecting a > node to itself, and exactly one of those arrows is defined as the > identity arrow: > > The identity arrow for 0 is a constant function with the domain 0 and > the result 0: > 0 idArrow 0 > 0 > > This arrow behaves the same as an arrow based on the constant function 0: > (0 idArrow -: 0: arrow 0) 0 > 1 > > (Note that, in the above sentence, the parenthesis are important > because of J's word formation rules.) > > However, only one of these two arrows is the identity arrow: > (0 idArrow) isIdArrow > 1 > (0: arrow 0) isIdArrow > 0 > > And, we can compose arrows: > (>: arrow 2) compose (>: arrow 1) target > 3 > (>: arrow 2) compose (>: arrow 1) source > 1 > > Anyways, the above operations and examples roughly correspond with > what the authors describe as a "large category". The interesting > stuff starts happening when they deal with a "small category", which > is to say where the arrows and the objects are sets. > > So, first off, let's consider an example of what we can do if the > objects are sets. I want to write a concrete implementation, so I > will restrict myself to representing sets as a sequence such that > ~.@/:~ is an identity operation. > > smallArrowCore=: 2 :0 > 'codomain domain'=. n > assert. *./ (u"_1 domain) e. codomain > codomain"_@:(u"1) arrow domain > ) > > smallArrow=: 2 :0 > domain=. ~./:~ n > codomain=. ~./:~ m > smallArrowCore(codomain,&<domain) > ) > > smallDomain=: source > smallCodomain=: target > smallLabel=: 1 :0 > ({.('';1;0;1;1;1) {:: 5!:1 <'u')`:6 > ) > > smallCompose=: 2 :0 > assert. u source -: v target > (u label @ v label) (u target) smallArrow (u source) > ) > > smallIdArrow=: 1 :'(~./:~ m) idArrow' > > isSmallIdArrow=: 1 :0 > -:/ u`(u source smallIdArrow) > ) > > The difference here is that where before my function mapped directly > from the source to the target, here my function (my label) only > produces an image on the target, which means that I need to specify > the target explicitly. > > >: 1 2 smallArrow 0 1 target > 1 2 > >: 1 2 smallArrow 0 1 smallLabel > >: > > So now my objects are sets. But the authors specify that the arrows > be sets. What does this mean? > > I *think* this means that when they say "an arrow" they no longer mean > a single arrow but they mean "a set of arrows". And, I think they > mean the set of arrows in a category which (if they were build by the > routines I have implemented here) have the same label. > > But they might mean something else? > > If this is what they mean then the composition of arrows is also a set > of arrows, an identity arrow is a set of arrows, and so on... And, > where individual arrows must always be constant functions, a set of > arrows is a relationship, instead, between sets of domains. > > Anyways, if "an arrow" can be "an individual arrow" OR "a set of > arrows" then it is no longer the case that "an arrow" only connects a > single pair of objects. > > In other words, if my current understanding is correct, in chapter 1 > they went to great lengths to establish that an arrow was a unique, > single edge in a multigraph. And then, in chapter 2 they imply that > an arrow can be an entire subgraph of the multigraph. > > If my understanding is correct, then I am bothered that they would > make this leap without stating it more clearly. If my understanding > is not correct then I am missing something big. > > Thanks, > > -- > Raul > > On Fri, Apr 13, 2012 at 7:04 AM, Robert Raschke <rtrli...@googlemail.com> > wrote: > > May I recommend this introduction to Category Theory: > > > http://www.ling.ohio-state.edu/~plummer/courses/winter09/ling681/barrwells.pdf > > > > The first ten pages should suffice to get a bit of clarity with the > > terminology. (Section 2.1.11 defines the "category of sets".) > > > > Robby > > > > On Thu, Apr 12, 2012 at 10:49 PM, Raul Miller <rauldmil...@gmail.com> > wrote: > > > >> On Thu, Apr 12, 2012 at 3:46 PM, Jordan Tirrell > >> <jordantirr...@gmail.com> > We are using what we know about functions > >> on sets simply to define the > >> > category *Set* (where objects are all sets and arrows are all > functions > >> on > >> > sets). > >> > >> That seems to be ambiguous, though, and I am trying to understand > >> what's really meant. > >> > >> The issues which are significant, to me, are: > >> > >> 1. The difference(s) between a "Function" and an "Arrow" which in some > >> way represents a function. > >> > >> 2. The difference between a member of a domain and the domain itself. > >> > >> 3. What exactly is being represented by the composition of arrows. > >> > >> > We then usually try to capture ideas about functions in categorical > >> > language in *Set*. Marshall gave a great example about how we can > look at > >> > the category *Set* alone and identify which object corresponds to the > >> empty > >> > set, and which objects correspond to one-element sets. Specifically, > the > >> > empty set is the object in our category which has a unique arrow to > every > >> > object (in general this is called an initial object). > >> > >> And, this uniqueness works with a variety of different concepts for > >> how Arrows relate to Functions. > >> > >> > The dual notion of terminal object identifies the singleton sets. > >> > The power of category theory is right here: we have left behind > >> > our normal definitions of empty set and singleton set and discovered > >> > that they correspond to the categorical definitions of initial and > >> > terminal object (within this specific category *Set*). > >> > >> No. > >> > >> We have not yet left behind our normal definition of the -- that > >> definition was a part of the definition of this *Set*. We also > >> have not yet fully defined *Set*. > >> > >> > Now a set theorist can sit down with, say, a group theorist, and even > if > >> > both are ignorant of each other's field, they can have a meaningful > >> > conversation: Does the category you study have an initial/terminal > >> object? > >> > One or many? Of course this is a toy example, but I think its a good > >> > glimpse into the usefulness of category theory as a unifying theme in > >> math. > >> > >> I have no problems believing that a notation can be useful. > >> > >> That is why I am interested in the first place. > >> > >> But before I can go there, there's a little matter of making sure > >> I understand what the notation means. > >> > >> >> First off, as a side note, let us consider "the set of all sets which > >> >> are not contained in any categories". Without further axioms we do > >> >> not know if this set is empty or non-empty. (Example axioms: "The > >> >> set of all sets which are not contained in any categories is a > >> >> non-empty set", or "The set of all sets which are not contained in > any > >> >> categories is an empty set".) So right off, we know that involving > >> >> sets introduces all of the problems that sets have. > >> > > >> > As far as I know, set theory axioms would not allow a definition like > >> "the > >> > set of all sets which are not contained in any categories". > >> > >> All I need, to be able to do this, is to have a formal definition > >> of "category" in my system. > >> > >> > There are some very interesting issues with the use of sets > >> > vs collections when we discuss categories, which is why > >> > restricting to categories whose objects and arrows both form > >> > sets (called a small category) is common. *Set* is not small, so > >> > we do have to be careful. Let's not get into set theory though, > >> > since I will quickly be unable to offer good answers to questions, > >> > and it is another step removed from J programming. > >> > >> Yes... I wanted to work with a category where the objects represented > >> the domain of the values 0 and 1 and where arrows represented functions > >> on that domain. Another domain I liked was where objects represented > >> the domain of the values 0, 1, 2, 3 or 4. > >> > >> >> We could say that an arrow corresponds to a function and an object > >> >> corresponds to the domain of a function (and the object that an arrow > >> >> leads to corresponds to the image of the function). Here, > identifying > >> >> an arrow uniquely identifies a function. > >> > > >> > This is a category, it is like *Set* but restricted to onto functions. > >> > >> Then I need a more complete definition of the category *Set*. > >> > >> But I think you are saying here that the function with the > >> domain {0, 1} and the image {0} with codomain {0} is a different > >> function from the function with the domain {0, 1} and the image > >> {0} with the codomain {0, 1}. > >> > >> And, while I can accept that these are different arrows, it > >> seems to me that these are the same function. > >> > >> -- > >> Raul > >> ---------------------------------------------------------------------- > >> For information about J forums see http://www.jsoftware.com/forums.htm > >> > > ---------------------------------------------------------------------- > > For information about J forums see http://www.jsoftware.com/forums.htm > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm > ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm