set M = MapsC X;
set d = CDom X;
set c = CCod X;
set p = CComp X;
set C = CohCat X;
thus A1:
CohCat X is Category-like
( CohCat X is transitive & CohCat X is associative & CohCat X is reflexive )
thus A2:
CohCat X is transitive
( CohCat X is associative & CohCat X is reflexive )proof
let ff,
gg be
Morphism of
(CohCat X);
CAT_1:def 7 ( not dom gg = cod ff or ( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg ) )
assume A3:
dom gg = cod ff
;
( dom (gg (*) ff) = dom ff & cod (gg (*) ff) = cod gg )
[gg,ff] in dom the
Comp of
(CohCat X)
by A3, A1;
then A4:
the
Comp of
(CohCat X) . (
gg,
ff)
= gg (*) ff
by CAT_1:def 1;
reconsider f =
ff,
g =
gg as
Element of
MapsC X ;
A5:
(
(CDom X) . g = dom g &
(CCod X) . f = cod f )
by Def11, Def12;
then A6:
(CComp X) . [g,f] = g * f
by A3, Def13;
A7:
(
(CDom X) . f = dom f &
(CCod X) . g = cod g )
by Def11, Def12;
(
dom (g * f) = dom f &
cod (g * f) = cod g )
by A3, A5, Th22;
hence
(
dom (gg (*) ff) = dom ff &
cod (gg (*) ff) = cod gg )
by A6, A7, Def11, Def12, A4;
verum
end;
thus
CohCat X is associative
CohCat X is reflexive proof
let ff,
gg,
hh be
Morphism of
(CohCat X);
CAT_1:def 8 ( not dom hh = cod gg or not dom gg = cod ff or hh (*) (gg (*) ff) = (hh (*) gg) (*) ff )
assume that A8:
dom hh = cod gg
and A9:
dom gg = cod ff
;
hh (*) (gg (*) ff) = (hh (*) gg) (*) ff
reconsider f =
ff,
g =
gg,
h =
hh as
Element of
MapsC X ;
A10:
(
dom h = (CDom X) . h &
cod g = (CCod X) . g )
by Def11, Def12;
then A11:
dom (h * g) = dom g
by A8, Th22;
A12:
(
dom g = (CDom X) . g &
cod f = (CCod X) . f )
by Def11, Def12;
then A13:
cod (g * f) = dom h
by A8, A9, A10, Th22;
[hh,gg] in dom the
Comp of
(CohCat X)
by A1, A8;
then A14:
hh (*) gg = the
Comp of
(CohCat X) . (
hh,
gg)
by CAT_1:def 1;
dom (hh (*) gg) = dom gg
by A2, A8;
then A15:
[(hh (*) gg),ff] in dom the
Comp of
(CohCat X)
by A1, A9;
[gg,ff] in dom the
Comp of
(CohCat X)
by A1, A9;
then A16:
gg (*) ff = the
Comp of
(CohCat X) . (
gg,
ff)
by CAT_1:def 1;
cod (gg (*) ff) = cod gg
by A2, A9;
then
[hh,(gg (*) ff)] in dom the
Comp of
(CohCat X)
by A1, A8;
hence hh (*) (gg (*) ff) =
the
Comp of
(CohCat X) . (
hh,
( the Comp of (CohCat X) . (gg,ff)))
by A16, CAT_1:def 1
.=
(CComp X) . [h,(g * f)]
by A9, A12, Def13
.=
h * (g * f)
by A13, Def13
.=
(h * g) * f
by A8, A9, A10, A12, Th23
.=
(CComp X) . [(h * g),f]
by A9, A12, A11, Def13
.=
the
Comp of
(CohCat X) . (
( the Comp of (CohCat X) . (hh,gg)),
ff)
by A8, A10, Def13
.=
(hh (*) gg) (*) ff
by A14, A15, CAT_1:def 1
;
verum
end;
let a be Object of (CohCat X); CAT_1:def 9 not Hom (a,a) = {}
reconsider aa = a as Element of CSp X ;
reconsider ii = id$ aa as Morphism of (CohCat X) ;
A17: cod ii =
cod (id$ aa)
by Def12
.=
aa
;
dom ii =
dom (id$ aa)
by Def11
.=
aa
;
then
id$ aa in Hom (a,a)
by A17;
hence
Hom (a,a) <> {}
; verum