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.

]]>