On internal natural isomorphisms and topological categories

Consider internal categories and in a finitely complete ambient category , and functors . Assume we have a natural transformation . To say that is a(n internal) natural isomorphism, in my 2012 paper in TAC I wrote “We say a natural transformation is a natural isomorphism if it has an inverse with respect to vertical composition”, that is to say, there is some natural transformation such that the vertical composition and . For any internal category internal to a finitely complete category we can form the pullback (the sketchy formatting is deliberate here) Y^iso_1 ---> Y_1 x_{Y_0^2} Y_1 | | | | (m,m) | | v vY_0 x Y_0 ---> Y_1 x Y_1 u^2 where the top right pullback is Y_1 x_{Y_0^2} Y_1 ---> Y_1 | | | | (s,t) | | v v Y_1 -----------> Y_0 x Y_0 (t,s) Since is a section (as is a section of both and ) it is a monomorphism, and so the projection is a monomorphism. Moreover: CLAIM: is a monomorphism. Suppose I have such that . Write and , so that we have . Since , we can do so that , and…