:: Introduction to Categories and Functors
:: by Czes{\l}aw Byli\'nski
::
:: Received October 25, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users


definition
attr c1 is strict ;
struct CatStr -> MultiGraphStruct ;
aggr CatStr(# carrier, carrier', Source, Target, Comp #) -> CatStr ;
sel Comp c1 -> PartFunc of [: the carrier' of c1, the carrier' of c1:], the carrier' of c1;
end;

definition
let C be CatStr ;
mode Object of C is Element of C;
mode Morphism of C is Element of the carrier' of C;
end;

:: Domain and codomain of a Morphism
registration
cluster non empty non void for CatStr ;
existence
ex b1 being CatStr st
( not b1 is void & not b1 is empty )
proof end;
end;

definition
let C be CatStr ;
let f, g be Morphism of C;
assume A1: [g,f] in dom the Comp of C ;
func g (*) f -> Morphism of C equals :Def1: :: CAT_1:def 1
 the Comp of C . (g,f);
coherence
the Comp of C . (g,f) is Morphism of C by A1, PARTFUN1:4;
end;

:: deftheorem Def1 defines (*) CAT_1:def 1 :
for C being CatStr
for f, g being Morphism of C st [g,f] in dom the Comp of C holds
g (*) f = the Comp of C . (g,f);

definition
let C be non empty non void CatStr ;
let a, b be Object of C;
func Hom (a,b) -> Subset of the carrier' of C equals :: CAT_1:def 4
 { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;
correctness
coherence
{ f where f is Morphism of C : ( dom f = a & cod f = b ) } is Subset of the carrier' of C;
proof end;
end;

:: deftheorem CAT_1:def 2 :
canceled;

:: deftheorem CAT_1:def 3 :
canceled;

:: deftheorem defines Hom CAT_1:def 4 :
for C being non empty non void CatStr
for a, b being Object of C holds Hom (a,b) = { f where f is Morphism of C : ( dom f = a & cod f = b ) } ;

theorem Th1: :: CAT_1:1
for C being non empty non void CatStr
for f being Morphism of C
for a, b being Object of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
proof end;

theorem :: CAT_1:2
for C being non empty non void CatStr
for f being Morphism of C holds Hom ((dom f),(cod f)) <> {} by Th1;

definition
let C be non empty non void CatStr ;
let a, b be Object of C;
assume A1: Hom (a,b) <> {} ;
mode Morphism of a,b -> Morphism of C means :Def3: :: CAT_1:def 5
it in Hom (a,b);
existence
ex b1 being Morphism of C st b1 in Hom (a,b) by A1, SUBSET_1:4;
end;

:: deftheorem Def3 defines Morphism CAT_1:def 5 :
for C being non empty non void CatStr
for a, b being Object of C st Hom (a,b) <> {} holds
for b4 being Morphism of C holds
( b4 is Morphism of a,b iff b4 in Hom (a,b) );

theorem :: CAT_1:3
canceled;

::$CT
theorem Th3: :: CAT_1:4
for C being non empty non void CatStr
for f being Morphism of C holds f is Morphism of dom f, cod f
proof end;

theorem Th4: :: CAT_1:5
for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( dom f = a & cod f = b )
proof end;

theorem :: CAT_1:6
for C being non empty non void CatStr
for a, b, c, d being Object of C
for f being Morphism of a,b
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (c,d) <> {} & f = h holds
( a = c & b = d )
proof end;

theorem Th6: :: CAT_1:7
for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g
proof end;

theorem Th7: :: CAT_1:8
for C being non empty non void CatStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}
proof end;

theorem :: CAT_1:9
for C being non empty non void CatStr
for a, b, c, d being Object of C
for f being Morphism of a,b st Hom (a,b), Hom (c,d) are_equipotent & Hom (a,b) = {f} holds
ex h being Morphism of c,d st Hom (c,d) = {h}
proof end;

:: Category
definition
let C be non empty non void CatStr ;
attr C is Category-like means :Def4: :: CAT_1:def 6
 for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f );
attr C is transitive means :Def5: :: CAT_1:def 7
 for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g );
attr C is associative means :Def6: :: CAT_1:def 8
 for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f;
attr C is reflexive means :Def7: :: CAT_1:def 9
 for b being Element of C holds Hom (b,b) <> {} ;
attr C is with_identities means :Def8: :: CAT_1:def 10
 for a being Element of C ex i being Morphism of a,a st
for b being Element of C holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) );
end;

