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 relationsI 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?
Category theory in plain MLTT
type theory;ct.category theory;homotopy type theory