fact: Definition Group_arity (o : Group_operation) := match o with | one => nullary | mul => binary | inv => unary end.
imports: Category.Lib Category.Theory.Category Category.Structure.Terminal Category.Structure.Initial Category.Structure.Cartesian