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]
-
Preliminaries
-
Cartesian Categories
-
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]