# cat

Cat package contains precategory and category definition from HoTT book.

## precategory

Precategory defined as set of $hom_A(a,b)$ where $a,b:A$ are objects defined by its $id$ arrows. Properfies of left and right units included with composition c and its associativity.

More formal, precategory $A$ consists of the following. (i) A type $A_0$, whose elements are called objects. We write $a: A$ for $a: A_0$. (ii) For each $a,b: A$, a set $hom_A(a,b)$, whose elements are called arrows or morphisms. (iii) For each $a: A$, a morphism $1_a : hom_A(a,a)$, called the identity morphism. (iv) For each $a,b,c: A$, a function $hom_A(b,c) \rightarrow hom_A(a,b) \rightarrow hom_A(a,c)$ called composition, and denoted $g \circ f$. (v) For each $a,b: A$ and $f: hom_A(a,b)$, we have $f = 1_b \circ f$ and $f = f \circ 1_a$. (vi) For each $a,b,c,d: A$ and $f: hom_A(a,b)$, $g: hom_A(b,c)$, $h: homA(c,d)$, we have $h \circ (g \circ f ) = (h \circ g) \circ f$.

```
cat: U = (A: U) * (A -> A -> U)
isPrecategory (C: cat): U
= (id: (x: C.1) -> C.2 x x)
* (c: (x y z: C.1) -> C.2 x y -> C.2 y z -> C.2 x z)
* (homSet: (x y: C.1) -> isSet (C.2 x y))
* (left: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x x y (id x) f) f)
* (right: (x y: C.1) -> (f: C.2 x y) -> Path (C.2 x y) (c x y y f (id y)) f)
* ( (x y z w: C.1) -> (f: C.2 x y) -> (g: C.2 y z) -> (h: C.2 z w) ->
Path (C.2 x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))
precategory: U = (C: cat) * isPrecategory C
```

Accessors of the precategory structure.

```
carrier (C: precategory): U = C.1.1
hom (C: precategory) (a b: carrier C): U = C.1.2 a b
path (C: precategory) (x: carrier C): hom C x x = C.2.1 x
compose (C: precategory) (x y z: carrier C)
(f: hom C x y) (g: hom C y z): hom C x z = C.2.2.1 x y z f g
```

## iso

A morphism f : $hom_A(a,b)$ is an iso
if there is a morphism g : hom_{A}(b,a) such that
$1_a =_\eta g \circ f$ and
$f \circ g =_\epsilon 1_b = g$. "f is iso" is
a mere proposition.

If A is a precategory and $a,b: A$, then $a = b \rightarrow iso_A(a,b)$ (idtoiso).

```
iso (C: precategory) (A B: carrier C): U
= (f: hom C A B)
* (g: hom C B A)
* (eta: Path (hom C A A) (compose C A B A f g) (path C A))
* (Path (hom C B B) (compose C B A B g f) (path C B))
```

## category

A category is a precategory such that for all $a,b:A$, the function idtoiso is an equivalence.

```
isCategory (C: precategory): U
= (A: carrier C) ->
isContr ((B: carrier C) * iso C A B)
category: U = (C: precategory) * isCategory C
```