exponential category missing in Index of Symbols

[bblfish]

Definition 9.2.3. For precategories A, B, there is a precategory BA defined by...

Is there a name for this BA ? ( Exponential pre-category perhaps ? )

I could not find the notation in the Index of Symbols.

[bblfish]

I came across this while trying to understand the Yoneda Lemma. This starts with defining the hom-functor homA: Aop x A -> Set . From the definition it is clear that the subset of Set that is referred to here could be more precisely defined with generics. Following Scala notation perhaps one could write this as follows

homA: Aop x A -> Set[Arrow[A]] 

where Arrow[A] is a type homA(x,y) with x,y: A perhaps... This would then be the subcategory of Set where all the objects are limited to arrows between objects of A.

one could then define the induced yoneda functor as

y: A -> Set[Arrow[A]]^^Aop

(where ^^ is the to-the-power-of operator - as I can't show this in markdown here )

This would mean that given an a: A one can then get the "exponential pre-category(?)" Set[Arrow[A]]^^Aop whose objects are functors from Aop -> Set[Arrow[A]] and whose morphism are the natural transformation between them. ya would be of that type, meaning that its objects are functors that given any object a':A give us the morphisms ya(a'): Set[Arrow[A]] of morphisms between a and a' in A defined by homA(a,a') . This makes a lot of sense it seems. It does mean though that in the "exponential pre-category(?)" Set[Arrow[A]]^^Aop objects always contain an implicit selection of some a: A, otherwise how could one go in the functor Aop -> Set[Arrow[A]] from the antecedent to the conclusion which requires at least two points?

Is my reasoning correct here? It suggests that generics support in HoTT would make things even clearer. ( I could bring this up on the mailing list but thought I'd mention it here first ).

What led me to this thinking was wondering about Theorem 9.5.4 ( the Yoneda Lemma ) which established an isomorphism between the precategories homSet[Arrow[A]]^^Aop and Fa where F: Set[Arrow[A]]^^Aop ie F is an object in that "exponential pre-category(?)".

But then I was wondering to what a': A is F fixed to? Perhaps it does not matter, and that's the point of the proof... But at this point I was worried that I may have misunderstood something.

[andrejbauer]

Scala notation and in general thinking in terms of objects, classes and types as known in programming languages is at best misleading here. I would advise you to do it in very small amounts. The types in HoTT have only a very superficial resemblance with types in programming languages (and none with classes in object-oriented languages).

[bblfish]

Is it wrong to think that there may be a narrower category than Set that would better describe the objects of the range of the hom functor? After all as it is defined the hom functor only sends Aop x A to objects in Set that are morphisms... One could do this by defining a sub category of Set with generics as I did above, but one could just define a more precise category than Set with specific objects and morphisms using the definitions of hom-functor and name it say SetArrowA without thinking of generics. ( Generics would then be a later potential generalisation which as I understand some people are trying to bring to HoTT - using colors for example )

Can you be more precise about how it is misleading me here? That would help.

[andrejbauer]

Take any set S, and define a category C with two objects 0 and 1 such that

• Hom(0,0) = {id_0}
• Hom(0,1) = S
• Hom(1,1) = {id_1}
• Hom(1,0) = {}

Then S will be in the image of the Hom functor. So you cannot narrow down Set.

[bblfish]

I read in the HoTT book

Definition 9.1.1. A precategory A consists of the following.
...
(ii) For each a, b : A, a set homA(a, b) of arrows or morphisms.
...

It says clearly that it must be a set of arrows or morphisms. I.e not any set will do. Or else the sentence of arrows or morphisms would be useless. You seem to be suggesting that S can potentially a set that does not contain arrows or morphisms. But that seems to contradict the definition 9.1.1 .

Btw this notion of a set of is what generics captures. A Set of fish, is a set that contains just fish, a set of contracts contains just contracts as objects, etc...

[andrejbauer]

I just defined a category whose set of arrows between 0 and 1 is S. The point is that any set may be the "set of arrows".

[bblfish]

If any set can be a set of arrows, then the notion of a set of arrows is vacuous. 1) If S is a set of arrows then it must contains 0 or more arrows, and so I was correct to be able to constrain the hom functor to a subcategory of Set whose objects are only sets of arrows. 2) If S is not a set of arrows then there is a contradiction with the definition 9.1.1 (ii) quoted above

[pthariensflame]

@bblfish Your confusion arises because you think "arrows" is a pre-existing notion. It is not. The "set of arrows" can be any set and then an "arrow" is, by definition, an arbitrary element of that set.

[bblfish]

@pthariensflame hmm. I suppose it's grammatical then. Perhaps a bit like in RDF the relation that is an arrow when in the second position. Still there it refers to a set of pairs. ... (one kind of expects that if one knows an arrow one would know between what it was a morphism, whereas here one may never be able to find out ...) I'll think this through tomorrow in light of this.

[mikeshulman]

