Object-Free Definition of Categories
Category theory was formalized in Mizar with two different approaches [7], [18] that correspond to those most commonly used [16], [5]. Since there is a one-to-one correspondence between objects and identity morphisms, some authors have used an approach that does not refer to objects as elements of the theory, and are usually indicated as object-free category [1] or as arrowsonly category [16]. In this article is proposed a new definition of an object-free category, introducing the two properties:...