:: deftheorem Def4 defines Category-like CAT_1:def 6 :
for C being non empty non void CatStr holds
( C is Category-like iff for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f ) );

:: deftheorem Def5 defines transitive CAT_1:def 7 :
for C being non empty non void CatStr holds
( C is transitive iff for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) );

:: deftheorem Def6 defines associative CAT_1:def 8 :
for C being non empty non void CatStr holds
( C is associative iff for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f );

:: deftheorem Def7 defines reflexive CAT_1:def 9 :
for C being non empty non void CatStr holds
( C is reflexive iff for b being Element of C holds Hom (b,b) <> {} );

:: deftheorem Def8 defines with_identities CAT_1:def 10 :
for C being non empty non void CatStr holds
( C is with_identities iff for a being Element of C ex i being Morphism of a,a st
for b being Element of C holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) ) );

definition
let o, m be object ;
func 1Cat (o,m) -> strict CatStr equals :: CAT_1:def 11
 CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);
correctness
coherence
CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) is strict CatStr ;
;
end;

:: deftheorem defines 1Cat CAT_1:def 11 :
for o, m being object holds 1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #);

registration
let o, m be object ;
cluster 1Cat (o,m) -> non empty trivial non void trivial' strict ;
coherence
( not 1Cat (o,m) is empty & 1Cat (o,m) is trivial & not 1Cat (o,m) is void & 1Cat (o,m) is trivial' ) ;
end;

registration
cluster non empty trivial non void -> non empty non void transitive reflexive for CatStr ;
coherence
for b1 being non empty non void CatStr st not b1 is empty & b1 is trivial holds
( b1 is transitive & b1 is reflexive )
proof end;
end;

registration
cluster non empty non void trivial' -> non empty non void associative with_identities for CatStr ;
coherence
for b1 being non empty non void CatStr st not b1 is void & b1 is trivial' holds
( b1 is associative & b1 is with_identities )
proof end;
end;

registration
let o, m be object ;
cluster 1Cat (o,m) -> strict Category-like ;
coherence
1Cat (o,m) is Category-like
proof end;
end;

registration
cluster non empty non void V62() strict Category-like transitive associative reflexive with_identities for CatStr ;
existence
ex b1 being non empty non void CatStr st
( b1 is reflexive & b1 is transitive & b1 is associative & b1 is with_identities & b1 is Category-like & not b1 is void & not b1 is empty & b1 is strict )
proof end;
end;

definition
mode Category is non empty non void Category-like transitive associative reflexive with_identities CatStr ;
end;

registration
let C be non empty non void reflexive CatStr ;
let a be Object of C;
cluster Hom (a,a) -> non empty ;
coherence
not Hom (a,a) is empty by Def7;
end;

theorem :: CAT_1:10
canceled;

theorem Th9: :: CAT_1:11
for o, m being set
for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f in Hom (a,b)
proof end;

theorem :: CAT_1:12
for o, m being set
for a, b being Object of (1Cat (o,m))
for f being Morphism of (1Cat (o,m)) holds f is Morphism of a,b
proof end;

theorem :: CAT_1:13
for o, m being set
for a, b being Object of (1Cat (o,m)) holds Hom (a,b) <> {} by Th9;

theorem :: CAT_1:14
for o, m being set
for a, b, c, d being Object of (1Cat (o,m))
for f being Morphism of a,b
for g being Morphism of c,d holds f = g
proof end;

theorem :: CAT_1:15
for C being Category
for f, g being Morphism of C holds
( dom g = cod f iff [g,f] in dom the Comp of C ) by Def4;

theorem Th14: :: CAT_1:16
for C being Category
for f, g being Morphism of C st dom g = cod f holds
g (*) f = the Comp of C . (g,f)
proof end;

theorem :: CAT_1:17
for C being Category
for f, g being Morphism of C st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) by Def5;

theorem :: CAT_1:18
for C being Category
for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f by Def6;

definition
let C be non empty non void reflexive with_identities CatStr ;
let a be Object of C;
func id a -> Morphism of a,a means :Def10: :: CAT_1:def 12
 for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) it = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds it (*) f = f ) );
existence
ex b1 being Morphism of a,a st
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b1 (*) f = f ) ) by Def8;
uniqueness
for b1, b2 being Morphism of a,a st ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b1 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b1 (*) f = f ) ) ) & ( for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b2 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b2 (*) f = f ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines id CAT_1:def 12 :
for C being non empty non void reflexive with_identities CatStr
for a being Object of C
for b3 being Morphism of a,a holds
( b3 = id a iff for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) b3 = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds b3 (*) f = f ) ) );

