I want to define a category in simple MLTT (not in HoTT). I defined it with the help of setoids. I.e. category consists of:
- a type of objects with equivalence relation (Obj : Set)
- a type of arrows between two objects with equivalence relation on it (Hom : Obj -> Obj -> Set)
- a set of category operations (i.e. id : (O : Obj) -> Hom O O, and composition)
- a proof that these operations respect equivalence relations
I defined simple notions of category theory with such a definitions, i.e. terminal objects, functors and I feel that everything looks fine.
However, I feel that definitions like this isn't exactly what we want when we talk about a category. Consider objects A, B, A' and B'. Assume A is equivalent to A' and B is equivalent to B'. We assume that the structure of arrows between A and B is in some sense isomorphic to A' and B' but the foregoing definition doesn't say anything about this. As far as I understand, HoTT, would require these types of arrows to be "equivalent".
What's wrong with this? What should be added? Is there any name for such a structure?