Internal categories in Set are ordinary small categories

The theorem asserts the conjunction of two statements. First, let $A,O$ be arbitrary types, and let $s,t:A\to O$, $i:O\to A$, and $c:A\times A\to A$ be total functions satisfying $s(i(x))=t(i(x))=x$ for every $x\in O$; $s(c(g,f))=s(f)$ and $t(c(g,f))=t(g)$ whenever $t(f)=s(g)$; $c(i(t(f)),f)=f$ and $c(f,i(s(f)))=f$ for every $f\in A$; and $c(h,c(g,f))=c(c(h,g),f)$ whenever $t(f)=s(g)$ and $t(g)=s(h)$. Give $O$ the category whose morphisms $x\to y$ are elements $f\in A$ equipped with $s(f)=x$ and $t(f)=y$, whose identities are $i(x)$, and whose composition is induced by $c$. Let $T$ be the type of triples $(x,y,f)$ with $f:x\to y$ in this category, and let $q:A\to T$ be the bijection $q(a)=(s(a),t(a),a)$, where the last component includes its endpoint equalities. On $T$, define $S(x,y,f)=x$, $T_{\!o}(x,y,f)=y$, $I(x)=(x,x,\mathrm{id}_x)$, and define $C(\beta,\alpha)$, for $\alpha=(x,y,f)$ and $\beta=(z,w,g)$, to be $(x,w,f\text{ followed by the equality arrow }y\to z\text{ followed by }g)$ if $y=z$, and to be $\alpha$ otherwise. Then $S(q(a))=s(a)$ and $T_{\!o}(q(a))=t(a)$ for every $a$, $I(x)=q(i(x))$ for every $x$, and $C(q(g),q(f))=q(c(g,f))$ whenever $t(f)=s(g)$. Second, for every category with object type $O$, form its type of all morphism triples and the same maps $S,T_{\!o},I,C$, including the rule that composition returns its second argument when the endpoints do not match. These maps satisfy all the source, target, identity, and conditional associativity equations listed above; moreover $I(x)=(x,x,\mathrm{id}_x)$, $C((y,z,g),(x,y,f))=(x,z,g\circ f)$ for every $f:x\to y$ and $g:y\to z$, and the underlying triple of the image of $f:x\to y$ under the endpoint-restricted bijection is $(x,y,f)$. Empty types and empty morphism sets are allowed wherever the stated data exist; the composition-preservation assertions apply only when the specified endpoints match.