:: Object-Free Definition of Categories
:: by Marco Riccardi
::
:: Received October 7, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users


definition
attr c1 is strict ;
struct CategoryStr -> 1-sorted ;
aggr CategoryStr(# carrier, composition #) -> CategoryStr ;
sel composition c1 -> PartFunc of [: the carrier of c1, the carrier of c1:], the carrier of c1;
end;

definition
let C be CategoryStr ;
func Mor C -> set equals :: CAT_6:def 1
 the carrier of C;
correctness
coherence
the carrier of C is set ;
;
end;

:: deftheorem defines Mor CAT_6:def 1 :
for C being CategoryStr holds Mor C = the carrier of C;

definition
let C be CategoryStr ;
mode morphism of C is Element of Mor C;
end;

definition
let C be CategoryStr ;
let f1, f2 be morphism of C;
pred f1,f2 are_composable means :Def2: :: CAT_6:def 2
[f1,f2] in dom the composition of C;
end;

:: 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 );

notation
let C be CategoryStr ;
let f1, f2 be morphism of C;
synonym f1 |> f2 for f1,f2 are_composable ;
end;

definition
let C be CategoryStr ;
let f1, f2 be morphism of C;
assume A1: f1 |> f2 ;
func f1 (*) f2 -> morphism of C equals :Def3: :: CAT_6:def 3
 the composition of C . (f1,f2);
correctness
coherence
the composition of C . (f1,f2) is morphism of C;
proof end;
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);

definition
let C be CategoryStr ;
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;
attr f is right_identity means :Def5: :: CAT_6:def 5
 for f1 being morphism of C st f1 |> f holds
f1 (*) f = f1;
end;

:: 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 );

:: 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 );

definition
let C be CategoryStr ;
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 );
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 );
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 );
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 );
attr C is associative means :Def10: :: CAT_6:def 10
 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;
end;

:: 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 ) );

:: 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 ) );

:: 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 ) );

:: 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 ) );

:: 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 );

definition
let C be CategoryStr ;
attr C is composable means :Def11: :: CAT_6:def 11
( C is left_composable & C is right_composable );
attr C is with_identities means :Def12: :: CAT_6:def 12
( C is with_left_identities & C is with_right_identities );
end;

:: 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 ) );

:: 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 ) );

definition
let C be CategoryStr ;
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) #) is strict CategoryStr ;
end;

:: deftheorem defines opp CAT_6:def 13 :
for C being CategoryStr holds C opp = CategoryStr(# the carrier of C,(~ the composition of C) #);

theorem :: CAT_6:1
for C being CategoryStr
for f1, f2 being morphism of C st C is empty holds
not f1 |> f2 ;

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;

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
proof end;

theorem Th4: :: CAT_6:4
for C being CategoryStr holds
( C is left_composable iff C opp is right_composable )
proof end;

theorem Th5: :: CAT_6:5
for C being CategoryStr holds
( C is right_composable iff C opp is left_composable )
proof end;

theorem Th6: :: CAT_6:6
for C being CategoryStr holds
( C is with_left_identities iff C opp is with_right_identities )
proof end;

theorem Th7: :: CAT_6:7
for C being CategoryStr holds
( C is with_right_identities iff C opp is with_left_identities )
proof end;

theorem Th8: :: CAT_6:8
for C being CategoryStr holds
( C is associative iff C opp is associative )
proof end;

registration
cluster with_left_identities non with_right_identities associative composable for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( b1 is with_left_identities & not b1 is with_right_identities & b1 is composable & b1 is associative );
proof end;
end;

registration
cluster non with_left_identities with_right_identities associative composable for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( not b1 is with_left_identities & b1 is with_right_identities & b1 is composable & b1 is associative );
proof end;
end;

registration
cluster non left_composable right_composable associative with_identities for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( not b1 is left_composable & b1 is right_composable & b1 is with_identities & b1 is associative );
proof end;
end;

registration
cluster left_composable non right_composable associative with_identities for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( b1 is left_composable & not b1 is right_composable & b1 is with_identities & b1 is associative );
proof end;
end;

registration
cluster non associative composable with_identities for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( not b1 is associative & b1 is composable & b1 is with_identities );
proof end;
end;

registration
cluster empty for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st b1 is empty ;
proof end;
end;

registration
cluster empty -> with_left_identities with_right_identities left_composable right_composable associative for CategoryStr ;
correctness
coherence
for b1 being CategoryStr st b1 is empty holds
( b1 is left_composable & b1 is right_composable & b1 is with_left_identities & b1 is with_right_identities & b1 is associative );
proof end;
end;

registration
cluster strict with_left_identities with_right_identities left_composable right_composable associative for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( b1 is strict & b1 is with_left_identities & b1 is with_right_identities & b1 is left_composable & b1 is right_composable & b1 is associative );
proof end;
end;

registration
cluster strict associative composable with_identities for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( b1 is strict & b1 is with_identities & b1 is composable & b1 is associative );
proof end;
end;

definition
mode category is associative composable with_identities CategoryStr ;
end;

definition
let C be CategoryStr ;
let f be morphism of C;
attr f is identity means :: CAT_6:def 14
( f is left_identity & f is right_identity );
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 ) );

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 )
proof end;

