:: by Marco Riccardi

::

:: Received October 7, 2013

:: Copyright (c) 2013-2019 Association of Mizar Users

definition

attr c_{1} is strict ;

struct CategoryStr -> 1-sorted ;

aggr CategoryStr(# carrier, composition #) -> CategoryStr ;

sel composition c_{1} -> PartFunc of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier of c_{1};

end;
struct CategoryStr -> 1-sorted ;

aggr CategoryStr(# carrier, composition #) -> CategoryStr ;

sel composition c

:: deftheorem Def2 defines are_composable CAT_6:def 2 :

for C being CategoryStr

for f1, f2 being morphism of C holds

( f1,f2 are_composable iff [f1,f2] in dom the composition of C );

for C being CategoryStr

for f1, f2 being morphism of C holds

( f1,f2 are_composable iff [f1,f2] in dom the composition of C );

notation
end;

definition

let C be CategoryStr ;

let f1, f2 be morphism of C;

assume A1: f1 |> f2 ;

correctness

coherence

the composition of C . (f1,f2) is morphism of C;

end;
let f1, f2 be morphism of C;

assume A1: f1 |> f2 ;

correctness

coherence

the composition of C . (f1,f2) is morphism of C;

proof end;

:: deftheorem Def3 defines (*) CAT_6:def 3 :

for C being CategoryStr

for f1, f2 being morphism of C st f1 |> f2 holds

f1 (*) f2 = the composition of C . (f1,f2);

for C being CategoryStr

for f1, f2 being morphism of C st f1 |> f2 holds

f1 (*) f2 = the composition of C . (f1,f2);

definition

let C be CategoryStr ;

let f be morphism of C;

end;
let f be morphism of C;

attr f is left_identity means :Def4: :: CAT_6:def 4

for f1 being morphism of C st f |> f1 holds

f (*) f1 = f1;

for f1 being morphism of C st f |> f1 holds

f (*) f1 = f1;

attr f is right_identity means :Def5: :: CAT_6:def 5

for f1 being morphism of C st f1 |> f holds

f1 (*) f = f1;

for f1 being morphism of C st f1 |> f holds

f1 (*) f = f1;

:: deftheorem Def4 defines left_identity CAT_6:def 4 :

for C being CategoryStr

for f being morphism of C holds

( f is left_identity iff for f1 being morphism of C st f |> f1 holds

f (*) f1 = f1 );

for C being CategoryStr

for f being morphism of C holds

( f is left_identity iff for f1 being morphism of C st f |> f1 holds

f (*) f1 = f1 );

:: deftheorem Def5 defines right_identity CAT_6:def 5 :

for C being CategoryStr

for f being morphism of C holds

( f is right_identity iff for f1 being morphism of C st f1 |> f holds

f1 (*) f = f1 );

for C being CategoryStr

for f being morphism of C holds

( f is right_identity iff for f1 being morphism of C st f1 |> f holds

f1 (*) f = f1 );

definition

let C be CategoryStr ;

end;
attr C is with_left_identities means :Def6: :: CAT_6:def 6

for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f |> f1 & f is left_identity );

for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f |> f1 & f is left_identity );

attr C is with_right_identities means :Def7: :: CAT_6:def 7

for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f1 |> f & f is right_identity );

for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f1 |> f & f is right_identity );

attr C is left_composable means :: CAT_6:def 8

for f, f1, f2 being morphism of C st f1 |> f2 holds

( f1 (*) f2 |> f iff f2 |> f );

for f, f1, f2 being morphism of C st f1 |> f2 holds

( f1 (*) f2 |> f iff f2 |> f );

attr C is right_composable means :Def9: :: CAT_6:def 9

for f, f1, f2 being morphism of C st f1 |> f2 holds

( f |> f1 (*) f2 iff f |> f1 );

for f, f1, f2 being morphism of C st f1 |> f2 holds

( f |> f1 (*) f2 iff f |> f1 );

:: deftheorem Def6 defines with_left_identities CAT_6:def 6 :

for C being CategoryStr holds

( C is with_left_identities iff for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f |> f1 & f is left_identity ) );

for C being CategoryStr holds

( C is with_left_identities iff for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f |> f1 & f is left_identity ) );

:: deftheorem Def7 defines with_right_identities CAT_6:def 7 :

for C being CategoryStr holds

( C is with_right_identities iff for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f1 |> f & f is right_identity ) );

for C being CategoryStr holds

( C is with_right_identities iff for f1 being morphism of C st f1 in the carrier of C holds

ex f being morphism of C st

( f1 |> f & f is right_identity ) );

:: deftheorem defines left_composable CAT_6:def 8 :

for C being CategoryStr holds

( C is left_composable iff for f, f1, f2 being morphism of C st f1 |> f2 holds

( f1 (*) f2 |> f iff f2 |> f ) );

for C being CategoryStr holds

( C is left_composable iff for f, f1, f2 being morphism of C st f1 |> f2 holds

( f1 (*) f2 |> f iff f2 |> f ) );

:: deftheorem Def9 defines right_composable CAT_6:def 9 :

for C being CategoryStr holds

( C is right_composable iff for f, f1, f2 being morphism of C st f1 |> f2 holds

( f |> f1 (*) f2 iff f |> f1 ) );

for C being CategoryStr holds

( C is right_composable iff for f, f1, f2 being morphism of C st f1 |> f2 holds

( f |> f1 (*) f2 iff f |> f1 ) );

:: deftheorem Def10 defines associative CAT_6:def 10 :

for C being CategoryStr holds

( C is associative iff for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds

f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 );

for C being CategoryStr holds

( C is associative iff for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 & f1 (*) f2 |> f3 & f1 |> f2 (*) f3 holds

f1 (*) (f2 (*) f3) = (f1 (*) f2) (*) f3 );

definition

let C be CategoryStr ;

