if I implement Category as idris interface, how should I implement production of Category ? it seems like a function take two interfaces and return an interface, thus interface need to be first class object to implement production this way. my repo of Category is here :: https://github.com/xieyuheng/idris-category/blob/master/Category.idr [For admin and other information see: http://www.mta.ca/~cat-dist/ ]