theorem Th10: :: CAT_6:10
for C being CategoryStr
for f being morphism of C st C is empty holds
f is 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
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 )
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 )
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;

theorem :: CAT_6:15
for C being CategoryStr holds
( 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 )
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 )
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 )
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 )
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;

definition
let C be CategoryStr ;
attr C is discrete means :Def15: :: CAT_6:def 15
 for f being morphism of C holds f is identity ;
end;

:: 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 );

Lm1: the empty CategoryStr opp is discrete
proof end;

registration
cluster empty strict associative composable with_identities discrete for CategoryStr ;
correctness
existence
ex b1 being CategoryStr st
( b1 is strict & b1 is empty & b1 is discrete & b1 is with_identities & b1 is composable & b1 is associative );
proof end;
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 )
proof end;

registration
cluster discrete -> associative composable for CategoryStr ;
correctness
coherence
for b1 being CategoryStr st b1 is discrete holds
( b1 is composable & b1 is associative );
proof end;
end;

definition
let X be set ;
func DiscreteCat X -> strict discrete category means :Def16: :: CAT_6:def 16
 the carrier of it = X;
existence
ex b1 being strict discrete category st the carrier of b1 = X
proof end;
uniqueness
for b1, b2 being strict discrete category st the carrier of b1 = X & the carrier of b2 = X holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines DiscreteCat CAT_6:def 16 :
for X being set
for b2 being strict discrete category holds
( b2 = DiscreteCat X iff the carrier of b2 = X );

registration
cluster strict associative composable with_identities for CategoryStr ;
correctness
existence
ex b1 being category st b1 is strict ;
proof end;
cluster empty strict associative composable with_identities for CategoryStr ;
correctness
existence
ex b1 being category st
( b1 is strict & b1 is empty );
proof end;
cluster non empty strict associative composable with_identities for CategoryStr ;
correctness
existence
ex b1 being category st
( b1 is strict & not b1 is empty );
proof end;
end;

definition
let C be CategoryStr ;
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
coherence
{ f where f is morphism of C : ( f is identity & f in Mor C ) } is Subset of (Mor C);
proof end;
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 ) } ;

definition
let C be CategoryStr ;
mode Object of C is Element of Ob C;
end;