This sort of language is very common in mathematics -- the boldface of "objects" in (i) and "arrows or morphisms" in (ii) also serves to emphasize that those words are being defined to mean elements of the types in question -- so it never occurred to me that it might be confusing. We could easily change it to be more explicit, like "a set hom_A(a,b), whose elements are called arrows or morphisms".

Regarding the original question, I would say B^A should be called the functor precategory. I guess we could add it to the index of symbols, although it's not exactly a "symbol" (since it doesn't involve any symbols other than A and B), and in particular I wouldn't know what to alphabetize it under; "f" for "functor" maybe?

[mikeshulman]

one kind of expects that if one knows an arrow one would know between what it was a morphism, whereas here one may never be able to find out

I'm not sure what you mean by that; if I have an arrow f : hom_A(x,y) then by definition it is between x and y.

[bblfish]

@mikeshulman I think your suggestion "a set hom_A(a,b), whose elements are called arrows or morphisms" would indeed be better. I think this is more important here in HoTT than elsewhere perhaps as in HoTT there is a lot of talk of things that are very much like arrows or morphisms but that are well defined, such as the paths of chapter 2. One is nearly expecting at this point that a unification of paths in homotopy and arrows in Category Theory are going to be made here.

Perhaps also it was a few remarks by Robert Harper in his course on HoTT at CMU where he criticises non intuitionistic logic for not helping explain why in an if-conditional one comes to the conclusion one does. He was arguing that the advantage of functions here is that this helps give a computational explanation. I suppose by taking any set to potentially be a morphism, one is back to something quite arbitrary of the same type.

one kind of expects that if one knows an arrow one would know between what it was a morphism, whereas here one may never be able to find out

I'm not sure what you mean by that; if I have an arrow f : hom_A(x,y) then by definition it is between x and y.

For example with the paths of chapter 2 I think one is nearly in the position if given a path to find out what the endpoints of those paths are. If an elephant Joe where to be the morphism for +2 there would be little way of knowing seeing joe that one was in presence of the +2 operation. So it some way it seems that one has to see a category as a mini language - as in language the arbitrariness of the sign is a well known phenomenon. But a sign refers to something and then one is left wondering if this notion of reference has been filled out here.

I suppose also that there is something a bit odd in that what in one category can be a set of morphisms, in another category is just going to be a set of numbers, or strings of an alphabet, etc... One gets the feeling here that this type of switching of meaning in different contexts is going to end up breaking type safety.

[bblfish]

Regarding the original question, I would say B^A should be called the functor precategory. I guess we could add it to the index of symbols, although it's not exactly a "symbol" (since it doesn't involve any symbols other than A and B), and in particular I wouldn't know what to alphabetize it under; "f" for "functor" maybe?

thanks that would help. It's perhaps not a symbol, but it certainly is a notation since you raise one of the symbols up. I just found that in S. Awodey's book "Category Theory" there is something similar called exponentials of categories in chapter 7.6

[mikeshulman]

Given a path, one is always in the position of knowing its endpoints, because just like for a morphism, the type of a path ("x=y") tells you what its endpoints are, and you can't have a path without knowing its type.

It's true that if one has a category such that hom(x,y) := Elephant for some objects x and y, then if we just have Joe:Elephant then we "don't know what its domain and codomain are". However I would argue that if we just have Joe:Elephant then we don't "know an arrow" at all! We know an elephant. In order to "know an arrow", we have to be given a thing whose type is a hom-type, and if we are given instead Joe:hom(x,y) then we do know the domain and codomain of Joe, namely x and y. In other words, in order to say that Joe:Elephant "is an arrow" we must have fixed a particular hom-type hom(x,y) that is (judgmentally) equal to Elephant.

[bblfish]

Thanks, will think through the problem with this extra information.

[bblfish]

( Back from walking in the mountains yesterday )

@mikeshulman from what you say could one then not define the homfunctor more precisely as:

hom: Aop x A -> SetOfHomsInA

Where one knows that every object in SetOfHomsInA is of type homA(a,b) for some a,b: A . Perhaps one could even make a type of it using dependent function type or the dependent pair type ( not sure about this ). Or perhaps one actually needs some notion of generics to do this...

I am just hoping that by being more precise I can then see more clearly the structure of the argument.

[mikeshulman]

No.

[bblfish]

ok.

[mikeshulman]

Sorry for being so brief, I was in a hurry (probably I should have waited and written a fuller reply later). I don't quite understand your motivation, but I don't think there is any way to define SetOfHomsInA without already having hom, so I don't think what you are proposing is possible. Which argument are you trying to see the structure of?

[andrejbauer]

Since you like to think in terms of Scala and programming language (which to me looks like the root cause of your misunderstanding what is hapenning – HoTT and category theory are not like Scala), let me give an example of a category whose morphisms obviously are not morphisms. Maybe that will help.

We define the category MyCat to consists of the following:

• the type of objects is Unit
• the type of morphisms from () to () is defined to be Boolean.
• the identity morphism from () to () is true
• the composition of morphisms p and q (which are Boolean by definiton) is the morphism p && q.

