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


begin

definition
attr c1 is strict ;
struct CatStr -> MultiGraphStruct ;
aggr CatStr(# carrier, carrier', Source, Target, Comp, Id #) -> CatStr ;
sel Comp c1 -> PartFunc of [: the carrier' of c1, the carrier' of c1:], the carrier' of c1;
sel Id c1 -> Function of 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;

registration
cluster non empty non void CatStr ;
existence
ex b1 being CatStr st
( not b1 is void & not b1 is empty )
proof end;
end;

definition
canceled;
canceled;
canceled;
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 :Def4: :: CAT_1:def 4
 the Comp of C . (g,f);
coherence
the Comp of C . (g,f) is Morphism of C by A1, PARTFUN1:27;
end;

:: deftheorem CAT_1:def 1 :
canceled;

:: deftheorem CAT_1:def 2 :
canceled;

:: deftheorem CAT_1:def 3 :
canceled;

:: deftheorem Def4 defines * CAT_1:def 4 :
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 be Object of C;
func id a -> Morphism of C equals :: CAT_1:def 5
 the Id of C . a;
correctness
coherence
the Id of C . a is Morphism of C;
;
end;

:: deftheorem defines id CAT_1:def 5 :
for C being non empty non void CatStr
for a being Object of C holds id a = the Id of C . a;

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 6
 { 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 defines Hom CAT_1:def 6 :
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 :: CAT_1:1
canceled;

theorem :: CAT_1:2
canceled;

theorem :: CAT_1:3
canceled;

theorem :: CAT_1:4
canceled;

theorem :: CAT_1:5
canceled;

theorem :: CAT_1:6
canceled;

theorem :: CAT_1:7
canceled;

theorem :: CAT_1:8
canceled;

theorem :: CAT_1:9
canceled;

theorem :: CAT_1:10
canceled;

theorem :: CAT_1:11
canceled;

theorem :: CAT_1:12
canceled;

theorem :: CAT_1:13
canceled;

theorem :: CAT_1:14
canceled;

theorem :: CAT_1:15
canceled;

theorem :: CAT_1:16
canceled;

theorem :: CAT_1:17
canceled;

theorem Th18: :: CAT_1:18
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:19
for C being non empty non void CatStr
for f being Morphism of C holds Hom ((dom f),(cod f)) <> {} by Th18;

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 :Def7: :: CAT_1:def 7
it in Hom (a,b);
existence
ex b1 being Morphism of C st b1 in Hom (a,b) by A1, SUBSET_1:10;
end;

:: deftheorem Def7 defines Morphism CAT_1:def 7 :
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:20
canceled;

theorem :: CAT_1:21
for C being non empty non void CatStr
for a, b being Object of C
for f being set st f in Hom (a,b) holds
f is Morphism of a,b by Def7;

theorem Th22: :: CAT_1:22
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 Th23: :: CAT_1:23
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:24
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 Th25: :: CAT_1:25
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 Th26: :: CAT_1:26
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:27
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;

Lm1: now
let o, m be set ; :: thesis: for C being non empty non void CatStr st C = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m) #) holds
( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . [g,f]) = the Source of C . f & the Target of C . ( the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) ) ) )
let C be non empty non void CatStr ; :: thesis: ( C = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m) #) implies ( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . [g,f]) = the Source of C . f & the Target of C . ( the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) ) ) ) )
assume A1: C = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(o :-> m) #) ; :: thesis: ( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . [g,f]) = the Source of C . f & the Target of C . ( the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) ) ) )
set CP = the Comp of C;
set CD = the Source of C;
set CC = the Target of C;
set CI = the Id of C;
thus for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) :: thesis: ( ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . [g,f]) = the Source of C . f & the Target of C . ( the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) ) ) )
proof
let f, g be Element of the carrier' of C; :: thesis: ( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f )
A2: dom the Comp of C = {[m,m]} by A1, FUNCOP_1:19;
( f = m & g = m ) by A1, TARSKI:def 1;
hence ( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) by A1, A2, TARSKI:def 1; :: thesis: verum
end;
thus for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . [g,f]) = the Source of C . f & the Target of C . ( the Comp of C . [g,f]) = the Target of C . g ) :: thesis: ( ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) ) ) )
proof
let f, g be Element of the carrier' of C; :: thesis: ( the Source of C . g = the Target of C . f implies ( the Source of C . ( the Comp of C . [g,f]) = the Source of C . f & the Target of C . ( the Comp of C . [g,f]) = the Target of C . g ) )
the Comp of C . (g,f) = m by A1, FUNCOP_1:92;
then reconsider gf = the Comp of C . [g,f] as Element of the carrier' of C by A1, TARSKI:def 1;
the Source of C . gf = o by A1, FUNCT_2:65;
hence ( the Source of C . g = the Target of C . f implies ( the Source of C . ( the Comp of C . [g,f]) = the Source of C . f & the Target of C . ( the Comp of C . [g,f]) = the Target of C . g ) ) by A1, FUNCT_2:65; :: thesis: verum
end;
thus for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] :: thesis: for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) )
proof
let f, g, h be Element of the carrier' of C; :: thesis: ( the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f implies the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] )
( the Comp of C . (g,f) = m & the Comp of C . (h,g) = m ) by A1, FUNCOP_1:92;
then reconsider gf = the Comp of C . (g,f), hg = the Comp of C . (h,g) as Element of the carrier' of C by A1, TARSKI:def 1;
( the Comp of C . (h,gf) = m & the Comp of C . (hg,f) = m ) by A1, FUNCOP_1:92;
hence ( the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f implies the Comp of C . [h,( the Comp of C . [g,f])] = the Comp of C . [( the Comp of C . [h,g]),f] ) ; :: thesis: verum
end;
let b be Element of C; :: thesis: ( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) )
b = o by A1, TARSKI:def 1;
hence ( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b ) by A1, FUNCT_2:65; :: thesis: ( ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g ) )
thus for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f :: thesis: for g being Element of the carrier' of C holds the Comp of C . (g,( the Id of C . b)) = g
proof
let f be Element of the carrier' of C; :: thesis: ( the Target of C . f = b implies the Comp of C . (( the Id of C . b),f) = f )
f = m by A1, TARSKI:def 1;
hence ( the Target of C . f = b implies the Comp of C . (( the Id of C . b),f) = f ) by A1, FUNCOP_1:92; :: thesis: verum
end;
let g be Element of the carrier' of C; :: thesis: the Comp of C . (g,( the Id of C . b)) = g
g = m by A1, TARSKI:def 1;
hence the Comp of C . (g,( the Id of C . b)) = g by A1, FUNCOP_1:92; :: thesis: verum
end;