registration
let C be non empty with_identities CategoryStr ;
cluster Ob C -> non empty ;
correctness
coherence
not Ob C is empty ;
proof end;
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 )
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 )
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
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 )
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;
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
( ( not C is empty implies ex b1 being Object of C ex f1 being morphism of C st
( b1 = f1 & f |> f1 & f1 is identity ) ) & ( C is empty implies ex b1 being Object of C st b1 = the Object of C ) )
proof end;
uniqueness
for b1, b2 being Object of C holds
( ( not C is empty & ex f1 being morphism of C st
( b1 = f1 & f |> f1 & f1 is identity ) & ex f1 being morphism of C st
( b2 = f1 & f |> f1 & f1 is identity ) implies b1 = b2 ) & ( C is empty & b1 = the Object of C & b2 = the Object of C implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Object of C holds verum;
;
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
( ( not C is empty implies ex b1 being Object of C ex f1 being morphism of C st
( b1 = f1 & f1 |> f & f1 is identity ) ) & ( C is empty implies ex b1 being Object of C st b1 = the Object of C ) )
proof end;
uniqueness
for b1, b2 being Object of C holds
( ( not C is empty & ex f1 being morphism of C st
( b1 = f1 & f1 |> f & f1 is identity ) & ex f1 being morphism of C st
( b2 = f1 & f1 |> f & f1 is identity ) implies b1 = b2 ) & ( C is empty & b1 = the Object of C & b2 = the Object of C implies b1 = b2 ) )
proof end;
correctness
consistency
for b1 being Object of C holds verum;
;
end;

:: deftheorem Def18 defines dom CAT_6:def 18 :
for C being composable with_identities CategoryStr
for f being morphism of C
for b3 being Object of C holds
( ( not C is empty implies ( b3 = dom f iff ex f1 being morphism of C st
( b3 = f1 & f |> f1 & f1 is identity ) ) ) & ( C is empty implies ( b3 = dom f iff b3 = the Object of C ) ) );

:: deftheorem Def19 defines cod CAT_6:def 19 :
for C being composable with_identities CategoryStr
for f being morphism of C
for b3 being Object of C holds
( ( not C is empty implies ( b3 = cod f iff ex f1 being morphism of C st
( b3 = f1 & f1 |> f & f1 is identity ) ) ) & ( C is empty implies ( b3 = cod f iff b3 = the Object of C ) ) );

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
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
proof end;

definition
let C be with_identities CategoryStr ;
let o be Object of C;
func id- o -> morphism of C equals :: CAT_6:def 20
o;
correctness
coherence
o is morphism of C;
proof end;
end;

:: deftheorem defines id- CAT_6:def 20 :
for C being with_identities CategoryStr
for o being Object of C holds id- o = o;

definition
let C, D be CategoryStr ;
mode Functor of C,D is Function of C,D;
end;

definition
let C, D be with_identities CategoryStr ;
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
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 b1 being morphism of D holds verum;
proof end;
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 ) );

definition
let C, D be with_identities CategoryStr ;
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 ;
attr F is multiplicative means :Def23: :: CAT_6:def 23
 for f1, f2 being morphism of C st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) );
attr F is antimultiplicative means :: CAT_6:def 24
 for f1, f2 being morphism of C st f1 |> f2 holds
( F . f2 |> F . f1 & F . (f1 (*) f2) = (F . f2) (*) (F . f1) );
end;

:: 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 );

:: 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) ) );

:: 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) ) );

registration
let C, D be with_identities CategoryStr ;
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 b1 being Functor of C,D st b1 is identity-preserving ;
proof end;
end;

registration
let C be empty with_identities CategoryStr ;
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() V100() V101() identity-preserving multiplicative antimultiplicative for Element of bool [: the carrier of C, the carrier of D:];
correctness
existence
ex b1 being Functor of C,D st
( b1 is identity-preserving & b1 is multiplicative & b1 is antimultiplicative );
proof end;
end;

registration
let C be with_identities CategoryStr ;
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 b1 being Functor of C,D st
( b1 is identity-preserving & b1 is multiplicative & b1 is antimultiplicative );
proof end;
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 )
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 )
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 )
proof end;

definition
let C, D be with_identities CategoryStr ;
let F be Functor of C,D;
attr F is covariant means :Def25: :: CAT_6:def 25
( F is identity-preserving & F is multiplicative );
attr F is contravariant means :: CAT_6:def 26
( F is identity-preserving & F is antimultiplicative );
end;

:: 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 ) );

:: 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 ) );

registration
let C be empty with_identities CategoryStr ;
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() V100() V101() covariant contravariant for Element of bool [: the carrier of C, the carrier of D:];
correctness
existence
ex b1 being Functor of C,D st
( b1 is covariant & b1 is contravariant );
proof end;
end;

registration
let C be with_identities CategoryStr ;
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 b1 being Functor of C,D st
( b1 is covariant & b1 is contravariant );
proof end;
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;

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
proof end;
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) )
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;

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 ) ) ;
func G (*) F -> Functor of C,E equals :Def27: :: CAT_6:def 27
F * G;
coherence
F * G is Functor of C,E
proof end;
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;

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)
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
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;

registration
let C be with_identities CategoryStr ;
cluster id C -> covariant ;
correctness
coherence
id C is covariant ;
proof end;
end;

definition
let C, D be with_identities CategoryStr ;
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
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 ) ;
end;

:: 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 ) );

notation
let C, D be with_identities CategoryStr ;
synonym C ~= D for C,D are_isomorphic ;
end;

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 ;
func CompMap C -> PartFunc of [:(Mor C),(Mor C):],(Mor C) equals :: CAT_6:def 29
 the composition of C;
correctness
coherence
the composition of C is PartFunc of [:(Mor C),(Mor C):],(Mor C);
;
end;