theorem :: CAT_1:19
canceled;

theorem :: CAT_1:20
canceled;

::$CT 2
theorem :: CAT_1:21
for C being Category
for b being Object of C
for f being Morphism of C st cod f = b holds
(id b) (*) f = f
proof end;

theorem :: CAT_1:22
for C being Category
for b being Object of C
for g being Morphism of C st dom g = b holds
g (*) (id b) = g
proof end;

theorem Th19: :: CAT_1:23
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g (*) f in Hom (a,c)
proof end;

definition
let C be Category;
let a, b, c be Object of C;
let f be Morphism of a,b;
let g be Morphism of b,c;
assume A1: ( Hom (a,b) <> {} & Hom (b,c) <> {} ) ;
func g * f -> Morphism of a,c equals :Def11: :: CAT_1:def 13
g (*) f;
correctness
coherence
g (*) f is Morphism of a,c;
proof end;
end;

:: deftheorem Def11 defines * CAT_1:def 13 :
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} holds
g * f = g (*) f;

theorem :: CAT_1:24
for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
Hom (a,c) <> {} by Th19;

theorem Th21: :: CAT_1:25
for C being Category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of b,c
for h being Morphism of c,d st Hom (a,b) <> {} & Hom (b,c) <> {} & Hom (c,d) <> {} holds
(h * g) * f = h * (g * f)
proof end;

theorem :: CAT_1:26
canceled;

::$CT
theorem :: CAT_1:27
for C being Category
for a being Object of C holds id a in Hom (a,a) by Def3;

theorem Th23: :: CAT_1:28
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
(id b) * f = f
proof end;

theorem Th24: :: CAT_1:29
for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
g * (id b) = g
proof end;

registration
let C be Category;
let a be Object of C;
let f be Morphism of a,a;
A1: Hom (a,a) <> {} ;
reduce f * (id a) to f;
reducibility
f * (id a) = f by A1, Th24;
reduce (id a) * f to f;
reducibility
(id a) * f = f by A1, Th23;
end;

theorem :: CAT_1:30
for C being Category
for a being Object of C holds (id a) * (id a) = id a ;

:: Monics, Epis
definition
let C be Category;
let b, c be Object of C;
let g be Morphism of b,c;
attr g is monic means :: CAT_1:def 14
( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 ) );
end;

:: deftheorem defines monic CAT_1:def 14 :
for C being Category
for b, c being Object of C
for g being Morphism of b,c holds
( g is monic iff ( Hom (b,c) <> {} & ( for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 ) ) );

definition
let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;
attr f is epi means :: CAT_1:def 15
( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ) );
end;

:: deftheorem defines epi CAT_1:def 15 :
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is epi iff ( Hom (a,b) <> {} & ( for c being Object of C st Hom (b,c) <> {} holds
for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds
g1 = g2 ) ) );

definition
let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;
attr f is invertible means :: CAT_1:def 16
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) );
end;

:: deftheorem defines invertible CAT_1:def 16 :
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is invertible iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) );

theorem :: CAT_1:31
for C being Category
for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) ;

theorem :: CAT_1:32
for C being Category
for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st g is monic & h is monic holds
h * g is monic
proof end;

theorem :: CAT_1:33
for C being Category
for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st Hom (b,c) <> {} & Hom (c,d) <> {} & h * g is monic holds
g is monic
proof end;

theorem :: CAT_1:34
for C being Category
for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
g is monic
proof end;

theorem :: CAT_1:35
for C being Category
for b being Object of C holds id b is monic
proof end;

theorem :: CAT_1:36
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is epi iff for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * f = g2 * f holds
g1 = g2 ) ;

theorem :: CAT_1:37
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is epi & g is epi holds
g * f is epi
proof end;

theorem :: CAT_1:38
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} & Hom (b,c) <> {} & g * f is epi holds
g is epi
proof end;

theorem :: CAT_1:39
for C being Category
for a, b being Object of C
for h being Morphism of a,b
for g being Morphism of b,a st Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b holds
h is epi
proof end;

theorem :: CAT_1:40
for C being Category
for b being Object of C holds id b is epi
proof end;

theorem :: CAT_1:41
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is invertible iff ( Hom (b,a) <> {} & ex g being Morphism of b,a st
( f * g = id b & g * f = id a ) ) ) ;

