It is well-known that we can do proof by induction in a topos using the natural number object, I am interested in proving the strong induction principle, and I am attempting to translate this proof here https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ( (I) $\to$ (SI) ) into an abstract version, so it works for the natural number object in a category satisfies ETCS (In particular, the topos satisfies well-foundedness, and every subobject has complement, therefore, this is a Boolean topos).

The $\le$ relation is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).

I think the statement of strong induction to prove is as the following.

For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, “all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$” implies “$s \circ n: 1 \to N \to N$ factors through P”, then $P\cong N$.

I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS, and hence have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?

p.s. The problem that I am actually interested in is proving the well-foundedness of natural number object (explicitly, every non-empty set has a minimal element), but the “material set theoretic proof” using strong induction. Therefore I think I should get strong induction principle for NNO. It will also be great if we can directly prove the well-ordered principle for NNO. (Have searched online for well-orderedness and strong induction for NNO, but nothing helpful is found. Is there any material to read about them?)

]]>I could not understand the proof of the fact that if a vector space $V$ over a field $k$ is dualisable in the monoidal category $\mathbf{Vect}_k$ then it should be finite dimensional. I understand that the image of $k$ under the unit is a $1$-dimensional subspace, but why should this imply the finite dimensionality of $V$? I would be thankful if someone could provide me the complete proof or a pointer to it.

With my regards,

partha

]]>It appears that the notion of “left dual” and “right dual” in nLab differs from the literature. If we want “left dual” to coincide with “left adjoint”, shouldn’t we worry about the fact that $\otimes$ is the composition of 1-cells in the *diagrammatic order*? So, $i : I \to A^* \otimes A$ would be $i : I \to AA^*$ in the normal juxtaposition notation. That would mean that $A^*$ is the *left adjoint* of $A$. But, the page dualizable object calls it the “right dual” of $A$.

It is well known that a category can be defined as a certain simplicial set obtained by iterated fibred products which satisfies the internal horn filler condition; moreover, requiring horn filling for all horns (i.e., the Kan condition) one obtains the notion of groupoid. Then both the notions of category and groupoid should have an internalization in any category where one is able to arrange things in a way to have the required fibered products, and to state the horn filling condition.

This is what happens, e.g., when one defines Lie groupoids imposing that the source and target maps are submersions. Similarly one has a notion of Lie category, which by some reason seems to be less widely known of the more particular notion of Lie groupoid (maybe this is not surprising.. after all I suspect the notion of category is less known of that of group..). Another classical example are topological categories and groupoids.

Moving from categories and groupoids to oo-categories and oo-groupoids, one should have a similar internal simplicial object based notion of, e.g., Lie oo-groupoid. However, in the nLab the oo-sheaf point of view seems to be largely preferred to the internal Kan object point of view. Why is it so? is the oo-sheaf version just more general and powerful or there are problems with the internal version? I’m asking this since at internal infinity-groupoid it is said that a classical example of the internal Kan complex definition of oo-groupoid are Lie oo-groupoids, but then at Lie infinity-groupoid there is no trace of the internal Kan complex definition.

]]>