:: deftheorem defines CompMap CAT_6:def 29 :
for C being CategoryStr holds CompMap C = the composition of C;

definition
let C be composable with_identities CategoryStr ;
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
consistency
for b1 being Function of (Mor C),(Ob C) holds verum;
existence
( ( for b1 being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b1 being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds b1 . f = dom f ) & ( C is empty implies ex b1 being Function of (Mor C),(Ob C) st b1 = {} ) );
uniqueness
for b1, b2 being Function of (Mor C),(Ob C) holds
( ( not C is empty & ( for f being Element of Mor C holds b1 . f = dom f ) & ( for f being Element of Mor C holds b2 . f = dom f ) implies b1 = b2 ) & ( C is empty & b1 = {} & b2 = {} implies b1 = b2 ) );
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
consistency
for b1 being Function of (Mor C),(Ob C) holds verum;
existence
( ( for b1 being Function of (Mor C),(Ob C) holds verum ) & ( not C is empty implies ex b1 being Function of (Mor C),(Ob C) st
for f being Element of Mor C holds b1 . f = cod f ) & ( C is empty implies ex b1 being Function of (Mor C),(Ob C) st b1 = {} ) );
uniqueness
for b1, b2 being Function of (Mor C),(Ob C) holds
( ( not C is empty & ( for f being Element of Mor C holds b1 . f = cod f ) & ( for f being Element of Mor C holds b2 . f = cod f ) implies b1 = b2 ) & ( C is empty & b1 = {} & b2 = {} implies b1 = b2 ) );
proof end;
end;

:: deftheorem Def30 defines SourceMap CAT_6:def 30 :
for C being composable with_identities CategoryStr
for b2 being Function of (Mor C),(Ob C) holds
( ( not C is empty implies ( b2 = SourceMap C iff for f being Element of Mor C holds b2 . f = dom f ) ) & ( C is empty implies ( b2 = SourceMap C iff b2 = {} ) ) );

:: deftheorem Def31 defines TargetMap CAT_6:def 31 :
for C being composable with_identities CategoryStr
for b2 being Function of (Mor C),(Ob C) holds
( ( not C is empty implies ( b2 = TargetMap C iff for f being Element of Mor C holds b2 . f = cod f ) ) & ( C is empty implies ( b2 = TargetMap C iff b2 = {} ) ) );

definition
let C be with_identities CategoryStr ;
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
consistency
for b1 being Function of (Ob C),(Mor C) holds verum;
existence
( ( for b1 being Function of (Ob C),(Mor C) holds verum ) & ( not C is empty implies ex b1 being Function of (Ob C),(Mor C) st
for o being Element of Ob C holds b1 . o = id- o ) & ( C is empty implies ex b1 being Function of (Ob C),(Mor C) st b1 = {} ) );
uniqueness
for b1, b2 being Function of (Ob C),(Mor C) holds
( ( not C is empty & ( for o being Element of Ob C holds b1 . o = id- o ) & ( for o being Element of Ob C holds b2 . o = id- o ) implies b1 = b2 ) & ( C is empty & b1 = {} & b2 = {} implies b1 = b2 ) );
proof end;
end;

:: deftheorem Def32 defines IdMap CAT_6:def 32 :
for C being with_identities CategoryStr
for b2 being Function of (Ob C),(Mor C) holds
( ( not C is empty implies ( b2 = IdMap C iff for o being Element of Ob C holds b2 . o = id- o ) ) & ( C is empty implies ( b2 = IdMap C iff b2 = {} ) ) );

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 )
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 )
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)
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 ) )
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;
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) #) is strict Category by Lm6;
end;

:: 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) #);

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

definition
let A be Category;
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 #) is strict category by Lm7;
end;

:: deftheorem defines alter CAT_6:def 34 :
for A being Category holds alter A = CategoryStr(# the carrier' of A, the Comp of A #);

registration
let A be Category;
cluster alter A -> non empty strict ;
correctness
coherence
not alter A is empty ;
;
end;

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
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 )
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)
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
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 )
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
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 )
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
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
proof end;

theorem Th50: :: CAT_6:49
for C1, C2 being Category st alter C1 ~= alter C2 holds
C1 ~= C2
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
proof end;

theorem :: CAT_6:51
for C being Category holds C ~= Alter (alter C) by Th51;

theorem :: CAT_6:52
for C being non empty category holds C ~= alter (Alter C)
proof end;