> You can't express a category of categories, with isomorphic categories considered equal in this way. Not sure why you think that. It's a straight-forward con

> You can't express a category of categories, with isomorphic categories considered equal in this way. Not sure why you think that. It's a straight-forward construction within this framework and even part of the development[1]. [1] https://github.com/jwiegley/category-theory/blob/master/Instance/Cat.v https://github.com/jwiegley/category-theory/blob/master/Inst...