theorem Th37: :: CAT_1:42
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & Hom (b,a) <> {} holds
for g1, g2 being Morphism of b,a st f * g1 = id b & g2 * f = id a holds
g1 = g2
proof end;

definition
let C be Category;
let a, b be Object of C;
let f be Morphism of a,b;
assume A1: f is invertible ;
func f " -> Morphism of b,a means :Def15: :: CAT_1:def 17
( f * it = id b & it * f = id a );
existence
ex b1 being Morphism of b,a st
( f * b1 = id b & b1 * f = id a ) by A1;
uniqueness
for b1, b2 being Morphism of b,a st f * b1 = id b & b1 * f = id a & f * b2 = id b & b2 * f = id a holds
b1 = b2 by A1, Th37;
end;

:: deftheorem Def15 defines " CAT_1:def 17 :
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
for b5 being Morphism of b,a holds
( b5 = f " iff ( f * b5 = id b & b5 * f = id a ) );

theorem :: CAT_1:43
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
( f is monic & f is epi )
proof end;

theorem :: CAT_1:44
for C being Category
for a being Object of C holds id a is invertible
proof end;

theorem Th40: :: CAT_1:45
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
g * f is invertible
proof end;

theorem :: CAT_1:46
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is invertible holds
f " is invertible
proof end;

theorem :: CAT_1:47
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st f is invertible & g is invertible holds
(g * f) " = (f ") * (g ")
proof end;

definition
let C be Category;
let a be Object of C;
attr a is terminal means :: CAT_1:def 18
 for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g );
attr a is initial means :: CAT_1:def 19
 for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g );
let b be Object of C;
pred a,b are_isomorphic means :: CAT_1:def 20
 ex f being Morphism of a,b st f is invertible ;
reflexivity
for a being Object of C ex f being Morphism of a,a st f is invertible
proof end;
symmetry
for a, b being Object of C st ex f being Morphism of a,b st f is invertible holds
ex f being Morphism of b,a st f is invertible
proof end;
end;

:: deftheorem defines terminal CAT_1:def 18 :
for C being Category
for a being Object of C holds
( a is terminal iff for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g ) );

:: deftheorem defines initial CAT_1:def 19 :
for C being Category
for a being Object of C holds
( a is initial iff for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g ) );

:: deftheorem defines are_isomorphic CAT_1:def 20 :
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ex f being Morphism of a,b st f is invertible );

theorem :: CAT_1:48
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex f being Morphism of a,b ex f9 being Morphism of b,a st
( f * f9 = id b & f9 * f = id a ) ) )
proof end;