end;
attr C is with_identities means :Def12: :: CAT_6:def 12

( C is with_left_identities & C is with_right_identities );

( C is with_left_identities & C is with_right_identities );

:: deftheorem Def11 defines composable CAT_6:def 11 :

for C being CategoryStr holds

( C is composable iff ( C is left_composable & C is right_composable ) );

for C being CategoryStr holds

( C is composable iff ( C is left_composable & C is right_composable ) );

:: deftheorem Def12 defines with_identities CAT_6:def 12 :

for C being CategoryStr holds

( C is with_identities iff ( C is with_left_identities & C is with_right_identities ) );

for C being CategoryStr holds

( C is with_identities iff ( C is with_left_identities & C is with_right_identities ) );

definition

let C be CategoryStr ;

CategoryStr(# the carrier of C,(~ the composition of C) #) is strict CategoryStr ;

end;
func C opp -> strict CategoryStr equals :: CAT_6:def 13

CategoryStr(# the carrier of C,(~ the composition of C) #);

coherence CategoryStr(# the carrier of C,(~ the composition of C) #);

CategoryStr(# the carrier of C,(~ the composition of C) #) is strict CategoryStr ;

:: deftheorem defines opp CAT_6:def 13 :

for C being CategoryStr holds C opp = CategoryStr(# the carrier of C,(~ the composition of C) #);

for C being CategoryStr holds C opp = CategoryStr(# the carrier of C,(~ the composition of C) #);

theorem :: CAT_6:1

theorem :: CAT_6:2

for C being CategoryStr

for f1, f2 being morphism of C

for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 holds

( f1 |> f2 iff g2 |> g1 ) by FUNCT_4:42;

for f1, f2 being morphism of C

for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 holds

( f1 |> f2 iff g2 |> g1 ) by FUNCT_4:42;

theorem Th3: :: CAT_6:3

for C being CategoryStr

for f1, f2 being morphism of C

for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 & f1 |> f2 holds

f1 (*) f2 = g2 (*) g1

for f1, f2 being morphism of C

for g1, g2 being morphism of (C opp) st f1 = g1 & f2 = g2 & f1 |> f2 holds

f1 (*) f2 = g2 (*) g1

proof end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( b_{1} is with_left_identities & not b_{1} is with_right_identities & b_{1} is composable & b_{1} is associative );

end;
existence

ex b

( b

proof end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( not b_{1} is with_left_identities & b_{1} is with_right_identities & b_{1} is composable & b_{1} is associative );

end;
existence

ex b

( not b

proof end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( not b_{1} is left_composable & b_{1} is right_composable & b_{1} is with_identities & b_{1} is associative );

end;
existence

ex b

( not b

proof end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( b_{1} is left_composable & not b_{1} is right_composable & b_{1} is with_identities & b_{1} is associative );

end;
existence

ex b

( b

proof end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( not b_{1} is associative & b_{1} is composable & b_{1} is with_identities );

end;
existence

ex b

( not b

proof end;

registration

coherence

for b_{1} being CategoryStr st b_{1} is empty holds

( b_{1} is left_composable & b_{1} is right_composable & b_{1} is with_left_identities & b_{1} is with_right_identities & b_{1} is associative );

end;

cluster empty -> with_left_identities with_right_identities left_composable right_composable associative for CategoryStr ;

correctness coherence

for b

( b

proof end;

registration

existence

ex b_{1} being CategoryStr st

( b_{1} is strict & b_{1} is with_left_identities & b_{1} is with_right_identities & b_{1} is left_composable & b_{1} is right_composable & b_{1} is associative );

end;

cluster strict with_left_identities with_right_identities left_composable right_composable associative for CategoryStr ;

correctness existence

ex b

( b

proof end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( b_{1} is strict & b_{1} is with_identities & b_{1} is composable & b_{1} is associative );

end;
existence

ex b

( b

proof end;

:: deftheorem defines identity CAT_6:def 14 :

for C being CategoryStr

for f being morphism of C holds

( f is identity iff ( f is left_identity & f is right_identity ) );

for C being CategoryStr

for f being morphism of C holds

( f is identity iff ( f is left_identity & f is right_identity ) );

theorem Th9: :: CAT_6:9

for C being CategoryStr

for f being morphism of C st C is with_identities holds

( f is left_identity iff f is right_identity )

for f being morphism of C st C is with_identities holds

( f is left_identity iff f is right_identity )

proof end;

theorem Th11: :: CAT_6:11

for C being CategoryStr

for f1, f2 being morphism of C

for g1, g2 being morphism of CategoryStr(# the carrier of C, the composition of C #) st f1 = g1 & f2 = g2 & f1 |> f2 holds

f1 (*) f2 = g1 (*) g2

for f1, f2 being morphism of C

for g1, g2 being morphism of CategoryStr(# the carrier of C, the composition of C #) st f1 = g1 & f2 = g2 & f1 |> f2 holds

f1 (*) f2 = g1 (*) g2

proof end;

theorem Th12: :: CAT_6:12

for C being CategoryStr holds

( C is left_composable iff CategoryStr(# the carrier of C, the composition of C #) is left_composable )

( C is left_composable iff CategoryStr(# the carrier of C, the composition of C #) is left_composable )

proof end;

theorem Th13: :: CAT_6:13

for C being CategoryStr holds

( C is right_composable iff CategoryStr(# the carrier of C, the composition of C #) is right_composable )

( C is right_composable iff CategoryStr(# the carrier of C, the composition of C #) is right_composable )

proof end;

theorem :: CAT_6:14

for C being CategoryStr holds

( C is composable iff CategoryStr(# the carrier of C, the composition of C #) is composable ) by Th12, Th13;

( C is composable iff CategoryStr(# the carrier of C, the composition of C #) is composable ) by Th12, Th13;

theorem :: CAT_6:15

for C being CategoryStr holds

( C is associative iff CategoryStr(# the carrier of C, the composition of C #) is associative )

( C is associative iff CategoryStr(# the carrier of C, the composition of C #) is associative )

proof end;

theorem Th16: :: CAT_6:16

for C being CategoryStr

for f being morphism of C

for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds

( f is left_identity iff g is left_identity )

for f being morphism of C

for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds

( f is left_identity iff g is left_identity )

proof end;

theorem Th17: :: CAT_6:17

for C being CategoryStr holds

( C is with_left_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_left_identities )

( C is with_left_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_left_identities )

proof end;

theorem Th18: :: CAT_6:18

for C being CategoryStr

for f being morphism of C

for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds

( f is right_identity iff g is right_identity )

for f being morphism of C

for g being morphism of CategoryStr(# the carrier of C, the composition of C #) st f = g holds

( f is right_identity iff g is right_identity )

proof end;

theorem Th19: :: CAT_6:19

for C being CategoryStr holds

( C is with_right_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_right_identities )

( C is with_right_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_right_identities )

proof end;

theorem :: CAT_6:20

for C being CategoryStr holds

( C is with_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_identities ) by Th17, Th19;

( C is with_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_identities ) by Th17, Th19;

:: deftheorem Def15 defines discrete CAT_6:def 15 :

for C being CategoryStr holds

( C is discrete iff for f being morphism of C holds f is identity );

for C being CategoryStr holds

( C is discrete iff for f being morphism of C holds f is identity );

Lm1: the empty CategoryStr opp is discrete

proof end;

registration

correctness

existence

ex b_{1} being CategoryStr st

( b_{1} is strict & b_{1} is empty & b_{1} is discrete & b_{1} is with_identities & b_{1} is composable & b_{1} is associative );

end;
existence

ex b

( b

proof end;

theorem Th21: :: CAT_6:21

for C being discrete CategoryStr

for f1, f2 being morphism of C st f1 |> f2 holds

( f1 = f2 & f1 (*) f2 = f2 )

for f1, f2 being morphism of C st f1 |> f2 holds

( f1 = f2 & f1 (*) f2 = f2 )

proof end;

registration

correctness

coherence

for b_{1} being CategoryStr st b_{1} is discrete holds

( b_{1} is composable & b_{1} is associative );

end;
coherence

for b

( b

proof end;

definition

let X be set ;

existence

ex b_{1} being strict discrete category st the carrier of b_{1} = X

for b_{1}, b_{2} being strict discrete category st the carrier of b_{1} = X & the carrier of b_{2} = X holds

b_{1} = b_{2}

end;
existence

ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def16 defines DiscreteCat CAT_6:def 16 :

for X being set

for b_{2} being strict discrete category holds

( b_{2} = DiscreteCat X iff the carrier of b_{2} = X );

for X being set

for b

( b

registration

correctness

existence

ex b_{1} being category st b_{1} is strict ;

existence

ex b_{1} being category st

( b_{1} is strict & b_{1} is empty );

existence

ex b_{1} being category st

( b_{1} is strict & not b_{1} is empty );

end;
existence

ex b

proof end;

correctness existence

ex b

( b

proof end;

correctness existence

ex b

( b

proof end;

definition

let C be CategoryStr ;

coherence

{ f where f is morphism of C : ( f is identity & f in Mor C ) } is Subset of (Mor C);

end;
func Ob C -> Subset of (Mor C) equals :: CAT_6:def 17

{ f where f is morphism of C : ( f is identity & f in Mor C ) } ;

correctness { f where f is morphism of C : ( f is identity & f in Mor C ) } ;

coherence

{ f where f is morphism of C : ( f is identity & f in Mor C ) } is Subset of (Mor C);

proof end;

:: deftheorem defines Ob CAT_6:def 17 :

for C being CategoryStr holds Ob C = { f where f is morphism of C : ( f is identity & f in Mor C ) } ;

for C being CategoryStr holds Ob C = { f where f is morphism of C : ( f is identity & f in Mor C ) } ;

registration

let C be non empty with_identities CategoryStr ;

correctness

coherence

not Ob C is empty ;

end;
correctness

coherence

not Ob C is empty ;

proof end;

theorem Th22: :: CAT_6:22

for C being non empty with_identities CategoryStr

for f being morphism of C holds

( f is identity iff f is Object of C )

for f being morphism of C holds

( f is identity iff f is Object of C )

proof end;

theorem Th23: :: CAT_6:23

for C being non empty with_identities CategoryStr

for f, f1 being morphism of C

for o being Object of C st f = o holds

( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f )

for f, f1 being morphism of C

for o being Object of C st f = o holds

( ( f |> f1 implies f (*) f1 = f1 ) & ( f1 |> f implies f1 (*) f = f1 ) & f |> f )

proof end;

theorem Th24: :: CAT_6:24

for C being non empty with_identities CategoryStr

for f being morphism of C st f is identity holds

f |> f

for f being morphism of C st f is identity holds

f |> f

proof end;

theorem Th25: :: CAT_6:25

for C1, C2 being with_identities CategoryStr st CategoryStr(# the carrier of C1, the composition of C1 #) = CategoryStr(# the carrier of C2, the composition of C2 #) holds

for f1 being morphism of C1

for f2 being morphism of C2 st f1 = f2 holds

( f1 is identity iff f2 is identity )

for f1 being morphism of C1

for f2 being morphism of C2 st f1 = f2 holds

( f1 is identity iff f2 is identity )

proof end;

Lm2: for C being CategoryStr holds

( C is with_identities iff for f being morphism of C st f in Mor C holds

( ex c being morphism of C st

( c |> f & c is identity ) & ex d being morphism of C st

( f |> d & d is identity ) ) )

proof end;

Lm3: for C being CategoryStr holds

( C is composable iff for f, g, h being morphism of C holds

( ( h (*) g |> f & h |> g implies g |> f ) & ( h |> g (*) f & g |> f implies h |> g ) & ( g |> f & h |> g implies ( h (*) g |> f & h |> g (*) f ) ) ) )

proof end;

definition

let C be composable with_identities CategoryStr ;

let f be morphism of C;

( ( not C is empty implies ex b_{1} being Object of C ex f1 being morphism of C st

( b_{1} = f1 & f |> f1 & f1 is identity ) ) & ( C is empty implies ex b_{1} being Object of C st b_{1} = the Object of C ) )

for b_{1}, b_{2} being Object of C holds

( ( not C is empty & ex f1 being morphism of C st

( b_{1} = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st

( b_{2} = f1 & f |> f1 & f1 is identity ) implies b_{1} = b_{2} ) & ( C is empty & b_{1} = the Object of C & b_{2} = the Object of C implies b_{1} = b_{2} ) )

consistency

for b_{1} being Object of C holds verum;

;

( ( not C is empty implies ex b_{1} being Object of C ex f1 being morphism of C st

( b_{1} = f1 & f1 |> f & f1 is identity ) ) & ( C is empty implies ex b_{1} being Object of C st b_{1} = the Object of C ) )

for b_{1}, b_{2} being Object of C holds

( ( not C is empty & ex f1 being morphism of C st

( b_{1} = f1 & f1 |> f & f1 is identity ) & ex f1 being morphism of C st

( b_{2} = f1 & f1 |> f & f1 is identity ) implies b_{1} = b_{2} ) & ( C is empty & b_{1} = the Object of C & b_{2} = the Object of C implies b_{1} = b_{2} ) )

consistency

for b_{1} being Object of C holds verum;

;

end;
let f be morphism of C;

func dom f -> Object of C means :Def18: :: CAT_6:def 18

ex f1 being morphism of C st

( it = f1 & f |> f1 & f1 is identity ) if not C is empty

otherwise it = the Object of C;

existence ex f1 being morphism of C st

( it = f1 & f |> f1 & f1 is identity ) if not C is empty

otherwise it = the Object of C;

( ( not C is empty implies ex b

( b

proof end;

uniqueness for b

( ( not C is empty & ex f1 being morphism of C st

( b

( b

proof end;

correctness consistency

for b

;

func cod f -> Object of C means :Def19: :: CAT_6:def 19

ex f1 being morphism of C st

( it = f1 & f1 |> f & f1 is identity ) if not C is empty

otherwise it = the Object of C;

existence ex f1 being morphism of C st

( it = f1 & f1 |> f & f1 is identity ) if not C is empty

otherwise it = the Object of C;

( ( not C is empty implies ex b

( b

proof end;

uniqueness for b

( ( not C is empty & ex f1 being morphism of C st

( b

( b

proof end;

correctness consistency

for b

;

:: deftheorem Def18 defines dom CAT_6:def 18 :

for C being composable with_identities CategoryStr

for f being morphism of C

for b_{3} being Object of C holds

( ( not C is empty implies ( b_{3} = dom f iff ex f1 being morphism of C st

( b_{3} = f1 & f |> f1 & f1 is identity ) ) ) & ( C is empty implies ( b_{3} = dom f iff b_{3} = the Object of C ) ) );

for C being composable with_identities CategoryStr

for f being morphism of C

for b

( ( not C is empty implies ( b

( b

:: deftheorem Def19 defines cod CAT_6:def 19 :

for C being composable with_identities CategoryStr

for f being morphism of C

for b_{3} being Object of C holds

( ( not C is empty implies ( b_{3} = cod f iff ex f1 being morphism of C st

( b_{3} = f1 & f1 |> f & f1 is identity ) ) ) & ( C is empty implies ( b_{3} = cod f iff b_{3} = the Object of C ) ) );

for C being composable with_identities CategoryStr

for f being morphism of C

for b

( ( not C is empty implies ( b

( b

theorem Th26: :: CAT_6:26

for C being composable with_identities CategoryStr

for f, f1 being morphism of C st f |> f1 & f1 is identity holds

dom f = f1

for f, f1 being morphism of C st f |> f1 & f1 is identity holds

dom f = f1

proof end;

theorem Th27: :: CAT_6:27

for C being composable with_identities CategoryStr

for f, f1 being morphism of C st f1 |> f & f1 is identity holds

cod f = f1

for f, f1 being morphism of C st f1 |> f & f1 is identity holds

cod f = f1

proof end;

definition

let C be with_identities CategoryStr ;

let o be Object of C;

correctness

coherence

o is morphism of C;

end;
let o be Object of C;

correctness

coherence

o is morphism of C;

proof end;

:: deftheorem defines id- CAT_6:def 20 :

for C being with_identities CategoryStr

for o being Object of C holds id- o = o;

for C being with_identities CategoryStr

for o being Object of C holds id- o = o;

definition

let C, D be with_identities CategoryStr ;

let F be Functor of C,D;

let f be morphism of C;

coherence

( ( not C is empty implies F . f is morphism of D ) & ( C is empty implies the Object of D is morphism of D ) );

consistency

for b_{1} being morphism of D holds verum;

end;
let F be Functor of C,D;

let f be morphism of C;

func F . f -> morphism of D equals :Def21: :: CAT_6:def 21

F . f if not C is empty

otherwise the Object of D;

correctness F . f if not C is empty

otherwise the Object of D;

coherence

( ( not C is empty implies F . f is morphism of D ) & ( C is empty implies the Object of D is morphism of D ) );

consistency

for b

proof end;

:: deftheorem Def21 defines . CAT_6:def 21 :

for C, D being with_identities CategoryStr

for F being Functor of C,D

for f being morphism of C holds

( ( not C is empty implies F . f = F . f ) & ( C is empty implies F . f = the Object of D ) );

for C, D being with_identities CategoryStr

for F being Functor of C,D

for f being morphism of C holds

( ( not C is empty implies F . f = F . f ) & ( C is empty implies F . f = the Object of D ) );

definition

let C, D be with_identities CategoryStr ;

let F be Functor of C,D;

end;
let F be Functor of C,D;

attr F is identity-preserving means :Def22: :: CAT_6:def 22

for f being morphism of C st f is identity holds

F . f is identity ;

for f being morphism of C st f is identity holds

F . f is identity ;

:: deftheorem Def22 defines identity-preserving CAT_6:def 22 :

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is identity-preserving iff for f being morphism of C st f is identity holds

F . f is identity );

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is identity-preserving iff for f being morphism of C st f is identity holds

F . f is identity );

:: deftheorem Def23 defines multiplicative CAT_6:def 23 :

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is multiplicative iff for f1, f2 being morphism of C st f1 |> f2 holds

( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) );

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is multiplicative iff for f1, f2 being morphism of C st f1 |> f2 holds

( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) );

:: deftheorem defines antimultiplicative CAT_6:def 24 :

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is antimultiplicative iff for f1, f2 being morphism of C st f1 |> f2 holds

( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) ) );

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is antimultiplicative iff for f1, f2 being morphism of C st f1 |> f2 holds

( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) ) );

registration

let C, D be with_identities CategoryStr ;

existence

ex b_{1} being Functor of C,D st b_{1} is identity-preserving ;

end;
cluster Relation-like the carrier of C -defined the carrier of D -valued Function-like V28( the carrier of C, the carrier of D) identity-preserving for Element of bool [: the carrier of C, the carrier of D:];

correctness existence

ex b

proof end;

registration

let C be empty with_identities CategoryStr ;

let D be with_identities CategoryStr ;

existence

ex b_{1} being Functor of C,D st

( b_{1} is identity-preserving & b_{1} is multiplicative & b_{1} is antimultiplicative );

end;
let D be with_identities CategoryStr ;

cluster Relation-like non-empty empty-yielding the carrier of C -defined the carrier of D -valued empty trivial non proper V9() V10() V11() V13() V14() V15() V16() V17() V18() Function-like one-to-one constant functional total V28( the carrier of C, the carrier of D) V31() V35() V36() V39() cardinal 0 -element V43() V44() V45() V98() V99() V100() V101() V102() V105() V106() V107() V108() V109() V110() V111() V112() identity-preserving multiplicative antimultiplicative for Element of bool [: the carrier of C, the carrier of D:];

correctness existence

ex b

( b

proof end;

registration

let C be with_identities CategoryStr ;

let D be non empty with_identities CategoryStr ;

existence

ex b_{1} being Functor of C,D st

( b_{1} is identity-preserving & b_{1} is multiplicative & b_{1} is antimultiplicative );

end;
let D be non empty with_identities CategoryStr ;

cluster Relation-like the carrier of C -defined the carrier of D -valued Function-like total V28( the carrier of C, the carrier of D) identity-preserving multiplicative antimultiplicative for Element of bool [: the carrier of C, the carrier of D:];

correctness existence

ex b

( b

proof end;

theorem :: CAT_6:28

ex C, D being category ex F being Functor of C,D st

( F is multiplicative & not F is identity-preserving )

( F is multiplicative & not F is identity-preserving )

proof end;

theorem Th29: :: CAT_6:29

for C, D being with_identities CategoryStr st not C is empty & D is empty holds

for F being Functor of C,D holds

( not F is multiplicative & not F is antimultiplicative )

for F being Functor of C,D holds

( not F is multiplicative & not F is antimultiplicative )

proof end;

theorem :: CAT_6:30

ex C, D being category ex F being Functor of C,D st

( not F is multiplicative & F is identity-preserving )

( not F is multiplicative & F is identity-preserving )

proof end;

definition

let C, D be with_identities CategoryStr ;

let F be Functor of C,D;

end;
let F be Functor of C,D;

attr F is covariant means :Def25: :: CAT_6:def 25

( F is identity-preserving & F is multiplicative );

( F is identity-preserving & F is multiplicative );

attr F is contravariant means :: CAT_6:def 26

( F is identity-preserving & F is antimultiplicative );

( F is identity-preserving & F is antimultiplicative );

:: deftheorem Def25 defines covariant CAT_6:def 25 :

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is covariant iff ( F is identity-preserving & F is multiplicative ) );

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is covariant iff ( F is identity-preserving & F is multiplicative ) );

:: deftheorem defines contravariant CAT_6:def 26 :

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is contravariant iff ( F is identity-preserving & F is antimultiplicative ) );

for C, D being with_identities CategoryStr

for F being Functor of C,D holds

( F is contravariant iff ( F is identity-preserving & F is antimultiplicative ) );

registration

let C be empty with_identities CategoryStr ;

let D be with_identities CategoryStr ;

existence

ex b_{1} being Functor of C,D st

( b_{1} is covariant & b_{1} is contravariant );

end;
let D be with_identities CategoryStr ;

cluster Relation-like non-empty empty-yielding the carrier of C -defined the carrier of D -valued empty trivial non proper V9() V10() V11() V13() V14() V15() V16() V17() V18() Function-like one-to-one constant functional total V28( the carrier of C, the carrier of D) V31() V35() V36() V39() cardinal 0 -element V43() V44() V45() V98() V99() V100() V101() V102() V105() V106() V107() V108() V109() V110() V111() V112() covariant contravariant for Element of bool [: the carrier of C, the carrier of D:];

correctness existence

ex b

( b

proof end;

registration

let C be with_identities CategoryStr ;

let D be non empty with_identities CategoryStr ;

existence

ex b_{1} being Functor of C,D st

( b_{1} is covariant & b_{1} is contravariant );

end;
let D be non empty with_identities CategoryStr ;

cluster Relation-like the carrier of C -defined the carrier of D -valued Function-like total V28( the carrier of C, the carrier of D) covariant contravariant for Element of bool [: the carrier of C, the carrier of D:];

correctness existence

ex b

( b

proof end;

theorem :: CAT_6:31

for C, D being with_identities CategoryStr st not C is empty & D is empty holds

for F being Functor of C,D holds

( not F is covariant & not F is contravariant ) by Th29;

for F being Functor of C,D holds

( not F is covariant & not F is contravariant ) by Th29;

definition

let C, D be non empty with_identities CategoryStr ;

let F be covariant Functor of C,D;

let f be Object of C;

:: original: .

redefine func F . f -> Object of D;

coherence

F . f is Object of D

end;
let F be covariant Functor of C,D;

let f be Object of C;

:: original: .

redefine func F . f -> Object of D;

coherence

F . f is Object of D

proof end;

theorem Th32: :: CAT_6:32

for C, D being non empty composable with_identities CategoryStr

for F being covariant Functor of C,D

for f being morphism of C holds

( F . (dom f) = dom (F . f) & F . (cod f) = cod (F . f) )

for F being covariant Functor of C,D

for f being morphism of C holds

( F . (dom f) = dom (F . f) & F . (cod f) = cod (F . f) )

proof end;

theorem :: CAT_6:33

for C, D being non empty composable with_identities CategoryStr

for F being covariant Functor of C,D

for o being Object of C holds F . (id- o) = id- (F . o) by Def21;

for F being covariant Functor of C,D

for o being Object of C holds F . (id- o) = id- (F . o) by Def21;

definition

let C, D, E be with_identities CategoryStr ;

let F be Functor of C,D;

let G be Functor of D,E;

assume A1: ( ( F is covariant or F is contravariant ) & ( G is covariant or G is contravariant ) ) ;

coherence

F * G is Functor of C,E

end;
let F be Functor of C,D;

let G be Functor of D,E;

assume A1: ( ( F is covariant or F is contravariant ) & ( G is covariant or G is contravariant ) ) ;

coherence

F * G is Functor of C,E

proof end;

:: deftheorem Def27 defines (*) CAT_6:def 27 :

for C, D, E being with_identities CategoryStr

for F being Functor of C,D

for G being Functor of D,E st ( F is covariant or F is contravariant ) & ( G is covariant or G is contravariant ) holds

G (*) F = F * G;

for C, D, E being with_identities CategoryStr

for F being Functor of C,D

for G being Functor of D,E st ( F is covariant or F is contravariant ) & ( G is covariant or G is contravariant ) holds

G (*) F = F * G;

theorem Th34: :: CAT_6:34

for C, D, E being with_identities CategoryStr

for F being Functor of C,D

for G being Functor of D,E

for f being morphism of C st F is covariant & G is covariant & not C is empty holds

(G (*) F) . f = G . (F . f)

for F being Functor of C,D

for G being Functor of D,E

for f being morphism of C st F is covariant & G is covariant & not C is empty holds

(G (*) F) . f = G . (F . f)

proof end;

theorem :: CAT_6:35

for C, D, E being with_identities CategoryStr

for F being Functor of C,D

for G being Functor of D,E st F is covariant & G is covariant holds

G (*) F is covariant

for F being Functor of C,D

for G being Functor of D,E st F is covariant & G is covariant holds

G (*) F is covariant

proof end;

definition

let C be with_identities CategoryStr ;

:: original: id

redefine func id C -> Functor of C,C;

coherence

id C is Functor of C,C ;

end;
:: original: id

redefine func id C -> Functor of C,C;

coherence

id C is Functor of C,C ;

registration
end;

definition

let C, D be with_identities CategoryStr ;

for C being with_identities CategoryStr ex F, G being Functor of C,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id C )

for C, D being with_identities CategoryStr st ex F being Functor of C,D ex G being Functor of D,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) holds

ex F being Functor of D,C ex G being Functor of C,D st

( F is covariant & G is covariant & G (*) F = id D & F (*) G = id C ) ;

end;
pred C,D are_isomorphic means :: CAT_6:def 28

ex F being Functor of C,D ex G being Functor of D,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D );

reflexivity ex F being Functor of C,D ex G being Functor of D,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D );

for C being with_identities CategoryStr ex F, G being Functor of C,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id C )

proof end;

symmetry for C, D being with_identities CategoryStr st ex F being Functor of C,D ex G being Functor of D,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) holds

ex F being Functor of D,C ex G being Functor of C,D st

( F is covariant & G is covariant & G (*) F = id D & F (*) G = id C ) ;

:: deftheorem defines are_isomorphic CAT_6:def 28 :

for C, D being with_identities CategoryStr holds

( C,D are_isomorphic iff ex F being Functor of C,D ex G being Functor of D,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) );

for C, D being with_identities CategoryStr holds

( C,D are_isomorphic iff ex F being Functor of C,D ex G being Functor of D,C st

( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) );

Lm4: for C being CategoryStr

for f, g being morphism of C st g |> f holds

g (*) f = the composition of C . [g,f]

proof end;

Lm5: for C being composable CategoryStr holds

( C is associative iff for f, g, h being morphism of C st h |> g & g |> f holds

h (*) (g (*) f) = (h (*) g) (*) f )

proof end;

definition

let C be CategoryStr ;

coherence

the composition of C is PartFunc of [:(Mor C),(Mor C):],(Mor C);

;

end;
func CompMap C -> PartFunc of [:(Mor C),(Mor C):],(Mor C) equals :: CAT_6:def 29

the composition of C;

correctness the composition of C;

coherence

the composition of C is PartFunc of [:(Mor C),(Mor C):],(Mor C);

;

:: deftheorem defines CompMap CAT_6:def 29 :

for C being CategoryStr holds CompMap C = the composition of C;

for C being CategoryStr holds CompMap C = the composition of C;

definition

let C be composable with_identities CategoryStr ;

consistency

for b_{1} being Function of (Mor C),(Ob C) holds verum;

existence

( ( for b_{1} being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b_{1} being Function of (Mor C),(Ob C) st

for f being Element of Mor C holds b_{1} . f = dom f ) & ( C is empty implies ex b_{1} being Function of (Mor C),(Ob C) st b_{1} = {} ) );

uniqueness

for b_{1}, b_{2} being Function of (Mor C),(Ob C) holds

( ( not C is empty & ( for f being Element of Mor C holds b_{1} . f = dom f ) & ( for f being Element of Mor C holds b_{2} . f = dom f ) implies b_{1} = b_{2} ) & ( C is empty & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

consistency

for b_{1} being Function of (Mor C),(Ob C) holds verum;

existence

( ( for b_{1} being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b_{1} being Function of (Mor C),(Ob C) st

for f being Element of Mor C holds b_{1} . f = cod f ) & ( C is empty implies ex b_{1} being Function of (Mor C),(Ob C) st b_{1} = {} ) );

uniqueness

for b_{1}, b_{2} being Function of (Mor C),(Ob C) holds

( ( not C is empty & ( for f being Element of Mor C holds b_{1} . f = cod f ) & ( for f being Element of Mor C holds b_{2} . f = cod f ) implies b_{1} = b_{2} ) & ( C is empty & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

end;
func SourceMap C -> Function of (Mor C),(Ob C) means :Def30: :: CAT_6:def 30

for f being Element of Mor C holds it . f = dom f if not C is empty

otherwise it = {} ;

correctness for f being Element of Mor C holds it . f = dom f if not C is empty

otherwise it = {} ;

consistency

for b

existence

( ( for b

for f being Element of Mor C holds b

uniqueness

for b

( ( not C is empty & ( for f being Element of Mor C holds b

proof end;

func TargetMap C -> Function of (Mor C),(Ob C) means :Def31: :: CAT_6:def 31

for f being Element of Mor C holds it . f = cod f if not C is empty

otherwise it = {} ;

correctness for f being Element of Mor C holds it . f = cod f if not C is empty

otherwise it = {} ;

consistency

for b

existence

( ( for b

for f being Element of Mor C holds b

uniqueness

for b

( ( not C is empty & ( for f being Element of Mor C holds b

proof end;

:: deftheorem Def30 defines SourceMap CAT_6:def 30 :

for C being composable with_identities CategoryStr

for b_{2} being Function of (Mor C),(Ob C) holds

( ( not C is empty implies ( b_{2} = SourceMap C iff for f being Element of Mor C holds b_{2} . f = dom f ) ) & ( C is empty implies ( b_{2} = SourceMap C iff b_{2} = {} ) ) );

for C being composable with_identities CategoryStr

for b

( ( not C is empty implies ( b

:: deftheorem Def31 defines TargetMap CAT_6:def 31 :

for C being composable with_identities CategoryStr

for b_{2} being Function of (Mor C),(Ob C) holds

( ( not C is empty implies ( b_{2} = TargetMap C iff for f being Element of Mor C holds b_{2} . f = cod f ) ) & ( C is empty implies ( b_{2} = TargetMap C iff b_{2} = {} ) ) );

for C being composable with_identities CategoryStr

for b

( ( not C is empty implies ( b

definition

let C be with_identities CategoryStr ;

consistency

for b_{1} being Function of (Ob C),(Mor C) holds verum;

existence

( ( for b_{1} being Function of (Ob C),(Mor C) holds verum ) & ( not C is empty implies ex b_{1} being Function of (Ob C),(Mor C) st

for o being Element of Ob C holds b_{1} . o = id- o ) & ( C is empty implies ex b_{1} being Function of (Ob C),(Mor C) st b_{1} = {} ) );

uniqueness

for b_{1}, b_{2} being Function of (Ob C),(Mor C) holds

( ( not C is empty & ( for o being Element of Ob C holds b_{1} . o = id- o ) & ( for o being Element of Ob C holds b_{2} . o = id- o ) implies b_{1} = b_{2} ) & ( C is empty & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

end;
func IdMap C -> Function of (Ob C),(Mor C) means :Def32: :: CAT_6:def 32

for o being Element of Ob C holds it . o = id- o if not C is empty

otherwise it = {} ;

correctness for o being Element of Ob C holds it . o = id- o if not C is empty

otherwise it = {} ;

consistency

for b

existence

( ( for b

for o being Element of Ob C holds b

uniqueness

for b

( ( not C is empty & ( for o being Element of Ob C holds b

proof end;

:: deftheorem Def32 defines IdMap CAT_6:def 32 :

for C being with_identities CategoryStr

for b_{2} being Function of (Ob C),(Mor C) holds

( ( not C is empty implies ( b_{2} = IdMap C iff for o being Element of Ob C holds b_{2} . o = id- o ) ) & ( C is empty implies ( b_{2} = IdMap C iff b_{2} = {} ) ) );

for C being with_identities CategoryStr

for b

( ( not C is empty implies ( b

theorem Th37: :: CAT_6:36

for C being non empty composable with_identities CategoryStr

for f, g being Element of Mor C holds

( [g,f] in dom (CompMap C) iff (SourceMap C) . g = (TargetMap C) . f )

for f, g being Element of Mor C holds

( [g,f] in dom (CompMap C) iff (SourceMap C) . g = (TargetMap C) . f )

proof end;

theorem Th38: :: CAT_6:37

for C being composable with_identities CategoryStr

for f, g being Element of Mor C st (SourceMap C) . g = (TargetMap C) . f holds

( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )

for f, g being Element of Mor C st (SourceMap C) . g = (TargetMap C) . f holds

( (SourceMap C) . ((CompMap C) . (g,f)) = (SourceMap C) . f & (TargetMap C) . ((CompMap C) . (g,f)) = (TargetMap C) . g )

proof end;

theorem Th39: :: CAT_6:38

for C being associative composable with_identities CategoryStr

for f, g, h being Element of Mor C st (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f holds

(CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)

for f, g, h being Element of Mor C st (SourceMap C) . h = (TargetMap C) . g & (SourceMap C) . g = (TargetMap C) . f holds

(CompMap C) . (h,((CompMap C) . (g,f))) = (CompMap C) . (((CompMap C) . (h,g)),f)

proof end;

theorem Th40: :: CAT_6:39

for C being composable with_identities CategoryStr

for b being Element of Ob C holds

( (SourceMap C) . ((IdMap C) . b) = b & (TargetMap C) . ((IdMap C) . b) = b & ( for f being Element of Mor C st (TargetMap C) . f = b holds

(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds

(CompMap C) . (g,((IdMap C) . b)) = g ) )

for b being Element of Ob C holds

( (SourceMap C) . ((IdMap C) . b) = b & (TargetMap C) . ((IdMap C) . b) = b & ( for f being Element of Mor C st (TargetMap C) . f = b holds

(CompMap C) . (((IdMap C) . b),f) = f ) & ( for g being Element of Mor C st (SourceMap C) . g = b holds

(CompMap C) . (g,((IdMap C) . b)) = g ) )

proof end;

Lm6: for C being non empty category holds CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is Category

proof end;

definition

let C be non empty category;

CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is strict Category by Lm6;

end;
func Alter C -> strict Category equals :: CAT_6:def 33

CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #);

coherence CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #);

CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #) is strict Category by Lm6;

:: deftheorem defines Alter CAT_6:def 33 :

for C being non empty category holds Alter C = CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #);

for C being non empty category holds Alter C = CatStr(# (Ob C),(Mor C),(SourceMap C),(TargetMap C),(CompMap C) #);

Lm7: for C being Category holds CategoryStr(# the carrier' of C, the Comp of C #) is category

proof end;

definition

let A be Category;

CategoryStr(# the carrier' of A, the Comp of A #) is strict category by Lm7;

end;
func alter A -> strict category equals :: CAT_6:def 34

CategoryStr(# the carrier' of A, the Comp of A #);

coherence CategoryStr(# the carrier' of A, the Comp of A #);

CategoryStr(# the carrier' of A, the Comp of A #) is strict category by Lm7;

:: deftheorem defines alter CAT_6:def 34 :

for A being Category holds alter A = CategoryStr(# the carrier' of A, the Comp of A #);

for A being Category holds alter A = CategoryStr(# the carrier' of A, the Comp of A #);

theorem Th41: :: CAT_6:40

for A being Category

for a1, a2 being Morphism of A

for f1, f2 being morphism of (alter A) st a1 = f1 & a2 = f2 & [a1,a2] in dom the Comp of A holds

a1 (*) a2 = f1 (*) f2

for a1, a2 being Morphism of A

for f1, f2 being morphism of (alter A) st a1 = f1 & a2 = f2 & [a1,a2] in dom the Comp of A holds

a1 (*) a2 = f1 (*) f2

proof end;

theorem Th42: :: CAT_6:41

for A being Category

for f being morphism of (alter A) holds

( f is identity iff ex o being Object of A st f = id o )

for f being morphism of (alter A) holds

( f is identity iff ex o being Object of A st f = id o )

proof end;

theorem :: CAT_6:42

for A, B being Category

for F being Functor of A,B holds F is covariant Functor of (alter A),(alter B)

for F being Functor of A,B holds F is covariant Functor of (alter A),(alter B)

proof end;

theorem Th44: :: CAT_6:43

for C being non empty category

for a1, a2 being Morphism of (Alter C)

for f1, f2 being morphism of C st a1 = f1 & a2 = f2 & f1 |> f2 holds

a1 (*) a2 = f1 (*) f2

for a1, a2 being Morphism of (Alter C)

for f1, f2 being morphism of C st a1 = f1 & a2 = f2 & f1 |> f2 holds

a1 (*) a2 = f1 (*) f2

proof end;

theorem Th45: :: CAT_6:44

for C being non empty category

for f1 being morphism of C

for a1 being Morphism of (Alter C) st a1 = f1 holds

( dom f1 = dom a1 & cod f1 = cod a1 )

for f1 being morphism of C

for a1 being Morphism of (Alter C) st a1 = f1 holds

( dom f1 = dom a1 & cod f1 = cod a1 )

proof end;

theorem Th46: :: CAT_6:45

for C being non empty category

for o1 being Object of C

for o2 being Object of (Alter C) st o1 = o2 holds

id- o1 = id o2

for o1 being Object of C

for o2 being Object of (Alter C) st o1 = o2 holds

id- o1 = id o2

proof end;

theorem Th47: :: CAT_6:46

for C being non empty category

for f being morphism of C holds

( f is identity iff ex o being Object of (Alter C) st f = id o )

for f being morphism of C holds

( f is identity iff ex o being Object of (Alter C) st f = id o )

proof end;

theorem :: CAT_6:47

for C, D being non empty category

for F being covariant Functor of C,D holds F is Functor of Alter C, Alter D

for F being covariant Functor of C,D holds F is Functor of Alter C, Alter D

proof end;

theorem Th49: :: CAT_6:48

for C, D being Category

for F being covariant Functor of (alter C),(alter D) holds F is Functor of C,D

for F being covariant Functor of (alter C),(alter D) holds F is Functor of C,D

proof end;

theorem Th51: :: CAT_6:50

for C1, C2 being Category st the carrier' of C1 = the carrier' of C2 & the Comp of C1 = the Comp of C2 holds

C1 ~= C2

C1 ~= C2

proof end;