<abstract xmlns="http://www.w3.org/1999/xhtml"><p>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: left composable and right composable, and a simplification of the notation through a symbol, a binary relation between morphisms, that indicates whether the composition is defined. In the final part we define two functions that allow to switch from the two definitions, with and without objects, and it is shown that their composition produces isomorphic categories.</p></abstract>

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: left composable and right composable, and a simplification of the notation through a symbol, a binary relation between morphisms, that indicates whether the composition is defined. In the final part we define two functions that allow to switch from the two definitions, with and without objects, and it is shown that their composition produces isomorphic categories.

Object-Free Definition of Categories

Formalized Mathematics

{"article-title":"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...

Object-Free Definition of Categories

Data publikacji: 01 paź 2013

Zakres stron: 193 - 205

DOI: https://doi.org/10.2478/forma-2013-0021

Słowa kluczowe
object-free category, correspondence between different approaches to category

This content is open access.

Object-Free Definition of Categories

Data publikacji: 01 paź 2013

Zakres stron: 193 - 205

DOI: https://doi.org/10.2478/forma-2013-0021

Słowa kluczoweobject-free category, correspondence between different approaches to category

This content is open access.

Słowa kluczowe
object-free category, correspondence between different approaches to category