definition
let C be CatStr ;
attr C is Category-like means :Def8: :: CAT_1:def 8
( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . (g,f)) = the Source of C . f & the Target of C . ( the Comp of C . (g,f)) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . (h,( the Comp of C . (g,f))) = the Comp of C . (( the Comp of C . (h,g)),f) ) & ( for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C st the Source of C . g = b holds
the Comp of C . (g,( the Id of C . b)) = g ) ) ) );
end;

:: deftheorem Def8 defines Category-like CAT_1:def 8 :
for C being CatStr holds
( C is Category-like iff ( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . ( the Comp of C . (g,f)) = the Source of C . f & the Target of C . ( the Comp of C . (g,f)) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . (h,( the Comp of C . (g,f))) = the Comp of C . (( the Comp of C . (h,g)),f) ) & ( for b being Element of C holds
( the Source of C . ( the Id of C . b) = b & the Target of C . ( the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (( the Id of C . b),f) = f ) & ( for g being Element of the carrier' of C st the Source of C . g = b holds
the Comp of C . (g,( the Id of C . b)) = g ) ) ) ) );

registration
cluster non empty non void strict Category-like CatStr ;
existence
ex b1 being CatStr st
( 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 CatStr ;
end;

theorem :: CAT_1:28
canceled;

theorem :: CAT_1:29
for C being non empty non void CatStr st ( for f, g being Morphism of C holds
( [g,f] in dom the Comp of C iff dom g = cod f ) ) & ( for f, g being Morphism of C st dom g = cod f holds
( dom (g * f) = dom f & cod (g * f) = cod g ) ) & ( for f, g, h being Morphism of C st dom h = cod g & dom g = cod f holds
h * (g * f) = (h * g) * f ) & ( for b being Object of C holds
( dom (id b) = b & cod (id b) = b & ( for f being Morphism of C st cod f = b holds
(id b) * f = f ) & ( for g being Morphism of C st dom g = b holds
g * (id b) = g ) ) ) holds
C is Category-like
proof end;

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

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

theorem :: CAT_1:30
canceled;

theorem :: CAT_1:31
canceled;

theorem :: CAT_1:32
canceled;

theorem :: CAT_1:33
canceled;

theorem :: CAT_1:34
canceled;

theorem :: CAT_1:35
canceled;

theorem Th36: :: CAT_1:36
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:37
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:38
for o, m being set
for a, b being Object of (1Cat (o,m)) holds Hom (a,b) <> {} by Th36;

theorem :: CAT_1:39
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:40
for C being Category
for g, f being Morphism of C holds
( dom g = cod f iff [g,f] in dom the Comp of C ) by Def8;

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

theorem Th42: :: CAT_1:42
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 )
proof end;

theorem Th43: :: CAT_1:43
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
proof end;

