4
$\begingroup$

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?

Improve this question
$\endgroup$
6
  • 4
    $\begingroup$ 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. $\endgroup$
    – Mike Shulman
    Commented May 7, 2015 at 3:41
  • 1
    $\begingroup$ @MikeShulman But how can I do this? The only things that comes to my mind is to add "identity" arrows between equivalent objects. $\endgroup$
    – Konstantin Solomatov
    Commented May 7, 2015 at 4:33
  • 1
    $\begingroup$ 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. $\endgroup$
    – Konstantin Solomatov
    Commented May 7, 2015 at 19:18
  • $\begingroup$ I don't know what you mean by "how can I do this?" Omitting something is easy, you just don't write it down. (-: $\endgroup$
    – Mike Shulman
    Commented May 8, 2015 at 4:27
  • $\begingroup$ Does arxiv.org/pdf/1408.1364.pdf answer your question? $\endgroup$
    – Kai
    Commented May 8, 2015 at 8:14

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.