Internal groupoid

An internal groupoid in a category is a groupoid object: its objects, arrows, source, target, identity, composition, and inversion are objects and morphisms in the ambient category and satisfy the groupoid identities diagrammatically.

For a reflexive pair $f,g:A\rightrightarrows B$ with section $r$ in a preadditive category, each hom-set diagram defines a groupoid. Arrows $a,b:C\to A$ compose when $ga=fb$, by $b\circ a=a+b-rga$. Identity at $x:C\to B$ is $rx$, and the inverse of $a$ is $rfa+rga-a$. Bilinearity proves the endpoint, identity and associativity laws and compatibility with precomposition in $C$. In the hom-set formulation this does not assume that the composable-arrow pullback exists.

If $f,g:A\rightrightarrows B$ have common splitting $r$ in an additive category, define the composite of $x,y:C\to A$ with $gx=fy$ byThe identity at $b:C\to B$ is $rb$, and the inverse of $x$ is $rfx+rgx-x$. These formulas make the reflexive pair an internal groupoid.