# Category theory in plain MLTT

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?

• One option would be to simply omit the equivalence relation on Obj. With the rest of the structure you can define what it means for two objects to be isomorphic; use that as the notion of equivalence for objects. – Mike Shulman May 7 '15 at 3:41
• @MikeShulman But how can I do this? The only things that comes to my mind is to add "identity" arrows between equivalent objects. – Konstantin Solomatov May 7 '15 at 4:33
• I posted the same question to HoTT Cafe and got an interesting replies: groups.google.com/forum/#!topic/hott-cafe/RWcbIWiClNA However, I don't understand them so well that I will write an answer myself. – Konstantin Solomatov May 7 '15 at 19:18
• I don't know what you mean by "how can I do this?" Omitting something is easy, you just don't write it down. (-: – Mike Shulman May 8 '15 at 4:27
• Does arxiv.org/pdf/1408.1364.pdf answer your question? – Kai May 8 '15 at 8:14