Cat package contains precategory and category definition from HoTT book.


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


A morphism f : $hom_A(a,b)$ is an iso if there is a morphism g : homA(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))


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