theorem :: CAT_1:44
for C being Category
for b being Object of C holds
( dom (id b) = b & cod (id b) = b ) by Def8;

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

theorem Th46: :: CAT_1:46
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 Th47: :: CAT_1:47
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;

definition
let C be Category;
let g be Morphism of C;
attr g is monic means :: CAT_1:def 10
 for f1, f2 being Morphism of C st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g * f1 = g * f2 holds
f1 = f2;
end;

:: deftheorem defines monic CAT_1:def 10 :
for C being Category
for g being Morphism of C holds
( g is monic iff for f1, f2 being Morphism of C st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g * f1 = g * f2 holds
f1 = f2 );

definition
let C be Category;
let f be Morphism of C;
attr f is epi means :: CAT_1:def 11
 for g1, g2 being Morphism of C st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1 * f = g2 * f holds
g1 = g2;
end;

:: deftheorem defines epi CAT_1:def 11 :
for C being Category
for f being Morphism of C holds
( f is epi iff for g1, g2 being Morphism of C st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1 * f = g2 * f holds
g1 = g2 );

definition
let C be Category;
let f be Morphism of C;
attr f is invertible means :: CAT_1:def 12
 ex g being Morphism of C st
( dom g = cod f & cod g = dom f & f * g = id (cod f) & g * f = id (dom f) );
end;

:: deftheorem defines invertible CAT_1:def 12 :
for C being Category
for f being Morphism of C holds
( f is invertible iff ex g being Morphism of C st
( dom g = cod f & cod g = dom f & f * g = id (cod f) & g * f = id (dom f) ) );

theorem :: CAT_1:48
canceled;

theorem :: CAT_1:49
canceled;

theorem :: CAT_1:50
canceled;

theorem Th51: :: CAT_1:51
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;

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

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 :Def13: :: CAT_1:def 13
g * f;
correctness
coherence
g * f is Morphism of a,c;
proof end;
end;

:: deftheorem Def13 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:53
canceled;

theorem Th54: :: CAT_1:54
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 Th55: :: CAT_1:55
for C being Category
for a being Object of C holds id a in Hom (a,a)
proof end;

theorem :: CAT_1:56
for C being Category
for a being Object of C holds Hom (a,a) <> {} by Th55;

definition
let C be Category;
let a be Object of C;
:: original: id
redefine func id a -> Morphism of a,a;
coherence
id a is Morphism of a,a
proof end;
end;

theorem Th57: :: 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) <> {} holds
(id b) * f = f
proof end;

theorem Th58: :: CAT_1:58
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;

theorem Th59: :: CAT_1:59
for C being Category
for a being Object of C holds (id a) * (id a) = id a
proof end;

theorem Th60: :: CAT_1:60
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 )
proof end;

theorem :: CAT_1:61
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) <> {} & g is monic & h is monic holds
h * g is monic
proof end;

theorem :: CAT_1:62
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:63
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:64
for C being Category
for b being Object of C holds id b is monic
proof end;

theorem Th65: :: CAT_1:65
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 )
proof end;

theorem :: CAT_1:66
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) <> {} & f is epi & g is epi holds
g * f is epi
proof end;

theorem :: CAT_1:67
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:68
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:69
for C being Category
for b being Object of C holds id b is epi
proof end;

theorem Th70: :: CAT_1:70
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 ) ) )
proof end;

theorem Th71: :: CAT_1:71
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 that
A1: Hom (a,b) <> {} and
A2: f is invertible ;
func f " -> Morphism of b,a means :Def14: :: CAT_1:def 14
( 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, A2, Th70;
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
proof end;
end;

:: deftheorem Def14 defines " CAT_1:def 14 :
for C being Category
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & 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:72
canceled;

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

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

theorem Th75: :: CAT_1:75
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) <> {} & f is invertible & g is invertible holds
g * f is invertible
proof end;

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

theorem :: CAT_1:77
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) <> {} & 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 :Def15: :: CAT_1:def 15
 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 :Def16: :: CAT_1:def 16
 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 :Def17: :: CAT_1:def 17
( Hom (a,b) <> {} & ex f being Morphism of a,b st f is invertible );
end;

:: deftheorem Def15 defines terminal CAT_1:def 15 :
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 Def16 defines initial CAT_1:def 16 :
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 Def17 defines are_isomorphic CAT_1:def 17 :
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ( Hom (a,b) <> {} & ex f being Morphism of a,b st f is invertible ) );

theorem :: CAT_1:78
canceled;

theorem :: CAT_1:79
canceled;

theorem :: CAT_1:80
canceled;

theorem Th81: :: CAT_1:81
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:82
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 Th83: :: CAT_1:83
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:84
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:85
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:86
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 Th87: :: CAT_1:87
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:88
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:89
for C being Category
for b, a being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal
proof end;

