Where can I find or could you provide the definition of a category using dependent types?

Question

https://en.wikipedia.org/wiki/Dependent_type

I would prefer though Coq code.

Is this the only (quality) option:

https://github.com/HoTT/HoTT/tree/master/theories/Categories ?

But I don't understand HoTT, so would it be too difficult to use that HoTT library, or could I learn a little bit of HoTT and be okay?

One reason why that would be a bad idea is I would have to translate the Coq code into Python 3.x which has a dependent types feature, which I'm going to use for something.

Answer 1

Here you can find a complete definition of category in a dependent type theory.

In summary it is an element of a $\Sigma$-type, or a record if you prefer, made of:

• a type $Obj$ whose elements are the objects
• a dependent type $\hom \colon Obj \times Obj \to \mathbf{Type}$
• a dependent function $\circ \colon \prod_{x,y,z \colon Obj} \hom(y,z) \times \hom(x,y) \to \hom(x,z)$ (in the uncurried version)
• a dependent function $1 \colon \prod_{x \colon Obj} \hom(x,x)$
• a proof $ass \colon \prod_{x,y,z,w} \prod_{f \colon \hom(x,y),g\colon \hom(y,z),h\colon \hom(z,w)} h \circ (g \circ f) = (h \circ g) \circ f$
• proofs for the left and right unit $left-unit \colon \prod_{x,y}\prod_{f\colon\hom(x,y)} f \circ 1_x = f$ and $right-unit \colon \prod_{x,y}\prod_{f\colon\hom(x,y)} 1_y \circ f= f$.

This can be easily implemented in any programming language/proof assistant with dependent types with an equality type (not necessarily HoTT).

Hope this helps.