[Agda] formalization of category theory

kahl at cas.mcmaster.ca kahl at cas.mcmaster.ca
Thu Jun 17 16:12:24 CEST 2010


Vag Vagoff wrote:

 > It is more convenient to define category without mentioning objects:

I find the version with objects ``more typed''.
I feel absolutely no need to be able to write down undefined compositions.


Wolfram


More information about the Agda mailing list