Add opposite category
More stuff in sigma
Add unit setoid
Add Functor
add category of setoids
Reformulate (pre)sheaf in terms of functor