Reflexive-pair groupoid formula in a preadditive category
ID: reflexive-pair-groupoid-formula-in-a-preadditive-category
For a reflexive pair with section in a preadditive category, each hom-set diagram defines a groupoid. Arrows compose when , by . Identity at is , and the inverse of is . Bilinearity proves the endpoint, identity and associativity laws and compatibility with precomposition in . In the hom-set formulation this does not assume that the composable-arrow pullback exists.
New to topics? Read the docs here!