CatDat

Implication Details

Assumptions: left cancellativezero morphisms

Conclusions: thin

Reason: If f,g:ABf,g : A \to B are two morphisms, then 0B,Bf=0A,B=0B,Bg0_{B,B} \circ f = 0_{A,B} = 0_{B,B} \circ g, so that f=gf = g.