In agda-categories/src/Categories/Object/NaturalNumber.agda, I suggest renaming NaturalNumber to NNO (and adapt related names accordingly). It is not one number, it is really numbers, and then more accurately (and standard) would be NaturalNumberObject. But then, NNO would be better, it is also a standard abbreviation. I would rename the file to NaturalNumbers.agda, as a more suggestive name. Agreed?
JacquesCarette
commented
10 months ago
In
agda-categories/src/Categories/Object/NaturalNumber.agda, I suggest renamingNaturalNumbertoNNO(and adapt related names accordingly). It is not one number, it is really numbers, and then more accurately (and standard) would beNaturalNumberObject. But then,NNOwould be better, it is also a standard abbreviation. I would rename the file toNaturalNumbers.agda, as a more suggestive name. Agreed?