theorem :: CAT_1:90
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;

theorem :: CAT_1:91
for C being Category
for a being Object of C holds a,a are_isomorphic
proof end;

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

theorem :: CAT_1:93
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;

definition
let C, D be Category;
mode Functor of C,D -> Function of the carrier' of C, the carrier' of D means :Def18: :: CAT_1:def 18
( ( for c being Element of C ex d being Element of D st it . ( the Id of C . c) = the Id of D . d ) & ( for f being Element of the carrier' of C holds
( it . ( the Id of C . ( the Source of C . f)) = the Id of D . ( the Source of D . (it . f)) & it . ( the Id of C . ( the Target of C . f)) = the Id of D . ( the Target of D . (it . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
it . ( the Comp of C . (g,f)) = the Comp of D . ((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 . ( the Id of C . c) = the Id of D . d ) & ( for f being Element of the carrier' of C holds
( b1 . ( the Id of C . ( the Source of C . f)) = the Id of D . ( the Source of D . (b1 . f)) & b1 . ( the Id of C . ( the Target of C . f)) = the Id of D . ( the Target of D . (b1 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b1 . ( the Comp of C . (g,f)) = the Comp of D . ((b1 . g),(b1 . f)) ) )
proof end;
end;

:: deftheorem Def18 defines Functor CAT_1:def 18 :
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 . ( the Id of C . c) = the Id of D . d ) & ( for f being Element of the carrier' of C holds
( b3 . ( the Id of C . ( the Source of C . f)) = the Id of D . ( the Source of D . (b3 . f)) & b3 . ( the Id of C . ( the Target of C . f)) = the Id of D . ( the Target of D . (b3 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b3 . ( the Comp of C . (g,f)) = the Comp of D . ((b3 . g),(b3 . f)) ) ) );

theorem :: CAT_1:94
canceled;

theorem :: CAT_1:95
canceled;

theorem Th96: :: CAT_1:96
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 Th97: :: CAT_1:97
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
proof end;

theorem :: CAT_1:98
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 Def18;

theorem Th99: :: CAT_1:99
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 Th100: :: CAT_1:100
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;

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 . ( the Id of C . c) = the Id of D . d ;
func Obj F -> Function of the carrier of C, the carrier of D means :Def19: :: CAT_1:def 19
 for c being Element of C
for d being Element of D st F . ( the Id of C . c) = the Id of D . 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 . ( the Id of C . c) = the Id of D . 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 . ( the Id of C . c) = the Id of D . d holds
b1 . c = d ) & ( for c being Element of C
for d being Element of D st F . ( the Id of C . c) = the Id of D . d holds
b2 . c = d ) holds
b1 = b2
proof end;
end;

:: deftheorem Def19 defines Obj CAT_1:def 19 :
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 . ( the Id of C . c) = the Id of D . 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 . ( the Id of C . c) = the Id of D . d holds
b4 . c = d );

theorem :: CAT_1:101
canceled;

theorem Th102: :: CAT_1:102
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
proof end;

theorem Th103: :: CAT_1:103
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 Th104: :: CAT_1:104
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 Th105: :: CAT_1:105
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 20
(Obj T) . c;
correctness
coherence
(Obj T) . c is Object of D;
;
end;

:: deftheorem defines . CAT_1:def 20 :
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:106
canceled;

theorem :: CAT_1:107
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 Th103;

theorem :: CAT_1:108
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 Th104;

theorem :: CAT_1:109
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 Th105;

theorem Th110: :: CAT_1:110
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;

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

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

theorem Th112: :: CAT_1:112
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:113
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 Th112;

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

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

theorem :: CAT_1:114
canceled;

theorem :: CAT_1:115
canceled;

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

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

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

definition
let C, D be Category;
let T be Functor of C,D;
attr T is isomorphic means :: CAT_1:def 22
( T is one-to-one & rng T = the carrier' of D & rng (Obj T) = the carrier of D );
attr T is full means :Def23: :: CAT_1:def 23
 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 :Def24: :: CAT_1:def 24
 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 22 :
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 Def23 defines full CAT_1:def 23 :
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 Def24 defines faithful CAT_1:def 24 :
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:119
canceled;

theorem :: CAT_1:120
canceled;

theorem :: CAT_1:121
canceled;

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

theorem Th123: :: CAT_1:123
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 Th124: :: CAT_1:124
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 Th125: :: CAT_1:125
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 Th126: :: CAT_1:126
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:127
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:128
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 Th129: :: CAT_1:129
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 25
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 25 :
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 :: CAT_1:130
canceled;

theorem Th131: :: CAT_1:131
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:132
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:133
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;