theorem :: CAT_1:49
for C being Category
for a being Object of C holds
( a is initial iff for b being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
proof end;

theorem Th45: :: CAT_1:50
for C being Category
for a being Object of C st a is initial holds
for h being Morphism of a,a holds id a = h
proof end;

theorem :: CAT_1:51
for C being Category
for a, b being Object of C st a is initial & b is initial holds
a,b are_isomorphic
proof end;

theorem :: CAT_1:52
for C being Category
for a, b being Object of C st a is initial & a,b are_isomorphic holds
b is initial
proof end;

theorem :: CAT_1:53
for C being Category
for b being Object of C holds
( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )
proof end;

theorem Th49: :: CAT_1:54
for C being Category
for a being Object of C st a is terminal holds
for h being Morphism of a,a holds id a = h
proof end;

theorem :: CAT_1:55
for C being Category
for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic
proof end;

theorem :: CAT_1:56
for C being Category
for a, b being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal
proof end;

theorem :: CAT_1:57
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds
f is monic
proof end;

registration
let C be Category;
let a be Object of C;
reduce dom (id a) to a;
reducibility
dom (id a) = a
proof end;
reduce cod (id a) to a;
reducibility
cod (id a) = a
proof end;
end;

theorem Th53: :: CAT_1:58
for C being Category
for a being Object of C holds
( dom (id a) = a & cod (id a) = a ) ;

theorem Th54: :: CAT_1:59
for C being Category
for a, b being Object of C st id a = id b holds
a = b
proof end;

theorem :: CAT_1:60
for C being Category
for a, b, c being Object of C st a,b are_isomorphic & b,c are_isomorphic holds
a,c are_isomorphic
proof end;

:: Functors (Covariant Functors)
definition
let C, D be Category;
mode Functor of C,D -> Function of the carrier' of C, the carrier' of D means :Def19: :: CAT_1:def 21
( ( for c being Element of C ex d being Element of D st it . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( it . (id (dom f)) = id (dom (it . f)) & it . (id (cod f)) = id (cod (it . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
it . (g (*) f) = (it . g) (*) (it . f) ) );
existence
ex b1 being Function of the carrier' of C, the carrier' of D st
( ( for c being Element of C ex d being Element of D st b1 . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( b1 . (id (dom f)) = id (dom (b1 . f)) & b1 . (id (cod f)) = id (cod (b1 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b1 . (g (*) f) = (b1 . g) (*) (b1 . f) ) )
proof end;
end;

:: deftheorem Def19 defines Functor CAT_1:def 21 :
for C, D being Category
for b3 being Function of the carrier' of C, the carrier' of D holds
( b3 is Functor of C,D iff ( ( for c being Element of C ex d being Element of D st b3 . (id c) = id d ) & ( for f being Element of the carrier' of C holds
( b3 . (id (dom f)) = id (dom (b3 . f)) & b3 . (id (cod f)) = id (cod (b3 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b3 . (g (*) f) = (b3 . g) (*) (b3 . f) ) ) );

theorem Th56: :: CAT_1:61
for C, D being Category
for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) & ( for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D
proof end;

theorem :: CAT_1:62
for C, D being Category
for T being Functor of C,D
for c being Object of C ex d being Object of D st T . (id c) = id d by Def19;

theorem :: CAT_1:63
for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) by Def19;

theorem Th59: :: CAT_1:64
for C, D being Category
for T being Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
( dom (T . g) = cod (T . f) & T . (g (*) f) = (T . g) (*) (T . f) )
proof end;

theorem Th60: :: CAT_1:65
for C, D being Category
for T being Function of the carrier' of C, the carrier' of D
for F being Function of the carrier of C, the carrier of D st ( for c being Object of C holds T . (id c) = id (F . c) ) & ( for f being Morphism of C holds
( F . (dom f) = dom (T . f) & F . (cod f) = cod (T . f) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) holds
T is Functor of C,D
proof end;

:: Object Function of a Functor
definition
let C, D be Category;
let F be Function of the carrier' of C, the carrier' of D;
assume A1: for c being Element of C ex d being Element of D st F . (id c) = id d ;
func Obj F -> Function of the carrier of C, the carrier of D means :Def20: :: CAT_1:def 22
 for c being Element of C
for d being Element of D st F . (id c) = id d holds
it . c = d;
existence
ex b1 being Function of the carrier of C, the carrier of D st
for c being Element of C
for d being Element of D st F . (id c) = id d holds
b1 . c = d
proof end;
uniqueness
for b1, b2 being Function of the carrier of C, the carrier of D st ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
b1 . c = d ) & ( for c being Element of C
for d being Element of D st F . (id c) = id d holds
b2 . c = d ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines Obj CAT_1:def 22 :
for C, D being Category
for F being Function of the carrier' of C, the carrier' of D st ( for c being Element of C ex d being Element of D st F . (id c) = id d ) holds
for b4 being Function of the carrier of C, the carrier of D holds
( b4 = Obj F iff for c being Element of C
for d being Element of D st F . (id c) = id d holds
b4 . c = d );

theorem :: CAT_1:66
for C, D being Category
for T being Function of the carrier' of C, the carrier' of D st ( for c being Object of C ex d being Object of D st T . (id c) = id d ) holds
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d by Def20;

theorem Th62: :: CAT_1:67
for C, D being Category
for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
(Obj T) . c = d
proof end;

theorem Th63: :: CAT_1:68
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . (id c) = id ((Obj T) . c)
proof end;

theorem Th64: :: CAT_1:69
for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( (Obj T) . (dom f) = dom (T . f) & (Obj T) . (cod f) = cod (T . f) )
proof end;

definition
let C, D be Category;
let T be Functor of C,D;
let c be Object of C;
func T . c -> Object of D equals :: CAT_1:def 23
(Obj T) . c;
correctness
coherence
(Obj T) . c is Object of D;
;
end;

:: deftheorem defines . CAT_1:def 23 :
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . c = (Obj T) . c;

theorem :: CAT_1:70
for C, D being Category
for T being Functor of C,D
for c being Object of C
for d being Object of D st T . (id c) = id d holds
T . c = d by Th62;

theorem :: CAT_1:71
for C, D being Category
for T being Functor of C,D
for c being Object of C holds T . (id c) = id (T . c) by Th63;

theorem :: CAT_1:72
for C, D being Category
for T being Functor of C,D
for f being Morphism of C holds
( T . (dom f) = dom (T . f) & T . (cod f) = cod (T . f) ) by Th64;

theorem Th68: :: CAT_1:73
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D holds S * T is Functor of B,D
proof end;

:: Composition of Functors
definition
let B, C, D be Category;
let T be Functor of B,C;
let S be Functor of C,D;
:: original: *
redefine func S * T -> Functor of B,D;
coherence
T * S is Functor of B,D by Th68;
end;

theorem Th69: :: CAT_1:74
for C being Category holds id the carrier' of C is Functor of C,C
proof end;

theorem Th70: :: CAT_1:75
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (Obj (S * T)) . b = (Obj S) . ((Obj T) . b)
proof end;

theorem :: CAT_1:76
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D
for b being Object of B holds (S * T) . b = S . (T . b) by Th70;

:: Identity Functor
definition
let C be Category;
func id C -> Functor of C,C equals :: CAT_1:def 24
 id the carrier' of C;
coherence
id the carrier' of C is Functor of C,C by Th69;
end;

:: deftheorem defines id CAT_1:def 24 :
for C being Category holds id C = id the carrier' of C;

theorem Th72: :: CAT_1:77
for C being Category
for c being Object of C holds (Obj (id C)) . c = c
proof end;

theorem Th73: :: CAT_1:78
for C being Category holds Obj (id C) = id the carrier of C
proof end;

theorem :: CAT_1:79
for C being Category
for c being Object of C holds (id C) . c = c by Th72;

definition
let C, D be Category;
let T be Functor of C,D;
attr T is isomorphic means :: CAT_1:def 25
( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D );
attr T is full means :: CAT_1:def 26
 for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds
for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f );
attr T is faithful means :: CAT_1:def 27
 for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2;
end;

:: deftheorem defines isomorphic CAT_1:def 25 :
for C, D being Category
for T being Functor of C,D holds
( T is isomorphic iff ( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D ) );

:: deftheorem defines full CAT_1:def 26 :
for C, D being Category
for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C st Hom ((T . c),(T . c9)) <> {} holds
for g being Morphism of T . c,T . c9 holds
( Hom (c,c9) <> {} & ex f being Morphism of c,c9 st g = T . f ) );

:: deftheorem defines faithful CAT_1:def 27 :
for C, D being Category
for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2 );

theorem :: CAT_1:80
for C being Category holds id C is isomorphic
proof end;

theorem Th76: :: CAT_1:81
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C
for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
proof end;

theorem Th77: :: CAT_1:82
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f in Hom ((T . c),(T . c9))
proof end;

theorem Th78: :: CAT_1:83
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9
proof end;

theorem Th79: :: CAT_1:84
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
Hom ((T . c),(T . c9)) <> {}
proof end;

theorem :: CAT_1:85
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D st T is full & S is full holds
S * T is full
proof end;

theorem :: CAT_1:86
for B, C, D being Category
for T being Functor of B,C
for S being Functor of C,D st T is faithful & S is faithful holds
S * T is faithful
proof end;

theorem Th82: :: CAT_1:87
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))
proof end;

definition
let C, D be Category;
let T be Functor of C,D;
let c, c9 be Object of C;
func hom (T,c,c9) -> Function of (Hom (c,c9)),(Hom ((T . c),(T . c9))) equals :: CAT_1:def 28
T | (Hom (c,c9));
correctness
coherence
T | (Hom (c,c9)) is Function of (Hom (c,c9)),(Hom ((T . c),(T . c9)));
proof end;
end;

:: deftheorem defines hom CAT_1:def 28 :
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C holds hom (T,c,c9) = T | (Hom (c,c9));

theorem Th83: :: CAT_1:88
for C, D being Category
for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
proof end;

theorem :: CAT_1:89
for C, D being Category
for T being Functor of C,D holds
( T is full iff for c, c9 being Object of C holds rng (hom (T,c,c9)) = Hom ((T . c),(T . c9)) )
proof end;

theorem :: CAT_1:90
for C, D being Category
for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )
proof end;

theorem :: CAT_1:91
for C being Category
for a, b being Element of C st Hom (a,b) <> {} holds
ex m being Morphism of a,b st m in Hom (a,b)
proof end;

theorem :: CAT_1:92
for C being Category holds the carrier' of C = union { (Hom (a,b)) where a, b is Object of C : verum }
proof end;