:: Comma Category
:: by Grzegorz Bancerek and Agata Darmochwa\l
::
:: Received February 20, 1992
:: Copyright (c) 1992 Association of Mizar Users
begin
deffunc
H
1
(
CatStr
)
->
set
= the
carrier
of $1;
deffunc
H
2
(
CatStr
)
->
set
= the
carrier'
of $1;
definition
canceled;
canceled;
canceled;
canceled;
end;
::
deftheorem
COMMACAT:def 1 :
canceled;
::
deftheorem
COMMACAT:def 2 :
canceled;
::
deftheorem
COMMACAT:def 3 :
canceled;
::
deftheorem
COMMACAT:def 4 :
canceled;
theorem
:: COMMACAT:1
canceled;
definition
let
C
,
D
,
E
be
Category
;
let
F
be
Functor
of
C
,
E
;
let
G
be
Functor
of
D
,
E
;
given
c1
being
Object
of ,
d1
being
Object
of ,
f1
being
Morphism
of
such that
A1
:
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
;
func
commaObjs
F
,
G
->
non
empty
Subset
of
equals
:
Def5
:
:: COMMACAT:def 5
{
[
[
c
,
d
]
,
f
]
where
c
is
Object
of ,
d
is
Object
of ,
f
is
Morphism
of :
f
in
Hom
(
F
.
c
)
,
(
G
.
d
)
}
;
coherence
{
[
[
c
,
d
]
,
f
]
where
c
is
Object
of ,
d
is
Object
of ,
f
is
Morphism
of :
f
in
Hom
(
F
.
c
)
,
(
G
.
d
)
}
is non
empty
Subset
of
proof
end;
end;
::
deftheorem
Def5
defines
commaObjs
COMMACAT:def 5 :
for
C
,
D
,
E
being
Category
for
F
being
Functor
of
C
,
E
for
G
being
Functor
of
D
,
E
st ex
c1
being
Object
of ex
d1
being
Object
of ex
f1
being
Morphism
of st
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
holds
commaObjs
F
,
G
=
{
[
[
c
,
d
]
,
f
]
where
c
is
Object
of ,
d
is
Object
of ,
f
is
Morphism
of :
f
in
Hom
(
F
.
c
)
,
(
G
.
d
)
}
;
theorem
Th2
:
:: COMMACAT:2
for
C
,
D
,
E
being
Category
for
F
being
Functor
of
C
,
E
for
G
being
Functor
of
D
,
E
for
o
being
Element
of
commaObjs
F
,
G
st ex
c
being
Object
of ex
d
being
Object
of ex
f
being
Morphism
of st
f
in
Hom
(
F
.
c
)
,
(
G
.
d
)
holds
(
o
=
[
[
(
o
`11
)
,
(
o
`12
)
]
,
(
o
`2
)
]
&
o
`2
in
Hom
(
F
.
(
o
`11
)
)
,
(
G
.
(
o
`12
)
)
&
dom
(
o
`2
)
=
F
.
(
o
`11
)
&
cod
(
o
`2
)
=
G
.
(
o
`12
)
)
proof
end;
definition
let
C
,
D
,
E
be
Category
;
let
F
be
Functor
of
C
,
E
;
let
G
be
Functor
of
D
,
E
;
given
c1
being
Object
of ,
d1
being
Object
of ,
f1
being
Morphism
of
such that
A1
:
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
;
func
commaMorphs
F
,
G
->
non
empty
Subset
of
equals
:
Def6
:
:: COMMACAT:def 6
{
[
[
o1
,
o2
]
,
[
g
,
h
]
]
where
g
is
Morphism
of ,
h
is
Morphism
of ,
o1
,
o2
is
Element
of
commaObjs
F
,
G
: (
dom
g
=
o1
`11
&
cod
g
=
o2
`11
&
dom
h
=
o1
`12
&
cod
h
=
o2
`12
&
(
o2
`2
)
*
(
F
.
g
)
=
(
G
.
h
)
*
(
o1
`2
)
)
}
;
coherence
{
[
[
o1
,
o2
]
,
[
g
,
h
]
]
where
g
is
Morphism
of ,
h
is
Morphism
of ,
o1
,
o2
is
Element
of
commaObjs
F
,
G
: (
dom
g
=
o1
`11
&
cod
g
=
o2
`11
&
dom
h
=
o1
`12
&
cod
h
=
o2
`12
&
(
o2
`2
)
*
(
F
.
g
)
=
(
G
.
h
)
*
(
o1
`2
)
)
}
is non
empty
Subset
of
proof
end;
end;
::
deftheorem
Def6
defines
commaMorphs
COMMACAT:def 6 :
for
C
,
D
,
E
being
Category
for
F
being
Functor
of
C
,
E
for
G
being
Functor
of
D
,
E
st ex
c1
being
Object
of ex
d1
being
Object
of ex
f1
being
Morphism
of st
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
holds
commaMorphs
F
,
G
=
{
[
[
o1
,
o2
]
,
[
g
,
h
]
]
where
g
is
Morphism
of ,
h
is
Morphism
of ,
o1
,
o2
is
Element
of
commaObjs
F
,
G
: (
dom
g
=
o1
`11
&
cod
g
=
o2
`11
&
dom
h
=
o1
`12
&
cod
h
=
o2
`12
&
(
o2
`2
)
*
(
F
.
g
)
=
(
G
.
h
)
*
(
o1
`2
)
)
}
;
definition
let
C
,
D
,
E
be
Category
;
let
F
be
Functor
of
C
,
E
;
let
G
be
Functor
of
D
,
E
;
let
k
be
Element
of
commaMorphs
F
,
G
;
:: original:
`11
redefine
func
k
`11
->
Element
of
commaObjs
F
,
G
;
coherence
k
`11
is
Element
of
commaObjs
F
,
G
proof
end;
:: original:
`12
redefine
func
k
`12
->
Element
of
commaObjs
F
,
G
;
coherence
k
`12
is
Element
of
commaObjs
F
,
G
proof
end;
end;
theorem
Th3
:
:: COMMACAT:3
for
C
,
D
,
E
being
Category
for
F
being
Functor
of
C
,
E
for
G
being
Functor
of
D
,
E
for
k
being
Element
of
commaMorphs
F
,
G
st ex
c
being
Object
of ex
d
being
Object
of ex
f
being
Morphism
of st
f
in
Hom
(
F
.
c
)
,
(
G
.
d
)
holds
(
k
=
[
[
(
k
`11
)
,
(
k
`12
)
]
,
[
(
k
`21
)
,
(
k
`22
)
]
]
&
dom
(
k
`21
)
=
(
k
`11
)
`11
&
cod
(
k
`21
)
=
(
k
`12
)
`11
&
dom
(
k
`22
)
=
(
k
`11
)
`12
&
cod
(
k
`22
)
=
(
k
`12
)
`12
&
(
(
k
`12
)
`2
)
*
(
F
.
(
k
`21
)
)
=
(
G
.
(
k
`22
)
)
*
(
(
k
`11
)
`2
)
)
proof
end;
definition
let
C
,
D
,
E
be
Category
;
let
F
be
Functor
of
C
,
E
;
let
G
be
Functor
of
D
,
E
;
let
k1
,
k2
be
Element
of
commaMorphs
F
,
G
;
given
c1
being
Object
of ,
d1
being
Object
of ,
f1
being
Morphism
of
such that
A1
:
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
;
assume
A2
:
k1
`12
=
k2
`11
;
func
k2
*
k1
->
Element
of
commaMorphs
F
,
G
equals
:
Def7
:
:: COMMACAT:def 7
[
[
(
k1
`11
)
,
(
k2
`12
)
]
,
[
(
(
k2
`21
)
*
(
k1
`21
)
)
,
(
(
k2
`22
)
*
(
k1
`22
)
)
]
]
;
coherence
[
[
(
k1
`11
)
,
(
k2
`12
)
]
,
[
(
(
k2
`21
)
*
(
k1
`21
)
)
,
(
(
k2
`22
)
*
(
k1
`22
)
)
]
]
is
Element
of
commaMorphs
F
,
G
proof
end;
end;
::
deftheorem
Def7
defines
*
COMMACAT:def 7 :
for
C
,
D
,
E
being
Category
for
F
being
Functor
of
C
,
E
for
G
being
Functor
of
D
,
E
for
k1
,
k2
being
Element
of
commaMorphs
F
,
G
st ex
c1
being
Object
of ex
d1
being
Object
of ex
f1
being
Morphism
of st
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
&
k1
`12
=
k2
`11
holds
k2
*
k1
=
[
[
(
k1
`11
)
,
(
k2
`12
)
]
,
[
(
(
k2
`21
)
*
(
k1
`21
)
)
,
(
(
k2
`22
)
*
(
k1
`22
)
)
]
]
;
definition
let
C
,
D
,
E
be
Category
;
let
F
be
Functor
of
C
,
E
;
let
G
be
Functor
of
D
,
E
;
func
commaComp
F
,
G
->
PartFunc
of ,
means
:
Def8
:
:: COMMACAT:def 8
(
dom
it
=
{
[
k1
,
k2
]
where
k1
,
k2
is
Element
of
commaMorphs
F
,
G
:
k1
`11
=
k2
`12
}
& ( for
k
,
k'
being
Element
of
commaMorphs
F
,
G
st
[
k
,
k'
]
in
dom
it
holds
it
.
[
k
,
k'
]
=
k
*
k'
) );
existence
ex
b
1
being
PartFunc
of , st
(
dom
b
1
=
{
[
k1
,
k2
]
where
k1
,
k2
is
Element
of
commaMorphs
F
,
G
:
k1
`11
=
k2
`12
}
& ( for
k
,
k'
being
Element
of
commaMorphs
F
,
G
st
[
k
,
k'
]
in
dom
b
1
holds
b
1
.
[
k
,
k'
]
=
k
*
k'
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of , st
dom
b
1
=
{
[
k1
,
k2
]
where
k1
,
k2
is
Element
of
commaMorphs
F
,
G
:
k1
`11
=
k2
`12
}
& ( for
k
,
k'
being
Element
of
commaMorphs
F
,
G
st
[
k
,
k'
]
in
dom
b
1
holds
b
1
.
[
k
,
k'
]
=
k
*
k'
) &
dom
b
2
=
{
[
k1
,
k2
]
where
k1
,
k2
is
Element
of
commaMorphs
F
,
G
:
k1
`11
=
k2
`12
}
& ( for
k
,
k'
being
Element
of
commaMorphs
F
,
G
st
[
k
,
k'
]
in
dom
b
2
holds
b
2
.
[
k
,
k'
]
=
k
*
k'
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def8
defines
commaComp
COMMACAT:def 8 :
for
C
,
D
,
E
being
Category
for
F
being
Functor
of
C
,
E
for
G
being
Functor
of
D
,
E
for
b
6
being
PartFunc
of , holds
(
b
6
=
commaComp
F
,
G
iff (
dom
b
6
=
{
[
k1
,
k2
]
where
k1
,
k2
is
Element
of
commaMorphs
F
,
G
:
k1
`11
=
k2
`12
}
& ( for
k
,
k'
being
Element
of
commaMorphs
F
,
G
st
[
k
,
k'
]
in
dom
b
6
holds
b
6
.
[
k
,
k'
]
=
k
*
k'
) ) );
definition
let
C
,
D
,
E
be
Category
;
let
F
be
Functor
of
C
,
E
;
let
G
be
Functor
of
D
,
E
;
given
c1
being
Object
of ,
d1
being
Object
of ,
f1
being
Morphism
of
such that
A1
:
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
;
func
F
comma
G
->
strict
Category
means
:: COMMACAT:def 9
( the
carrier
of
it
=
commaObjs
F
,
G
& the
carrier'
of
it
=
commaMorphs
F
,
G
& ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Source
of
it
.
k
=
k
`11
) & ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Target
of
it
.
k
=
k
`12
) & ( for
o
being
Element
of
commaObjs
F
,
G
holds the
Id
of
it
.
o
=
[
[
o
,
o
]
,
[
(
id
(
o
`11
)
)
,
(
id
(
o
`12
)
)
]
]
) & the
Comp
of
it
=
commaComp
F
,
G
);
existence
ex
b
1
being
strict
Category
st
( the
carrier
of
b
1
=
commaObjs
F
,
G
& the
carrier'
of
b
1
=
commaMorphs
F
,
G
& ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Source
of
b
1
.
k
=
k
`11
) & ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Target
of
b
1
.
k
=
k
`12
) & ( for
o
being
Element
of
commaObjs
F
,
G
holds the
Id
of
b
1
.
o
=
[
[
o
,
o
]
,
[
(
id
(
o
`11
)
)
,
(
id
(
o
`12
)
)
]
]
) & the
Comp
of
b
1
=
commaComp
F
,
G
)
proof
end;
uniqueness
for
b
1
,
b
2
being
strict
Category
st the
carrier
of
b
1
=
commaObjs
F
,
G
& the
carrier'
of
b
1
=
commaMorphs
F
,
G
& ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Source
of
b
1
.
k
=
k
`11
) & ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Target
of
b
1
.
k
=
k
`12
) & ( for
o
being
Element
of
commaObjs
F
,
G
holds the
Id
of
b
1
.
o
=
[
[
o
,
o
]
,
[
(
id
(
o
`11
)
)
,
(
id
(
o
`12
)
)
]
]
) & the
Comp
of
b
1
=
commaComp
F
,
G
& the
carrier
of
b
2
=
commaObjs
F
,
G
& the
carrier'
of
b
2
=
commaMorphs
F
,
G
& ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Source
of
b
2
.
k
=
k
`11
) & ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Target
of
b
2
.
k
=
k
`12
) & ( for
o
being
Element
of
commaObjs
F
,
G
holds the
Id
of
b
2
.
o
=
[
[
o
,
o
]
,
[
(
id
(
o
`11
)
)
,
(
id
(
o
`12
)
)
]
]
) & the
Comp
of
b
2
=
commaComp
F
,
G
holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
defines
comma
COMMACAT:def 9 :
for
C
,
D
,
E
being
Category
for
F
being
Functor
of
C
,
E
for
G
being
Functor
of
D
,
E
st ex
c1
being
Object
of ex
d1
being
Object
of ex
f1
being
Morphism
of st
f1
in
Hom
(
F
.
c1
)
,
(
G
.
d1
)
holds
for
b
6
being
strict
Category
holds
(
b
6
=
F
comma
G
iff ( the
carrier
of
b
6
=
commaObjs
F
,
G
& the
carrier'
of
b
6
=
commaMorphs
F
,
G
& ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Source
of
b
6
.
k
=
k
`11
) & ( for
k
being
Element
of
commaMorphs
F
,
G
holds the
Target
of
b
6
.
k
=
k
`12
) & ( for
o
being
Element
of
commaObjs
F
,
G
holds the
Id
of
b
6
.
o
=
[
[
o
,
o
]
,
[
(
id
(
o
`11
)
)
,
(
id
(
o
`12
)
)
]
]
) & the
Comp
of
b
6
=
commaComp
F
,
G
) );
theorem
:: COMMACAT:4
for
y
,
x
being
set
holds
( the
carrier
of
(
1Cat
x
,
y
)
=
{
x
}
& the
carrier'
of
(
1Cat
x
,
y
)
=
{
y
}
) ;
theorem
Th5
:
:: COMMACAT:5
for
y
,
x
being
set
for
a
,
b
being
Object
of holds
Hom
a
,
b
=
{
y
}
proof
end;
definition
let
C
be
Category
;
let
c
be
Object
of ;
func
1Cat
c
->
strict
Subcategory
of
C
equals
:: COMMACAT:def 10
1Cat
c
,
(
id
c
)
;
coherence
1Cat
c
,
(
id
c
)
is
strict
Subcategory
of
C
proof
end;
end;
::
deftheorem
defines
1Cat
COMMACAT:def 10 :
for
C
being
Category
for
c
being
Object
of holds
1Cat
c
=
1Cat
c
,
(
id
c
)
;
definition
let
C
be
Category
;
let
c
be
Object
of ;
func
c
comma
C
->
strict
Category
equals
:: COMMACAT:def 11
(
incl
(
1Cat
c
)
)
comma
(
id
C
)
;
coherence
(
incl
(
1Cat
c
)
)
comma
(
id
C
)
is
strict
Category
;
func
C
comma
c
->
strict
Category
equals
:: COMMACAT:def 12
(
id
C
)
comma
(
incl
(
1Cat
c
)
)
;
coherence
(
id
C
)
comma
(
incl
(
1Cat
c
)
)
is
strict
Category
;
end;
::
deftheorem
defines
comma
COMMACAT:def 11 :
for
C
being
Category
for
c
being
Object
of holds
c
comma
C
=
(
incl
(
1Cat
c
)
)
comma
(
id
C
)
;
::
deftheorem
defines
comma
COMMACAT:def 12 :
for
C
being
Category
for
c
being
Object
of holds
C
comma
c
=
(
id
C
)
comma
(
incl
(
1Cat
c
)
)
;