Hi,

I am trying to answer my own question here…

Is it possible to derive the axiom of induction from a model of the natural numbers?

…and came across this page on nLab:

This seems to have what I need, but the going is hard. I wonder if anyone can help.

I am stuck, for example, on what exactly $rec_p^n(...)$ is, and what a fibration is. The text says ’the above fibration’ but there is no fibration above so far as I can see, only what I’m guessing is a related display map. The page on fibrations is duanting and didn’t, at a quick glance, seem to give me the necessary relevant information.

All help appreciated!

Kind regards,

James

]]>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.

]]>