:PROPERTIES: :ID: 12d70e9c-5793-47b3-8db0-8bc83c0f3925 :mtime: 20240109113340 :ctime: 20240109112648 :END: #+title: Category #+filetags: :category-theory:public:project: * Definition of a Category In the context of category theory, a category is a type of mathematical stucture with the 4 following parts 1) A collection of *objects*, $Obj : Type$ 2) A collection of *arrows* between two objects $\cdot \rightsquigarrow \cdot : Obj \to Obj \to Type$ 3) A *identity* function $id : (X : Obj) \to X \rightsquigarrow X$ 4) A *composition* function $\cdot \gg \cdot : \{ A B C : Obj\} \to (A \rightsquigarrow B) \to (B \rightsquigarrow C) \to (A \rightsquigarrow C)$ Subject to the 2 following conditions 1) *associativity* of composition, which means that \[ \forall (A B C D : Obj) (f : A \rightsquigarrow B) (g : B \rightsquigarrow C) (h : C \rightsquigarrow D) \qquad (f \gg_{ABC} g) \gg_{ACD} h = f \gg_{ABD} (g \gg_{BCD} h) = f \gg g \gg h\] 2) *cancellation* of identity, which means that \[\forall ( A B : Obj ) (f : A \rightsquigarrow B) \qquad id_{A} \gg_{AB} f = f \gg_{AB} id_{B} = f \]