Def CategoryTheory.sum.inrCompInrCompInverseAssociator

Modification history