Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorBen_Sprott
   • CommentTimeMay 4th 2012
   • PermaLink
   Author: Ben_Sprott
   Format: MarkdownItexI am looking for any kind of paper that uses structural induction where the ordered set is actually a collection of categories and the ordering relation is any kind of functor. I am thinking of the category with only one morphism as a base case. In particular, I am interested in the collection of internal categories in a monoidal category, but any usage of this method (over cats) would be of interest. In the case of internal cats, given any structural inductive proof in the collection of internal categories, what does the proof say about the underlying monoidal category. Can we present an axiom of the underlying monoidal category M as an inductive proof. That is, proven inductively over the collection of internal categories of M, any proven axiom also is an axiom of the underlying category? If I am dead wrong in assuming you can do structural induction over categories, please help me to understand why.

   I am looking for any kind of paper that uses structural induction where the ordered set is actually a collection of categories and the ordering relation is any kind of functor. I am thinking of the category with only one morphism as a base case. In particular, I am interested in the collection of internal categories in a monoidal category, but any usage of this method (over cats) would be of interest. In the case of internal cats, given any structural inductive proof in the collection of internal categories, what does the proof say about the underlying monoidal category. Can we present an axiom of the underlying monoidal category M as an inductive proof. That is, proven inductively over the collection of internal categories of M, any proven axiom also is an axiom of the underlying category?

   If I am dead wrong in assuming you can do structural induction over categories, please help me to understand why.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeMay 4th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexCan you define more precisely what you mean by "structural induction"? To me "structural induction" usually means induction over some inductive definition.

   Can you define more precisely what you mean by “structural induction”? To me “structural induction” usually means induction over some inductive definition.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeMay 5th 2012
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexAre there interesting cases where you have an initial 2-algebra in some 2-category of 2-algebras for a 2-functor: $Cat \to Cat$?

   Are there interesting cases where you have an initial 2-algebra in some 2-category of 2-algebras for a 2-functor: $Cat \to Cat$?

4. • CommentRowNumber4.
   • CommentAuthorBen_Sprott
   • CommentTimeMay 7th 2012
   • PermaLink
   Author: Ben_Sprott
   Format: MarkdownItexHi, I looked up inductive type and now I see David's comment as a generalization of the inductive type where the types are categories themselves. Let me know if I have that right. I tried all weekend to create an inductive defintion for a class of categories which fit my interests. I couldn't do it. I will have to work out the idea, but I guess you will have to inductively define a collection of categories where the ordering relation is a suitable functor. The main idea in my posting is that, since in structural induction you can have induction over ordered structures that are partially ordered you might get a rich collection of categories over which to do the induction. While I have your attention, I might add another desired property for the partially ordered, inductively defined collection of categories. A while back, I posted about a concept I called "category update", where an update is a functor like adding a morphism or adding the data that two morphisms can be composed or adding a commuting arrow to a composed pair so that you get a triangle or a square. I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be "updates". The simple intuition here is that, starting at the base case of an empty category, an update functor adds the first arrow. From there on you have a rich collection of cats to get to and this forms a partially ordered collection of cats. I can't grasp the initial algebra as the inductive type. I will probably look into that next as an alternate route. Is there a suggestion that anyone has? Does this sound like anything?

   Hi,

   I looked up inductive type and now I see David’s comment as a generalization of the inductive type where the types are categories themselves. Let me know if I have that right. I tried all weekend to create an inductive defintion for a class of categories which fit my interests. I couldn’t do it. I will have to work out the idea, but I guess you will have to inductively define a collection of categories where the ordering relation is a suitable functor. The main idea in my posting is that, since in structural induction you can have induction over ordered structures that are partially ordered you might get a rich collection of categories over which to do the induction.

   While I have your attention, I might add another desired property for the partially ordered, inductively defined collection of categories. A while back, I posted about a concept I called “category update”, where an update is a functor like adding a morphism or adding the data that two morphisms can be composed or adding a commuting arrow to a composed pair so that you get a triangle or a square. I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be “updates”. The simple intuition here is that, starting at the base case of an empty category, an update functor adds the first arrow. From there on you have a rich collection of cats to get to and this forms a partially ordered collection of cats.

   I can’t grasp the initial algebra as the inductive type. I will probably look into that next as an alternate route.

   Is there a suggestion that anyone has? Does this sound like anything?