This is a category because p && (q && r) = (p && q) && r and true && p == p && true == p.

You see, you can make a category from anything you like as long as your construction satifies the conditions given in the definition of a category. The definition of a category does not limit what you might take as objects and morphisms – anything goes. I can make a category out of pieces of wood.

[awodey]

On Aug 25, 2015, at 2:10 PM, Andrej Bauer notifications@github.com wrote: I can make a category out of pieces of wood.

I like you to do that!

; - )

Steve

[martinescardo]

On 25/08/15 19:13, Steve Awodey wrote:

On Aug 25, 2015, at 2:10 PM, Andrej Bauer notifications@github.com wrote: I can make a category out of pieces of wood.

I like you to do that!

Just for the record, Dan Ghica makes categories out of pieces of paper and strings together with very young school children.

http://researchblogs.cs.bham.ac.uk/thelablunch/2015/05/inventing-an-algebraic-knot-theory-for-eight-year-olds-iv/

Martin

; - )

Steve

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/851#issuecomment-134690594.

Martin Escardo http://www.cs.bham.ac.uk/~mhe

[andrejbauer]

Take 5 pieces of wood. Throw them all away. What is left is known as the empty category.

[awodey]

here is a category with 4 objects and one non-trivial arrow made of wood.

On Aug 25, 2015, at 3:39 PM, Andrej Bauer notifications@github.com wrote:

Take 5 pieces of wood. Throw them all away. What is left is known as the empty category.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/851#issuecomment-134712831.

[bblfish]

@andrejbauer wrote:

We define the category MyCat to consists of the following:

1. the type of objects is Unit
2. the type of morphisms from () to () is defined to be Boolean.
3. the identity morphism from () to () is true
4. the composition of morphisms p and q (which are Boolean by definiton) is the morphism p && q.

I suppose Unit is equivalent to 1 whose only element is * . So if I follow the new definition 9.1.1 of the book we have

For the pre-category MyCat abbreviated below to C we have

1. C0 :≡ 1
2. since there is only one instance *: 1 we have only one homC relation namely homC(*,*) :≡ Boolean ( which means by the way that there are only two morphisms true and false )
3. The identity on the only object * is 1*: homC(*,*) ≡ Boolean and 1* :≡ true

It follows from 2 and 3 that false: homC(*,*) and false: Boolean. ( if only because Boolean ≡ homC(*,*) ).

We can then define the hom-functor as in the book with

homfC: Cop x C -> Set

Perhaps I could then also define a category BC containing as objects just Boolean and as morphisms

homfC' (true,true)  :≡ b -> true && b && true
homfC' (true,false) :≡ b -> false && b && true
homfC' (false,false)  :≡ b -> false && b && false
homfC' (false,true) :≡ b -> true && b && false

then this would be precisely true

homfC': Cop x C -> BC

then I should have also

y': C -> BC^^Cop

I think I was thinking along these lines... It should work for this particular case, then it will help me understand the more general one...

[bblfish]

I worked through the above in more detail to see what it would look like. I seem to get two natural transformation ( which I need or else y': C -> BC^^Cop would not give the correct result.

[andrejbauer]

Uhm, what's your point? Also, the hott-caffe mailing list is a better forum for this discussion. We already got out of this issue what we could, namely a clarification of the text.

[andrejbauer]

Regarding Steve's wood category: the identity chickens are a bit displaced. I hear it's hard to keep them in one place.

[bblfish]

@andrejbauer I have no clear point at present. I was just was showing what I meant by thinking of the yoneda lemma by reducing the Set down to the smallest category of import to the given type A. So above y' : C -> BC^^Cop makes it possible for me to draw that category, whereas drawing Set is impossible. I am looking for the point at which this makes a difference to the reasoning in the book, but have not found that point yet. ( I am reading slowly - it's summer and very hot )

As for objects and morphisms it occurs to me that Steve Awodey in the second edition of Category Theory states in footnote 14 page 28 that:

The notion of a category can also be defined with just one sort ( arrows ) rather than two ( arrows and objects ); the domains and codomains are taken to be certain arrows that act as units under composition, which is partially defined. Read about this definition in section 1.1 of Mac Lane's Categories for the working mathematician, and do the exercises mentioned there....

Could it be that in Category Theory there really only are arrows?

[andrejbauer]

Your last question makes no sense, especially just after a quote which explains that there are several ways of defining categories. In some of these there are arrows and objects, and in others there are just arrows. But more importantly, you seem to think that the nature of mathematical objects is absolute and predetermined. I tried to demonstrate that this is no so by giving you two examples: (1) every set can be the hom-set in a category, and (2) boolean values may be seen as arrows. Rather than thinking in terms of mathematical entities having fixed, predetermined types, think instead about the fact that one and the same mathematical objects can play many different roles in many different structures (a pair of real numbers can be a complex number, a point in the plane, or a linear polynomial).

[bblfish]

everyone, thanks a lot for the answers. It's been very helpful.