Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

Cartesian Categories


Czeslaw Bylinski
Warsaw University, Bialystok

Summary.

We define and prove some simple facts on Cartesian categories and its duals co-Cartesian categories. The Cartesian category is defined as a category with the fixed terminal object, the fixed projections, and the binary products. Category $C$ has finite products if and only if $C$ has a terminal object and for every pair $a, b$ of objects of $C$ the product $a\times b$ exists. We say that a category $C$ has a finite product if every finite family of objects of $C$ has a product. Our work is based on ideas of [10], where the algebraic properties of the proof theory are investigated. The terminal object of a Cartesian category $C$ is denoted by $\hbox{\bf 1}_C$. The binary product of $a$ and $b$ is written as $a\times b$. The projections of the product are written as $pr_1(a,b)$ and as $pr_2(a,b)$. We define the products $f\times g$ of arrows $f: a\rightarrow a'$ and $g: b\rightarrow b'$ as $:a\times b\rightarrow a'\times b'$.\par Co-Cartesian category is defined dually to the Cartesian category. Dual to a terminal object is an initial object, and to products are coproducts. The initial object of a Cartesian category $C$ is written as $\hbox{\bf 0}_C$. Binary coproduct of $a$ and $b$ is written as $a+b$. Injections of the coproduct are written as $in_1(a,b)$ and as $in_2(a,b)$.

MML Identifier: CAT_4

The terminology and notation used in this paper have been introduced in the following articles [12] [5] [13] [8] [11] [14] [2] [3] [9] [1] [6] [4] [7]

Contents (PDF format)

  1. Preliminaries
  2. Cartesian Categories
  3. Co-Cartesian Categories

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Introduction to categories and functors. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[7] Czeslaw Bylinski. Products and coproducts in categories. Journal of Formalized Mathematics, 4, 1992.
[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[9] Michal Muzalewski and Wojciech Skaba. From loops to abelian multiplicative groups with zero. Journal of Formalized Mathematics, 2, 1990.
[10] M. E. Szabo. \em Algebra of Proofs. North Holland, 1978.
[11] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[12] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[13] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[14] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received October 27, 1992


[ Download a postscript version, MML identifier index, Mizar home page]