5. • CommentRowNumber5.
   • CommentAuthorBen_Sprott
   • CommentTimeMay 7th 2012
   • (edited May 7th 2012)
   • PermaLink
   Author: Ben_Sprott
   Format: MarkdownItexThis is going to sound cracked, but this all looks like the foundation for a Bayesian inference "over structure itself". (I guess I am quoting myself here. Mike will have to double quote that to get me to explain what I mean. So many of my vague comments have garnered quotation and patient puzzlement. Panangaden was not impressed when I used vague language, so I want to thank you all for your patience.) :) If someone could say anything about the compact or finitely presentable categories in our collection of cats and updates (inductively defined), it would help me a lot. I will never be able to finish this work. It sounds really neat, though. We need to finish off the axioms for what a "category update is", identify that it forms an inductively defined collection of cats, and then understand how to do the proof by induction over the collection (what I called structural induction). Another thing: any proof by this kind of induction is a proof about the collection itself. So, say that our collection of cats was, in fact, every cat. Then any proof by this induction would actually be about categories themselves. Taken together, the theorems would constitute a presentation of the theory of categories.

   This is going to sound cracked, but this all looks like the foundation for a Bayesian inference “over structure itself”. (I guess I am quoting myself here. Mike will have to double quote that to get me to explain what I mean. So many of my vague comments have garnered quotation and patient puzzlement. Panangaden was not impressed when I used vague language, so I want to thank you all for your patience.) :)

   If someone could say anything about the compact or finitely presentable categories in our collection of cats and updates (inductively defined), it would help me a lot.

   I will never be able to finish this work. It sounds really neat, though. We need to finish off the axioms for what a “category update is”, identify that it forms an inductively defined collection of cats, and then understand how to do the proof by induction over the collection (what I called structural induction).

   Another thing: any proof by this kind of induction is a proof about the collection itself. So, say that our collection of cats was, in fact, every cat. Then any proof by this induction would actually be about categories themselves. Taken together, the theorems would constitute a presentation of the theory of categories.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeMay 7th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be "updates". Are you suggesting that the idea of one thing coming "after" another in the ordering relation used for structural induction is analogous to the idea of one category being generated by adding objects or morphisms or relations to another one? If so, then I think the phrase ordering *relation* is misleading, because a category can be generated in many such ways. Perhaps what you are looking for is the idea of categorical cell complexes. Suppose in some category (this in an "ambient" category, not the categories you want to build with updates) we have a collection of morphisms $S_i \to D_i$, called "cells" or "generating cofibrations". In topology we think of $S_i$ as a "sphere" of some dimension, $D_i$ as a "disc", and the map as the inclusion of a sphere as the boundary of the disc of one higher dimension. In terms of your "updates" you can think of $S_i$ as specifying the data that you might have before your update, and $D_i$ as the result of the update. Then the operation of "attaching a cell", which might roughly correspond to your "updates", means pushing out one of these morphisms: $$\array{ S_i & \to & X \\ \downarrow && \downarrow \\ D_i & \to & X \sqcup_{S_i} D_i }$$ For instance, in the ambient category $Cat$, we can consider the following morphisms as our cells: * The inclusion $0\to 1$ of the empty category into the trivial category. * The inclusion $2\to I$ of the two-object discrete category into the [[interval category]]. * The map $P \to I$ from the walking [[parallel pair]] (which has two objects $x$ and $y$ and two nonidentity morphism $x\rightrightarrows y$) to the interval category. Then attaching a cell of the first type means adding an object. Attaching a cell of the second type means adding a morphism (and, in consequence, freely adding all composites of that morphism with the existing morphisms in the category). And attaching a cell of the third type means forcing two given morphisms to become equal (along with all other equalities of morphisms that that entails). In general, a *cell complex* is an object together with a way to build it up with a (possibly transfinite) sequence of cell attachments of this sort. (In the transfinite sequence we just take colimits at limit ordinals.) Being a cell complex is *structure* on an object: we may be able to build up an object in more than one way as a cell complex, or perhaps in no ways at all. (This is clear in topology: not all topological spaces are cell complexes!) But in $Cat$ with the above three cells, there is the special property that every object admits a cell complex structure. The nice thing about cell complexes is that once you've *chosen* a cell complex structure on a particular object, then you can argue by induction up the cell complex. This gives us a way to prove things about all cell complexes. For instance, we can prove something about arbitrary categories if we can prove that it is preserved by all three types of cell attachments, and by passage to colimits. Is this is the analogy to structural induction that you're thinking of?

   I think that the inductively defined collection of cats should have this property, ie that the functors forming the ordering relation to be “updates”.

   Are you suggesting that the idea of one thing coming “after” another in the ordering relation used for structural induction is analogous to the idea of one category being generated by adding objects or morphisms or relations to another one? If so, then I think the phrase ordering relation is misleading, because a category can be generated in many such ways.

   Perhaps what you are looking for is the idea of categorical cell complexes. Suppose in some category (this in an “ambient” category, not the categories you want to build with updates) we have a collection of morphisms $S_i \to D_i$, called “cells” or “generating cofibrations”. In topology we think of $S_i$ as a “sphere” of some dimension, $D_i$ as a “disc”, and the map as the inclusion of a sphere as the boundary of the disc of one higher dimension. In terms of your “updates” you can think of $S_i$ as specifying the data that you might have before your update, and $D_i$ as the result of the update. Then the operation of “attaching a cell”, which might roughly correspond to your “updates”, means pushing out one of these morphisms:

   $$\array{ S_i & \to & X \\ \downarrow && \downarrow \\ D_i & \to & X \sqcup_{S_i} D_i }$$

   For instance, in the ambient category $Cat$, we can consider the following morphisms as our cells:

   • The inclusion $0\to 1$ of the empty category into the trivial category.

   • The inclusion $2\to I$ of the two-object discrete category into the interval category.

   • The map $P \to I$ from the walking parallel pair (which has two objects $x$ and $y$ and two nonidentity morphism $x\rightrightarrows y$) to the interval category.

   Then attaching a cell of the first type means adding an object. Attaching a cell of the second type means adding a morphism (and, in consequence, freely adding all composites of that morphism with the existing morphisms in the category). And attaching a cell of the third type means forcing two given morphisms to become equal (along with all other equalities of morphisms that that entails).

   In general, a cell complex is an object together with a way to build it up with a (possibly transfinite) sequence of cell attachments of this sort. (In the transfinite sequence we just take colimits at limit ordinals.) Being a cell complex is structure on an object: we may be able to build up an object in more than one way as a cell complex, or perhaps in no ways at all. (This is clear in topology: not all topological spaces are cell complexes!) But in $Cat$ with the above three cells, there is the special property that every object admits a cell complex structure.

   The nice thing about cell complexes is that once you’ve chosen a cell complex structure on a particular object, then you can argue by induction up the cell complex. This gives us a way to prove things about all cell complexes. For instance, we can prove something about arbitrary categories if we can prove that it is preserved by all three types of cell attachments, and by passage to colimits. Is this is the analogy to structural induction that you’re thinking of?

7. • CommentRowNumber7.
   • CommentAuthorBen_Sprott
   • CommentTimeMay 19th 2012
   • PermaLink
   Author: Ben_Sprott
   Format: MarkdownItexHi Mike, I apologize for not replying. The simple fact is that your answer went over my head. I notice that you have agreed with me in spirit that we seem to have, at least according to your perscription, a foundation to have theorems in the theory of categories which are given, or proved, in an inductive way. I need to go over your suggestion carefully to see if it is what I am thinking about. In any case, thanks for the response!

   Hi Mike,

   I apologize for not replying. The simple fact is that your answer went over my head. I notice that you have agreed with me in spirit that we seem to have, at least according to your perscription, a foundation to have theorems in the theory of categories which are given, or proved, in an inductive way. I need to go over your suggestion carefully to see if it is what I am thinking about. In any case, thanks for the response!

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeMay 20th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSorry about that; I guessed that it might. You could try learning some Quillen model category theory, which is where the abstract notion of cell complex originates.

   Sorry about that; I guessed that it might. You could try learning some Quillen model category theory, which is where the abstract notion of cell complex originates.