Categories without Uniqueness of cod and dom
Andrzej Trybulec · 1996
Summary. Category theory had been formalized in Mizar quite early [6]. This had been done closely to the handbook of S. McLane [10]. In this paper we use a different approach. Category is a triple 〈O,{〈o1,o2〉} o1,o2∈O,{◦o1,o2,o3} o1,o2,o3∈O 〉 where ◦o1,o2,o3: 〈o2,o3 〉 × 〈o1,o2 〉 → 〈o1,o3 〉 that satisfies usual conditions (associativity and the existence of the identities). This approach is closer to the way in which categories are presented in homological algebra (e.g. [1], pp.58-59). We do not assume that 〈o1,o2〉’s are mutually disjoint. If f is simultaneously a morphism from o1 to o2 and o ′ 1 to o2 (o1 � = o ′ 1) than different compositions are used (◦o1,o2,o3 or ◦o ′ 1,o2,o3) to compose it with a morphism g from o2 to o3. The operation g · f has actually six arguments (two visible and four hidden: three objects and the category). We introduce some simple properties of categories. Perhaps more than necessary. It is partially caused by the formalization. The functional categories are characterized by the following properties: • quasi-functional that means that morphisms are functions (rather meaningless, if it stands alone) • semi-functional that means that the composition of morphism is the composition of functions, provided they are functions. • pseudo-functional that means that the composition of morphisms is the composition of functions. For categories pseudo-functional is just quasi-functional and semi-functional, but we work in a bit more general setting. Similarly the concept of a discrete category is split into two: • quasi-discrete that means that 〈o1,o2 〉 is empty for o1 � = o2 and • pseudo-discrete that means that 〈o,o 〉 is trivial, i.e. consists of the identity only, in a category. We plan to follow Semadeni-Wiweger book [13], in the development the category theory in Mizar. However, the beginning is not very close to [13], because of the approach adopted and because we work in Tarski-Grothendieck set theory.