<p>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:</p>

<ul>
<li>a type of objects with equivalence relation (Obj : Set)</li>
<li>a type of arrows between two objects with equivalence relation on it (Hom : Obj -> Obj -> Set)</li>
<li>a set of category operations (i.e. id : (O : Obj) -> Hom O O, and composition)</li>
<li>a proof that these operations respect equivalence relations</li>
</ul>

<p>I defined simple notions of category theory with such a definitions, i.e. terminal objects, functors and I feel that everything looks fine. </p>

<p>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".</p>

<p>What's wrong with this? What should be added? Is there any name for such a structure?</p>

CC BY-SA 3.0
2015-05-07T03:41:06.663Z
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
CC BY-SA 3.0
2015-05-07T04:33:50.837Z
@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
CC BY-SA 3.0
2015-05-07T19:18:52.693Z
I posted the same question to HoTT Cafe and got an interesting replies: https://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
CC BY-SA 3.0
2015-05-08T04:27:29.407Z
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
CC BY-SA 3.0
2015-05-08T08:14:16.553Z
Does http://arxiv.org/pdf/1408.1364.pdf answer your question?
Kai
CC BY-SA 3.0
2015-05-08T17:33:00.333Z
@Kai Yes, this article is exactly what I wanted.
Konstantin Solomatov
<type-theory><ct.category-theory><homotopy-type-theory>
Category theory in plain MLTT
Konstantin Solomatov
# Category theory in plain MLTT

(Asked by: username_0 on 2015-05-06)

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?

**Tags:** type-theory, ct.category-theory, homotopy-type-theory

> **Comments:**
> **username_1**: 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.  
> **username_0**: @MikeShulman But how can I do this? The only things that comes to my mind is to add "identity" arrows between equivalent objects.  
> **username_0**: I posted the same question to HoTT Cafe and got an interesting replies: https://groups.google.com/forum/#!topic/hott-cafe/RWcbIWiClNA However, I don't understand them so well that I will write an answer myself.  
> **username_1**: I don't know what you mean by "how can I do this?"  *Omitting* something is easy, you just don't write it down.  (-:  
> **username_2**: Does http://arxiv.org/pdf/1408.1364.pdf answer your question?  
> **username_0**: @username_2 Yes, this article is exactly what I wanted.  

---

## 0 answers

