:PROPERTIES: :ID: 6ac2146d-0b78-40f0-a546-9322e5f1e9f0 :mtime: 20240111105923 20240109115253 :ctime: 20240109115213 :END: #+title: Category of Computable Functions #+filetags: :public:project: * Category of Computable Functions Computable functions form a [[id:12d70e9c-5793-47b3-8db0-8bc83c0f3925][Category]]. To verify this fact, let us check the requirements of being a [[id:12d70e9c-5793-47b3-8db0-8bc83c0f3925][Category]]. 1) The objects are types $Obj = Type$ 2) The arrows are computable functions $\cdot \rightsquigarrow \cdot = \cdot \to \cdot$ 3) The identity arrow is the identity function \[id(x) = x\] 4) categorical composition is function composition \[ \forall (f : A \to B) (g : B \to C) \qquad (f \gg g)(x) = g(f(x))\] And the constraints are satisfied as well 1) Associativity is true by reflexivity 2) identity cancellation is true, trivially.