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 coCartesian 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
CoCartesian 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]

Preliminaries

Cartesian Categories

CoCartesian 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]