I would like to employ some basic category theory as a background for a PVS
specification. My question is wether anybody has done some Category Theory in PVS. I couldn't find anything.
Personally, I'm pretty much at a loss of how to explain to PVS what a Functor and a category is.
Any help would be appreciated.