CatDat

Implication Details

Assumptions: groupoidone-way

Conclusions: thin

Reason: If f,g:ABf,g : A \rightrightarrows B are two morphisms, then f1g:AAf^{-1} \circ g : A \to A must be the identity, so that f=gf = g.