:: Products and Coproducts in Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

scheme :: CAT_3:sch 1
LambdaIdx{ F1() -> set , F2() -> non empty set , F3( set ) -> Element of F2() } :
ex F being Function of F1(),F2() st
for x being set st x in F1() holds
F /. x = F3(x)
proof end;

theorem Th1: :: CAT_3:1
for I being set
for A being non empty set
for F1, F2 being Function of I,A st ( for x being set st x in I holds
F1 /. x = F2 /. x ) holds
F1 = F2
proof end;

scheme :: CAT_3:sch 2
FuncIdxcorrectness{ F1() -> set , F2() -> non empty set , F3( set ) -> Element of F2() } :
( ex F being Function of F1(),F2() st
for x being set st x in F1() holds
F /. x = F3(x) & ( for F1, F2 being Function of F1(),F2() st ( for x being set st x in F1() holds
F1 /. x = F3(x) ) & ( for x being set st x in F1() holds
F2 /. x = F3(x) ) holds
F1 = F2 ) )
proof end;

definition
let A be non empty set ;
let x be set ;
let a be Element of A;
:: original: .-->
redefine func x .--> a -> Function of {x},A;
coherence
x .--> a is Function of {x},A
by FUNCOP_1:46;
end;

theorem Th2: :: CAT_3:2
for I, x being set
for A being non empty set
for a being Element of A st x in I holds
(I --> a) /. x = a
proof end;

theorem Th3: :: CAT_3:3
for x1, x2 being set
for A being non empty set st x1 <> x2 holds
for y1, y2 being Element of A holds
( ((x1,x2) --> (y1,y2)) /. x1 = y1 & ((x1,x2) --> (y1,y2)) /. x2 = y2 )
proof end;

begin

definition
let C be Category;
let I be set ;
let F be Function of I, the carrier' of C;
func doms F -> Function of I, the carrier of C means :Def1: :: CAT_3:def 1
for x being set st x in I holds
it /. x = dom (F /. x);
correctness
existence
ex b1 being Function of I, the carrier of C st
for x being set st x in I holds
b1 /. x = dom (F /. x)
;
uniqueness
for b1, b2 being Function of I, the carrier of C st ( for x being set st x in I holds
b1 /. x = dom (F /. x) ) & ( for x being set st x in I holds
b2 /. x = dom (F /. x) ) holds
b1 = b2
;
proof end;
func cods F -> Function of I, the carrier of C means :Def2: :: CAT_3:def 2
for x being set st x in I holds
it /. x = cod (F /. x);
correctness
existence
ex b1 being Function of I, the carrier of C st
for x being set st x in I holds
b1 /. x = cod (F /. x)
;
uniqueness
for b1, b2 being Function of I, the carrier of C st ( for x being set st x in I holds
b1 /. x = cod (F /. x) ) & ( for x being set st x in I holds
b2 /. x = cod (F /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def1 defines doms CAT_3:def 1 :
for C being Category
for I being set
for F being Function of I, the carrier' of C
for b4 being Function of I, the carrier of C holds
( b4 = doms F iff for x being set st x in I holds
b4 /. x = dom (F /. x) );

:: deftheorem Def2 defines cods CAT_3:def 2 :
for C being Category
for I being set
for F being Function of I, the carrier' of C
for b4 being Function of I, the carrier of C holds
( b4 = cods F iff for x being set st x in I holds
b4 /. x = cod (F /. x) );

theorem Th4: :: CAT_3:4
for I being set
for C being Category
for f being Morphism of C holds doms (I --> f) = I --> (dom f)
proof end;

theorem Th5: :: CAT_3:5
for I being set
for C being Category
for f being Morphism of C holds cods (I --> f) = I --> (cod f)
proof end;

theorem Th6: :: CAT_3:6
for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C holds doms ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((dom p1),(dom p2))
proof end;

theorem Th7: :: CAT_3:7
for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C holds cods ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((cod p1),(cod p2))
proof end;

definition
let C be Category;
let I be set ;
let F be Function of I, the carrier' of C;
func F opp -> Function of I, the carrier' of (C opp) means :Def3: :: CAT_3:def 3
for x being set st x in I holds
it /. x = (F /. x) opp ;
correctness
existence
ex b1 being Function of I, the carrier' of (C opp) st
for x being set st x in I holds
b1 /. x = (F /. x) opp
;
uniqueness
for b1, b2 being Function of I, the carrier' of (C opp) st ( for x being set st x in I holds
b1 /. x = (F /. x) opp ) & ( for x being set st x in I holds
b2 /. x = (F /. x) opp ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def3 defines opp CAT_3:def 3 :
for C being Category
for I being set
for F being Function of I, the carrier' of C
for b4 being Function of I, the carrier' of (C opp) holds
( b4 = F opp iff for x being set st x in I holds
b4 /. x = (F /. x) opp );

theorem :: CAT_3:8
for I being set
for C being Category
for f being Morphism of C holds (I --> f) opp = I --> (f opp)
proof end;

theorem :: CAT_3:9
for x1, x2 being set
for C being Category
for p1, p2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) opp = (x1,x2) --> ((p1 opp),(p2 opp))
proof end;

theorem :: CAT_3:10
for I being set
for C being Category
for F being Function of I, the carrier' of C holds (F opp) opp = F
proof end;

definition
let C be Category;
let I be set ;
let F be Function of I, the carrier' of (C opp);
func opp F -> Function of I, the carrier' of C means :Def4: :: CAT_3:def 4
for x being set st x in I holds
it /. x = opp (F /. x);
correctness
existence
ex b1 being Function of I, the carrier' of C st
for x being set st x in I holds
b1 /. x = opp (F /. x)
;
uniqueness
for b1, b2 being Function of I, the carrier' of C st ( for x being set st x in I holds
b1 /. x = opp (F /. x) ) & ( for x being set st x in I holds
b2 /. x = opp (F /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def4 defines opp CAT_3:def 4 :
for C being Category
for I being set
for F being Function of I, the carrier' of (C opp)
for b4 being Function of I, the carrier' of C holds
( b4 = opp F iff for x being set st x in I holds
b4 /. x = opp (F /. x) );

theorem :: CAT_3:11
for I being set
for C being Category
for f being Morphism of (C opp) holds opp (I --> f) = I --> (opp f)
proof end;

theorem :: CAT_3:12
for x1, x2 being set
for C being Category st x1 <> x2 holds
for p1, p2 being Morphism of (C opp) holds opp ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((opp p1),(opp p2))
proof end;

theorem :: CAT_3:13
for I being set
for C being Category
for F being Function of I, the carrier' of C holds opp (F opp) = F
proof end;

definition
let C be Category;
let I be set ;
let F be Function of I, the carrier' of C;
let f be Morphism of C;
func F * f -> Function of I, the carrier' of C means :Def5: :: CAT_3:def 5
for x being set st x in I holds
it /. x = (F /. x) (*) f;
correctness
existence
ex b1 being Function of I, the carrier' of C st
for x being set st x in I holds
b1 /. x = (F /. x) (*) f
;
uniqueness
for b1, b2 being Function of I, the carrier' of C st ( for x being set st x in I holds
b1 /. x = (F /. x) (*) f ) & ( for x being set st x in I holds
b2 /. x = (F /. x) (*) f ) holds
b1 = b2
;
proof end;
func f * F -> Function of I, the carrier' of C means :Def6: :: CAT_3:def 6
for x being set st x in I holds
it /. x = f (*) (F /. x);
correctness
existence
ex b1 being Function of I, the carrier' of C st
for x being set st x in I holds
b1 /. x = f (*) (F /. x)
;
uniqueness
for b1, b2 being Function of I, the carrier' of C st ( for x being set st x in I holds
b1 /. x = f (*) (F /. x) ) & ( for x being set st x in I holds
b2 /. x = f (*) (F /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def5 defines * CAT_3:def 5 :
for C being Category
for I being set
for F being Function of I, the carrier' of C
for f being Morphism of C
for b5 being Function of I, the carrier' of C holds
( b5 = F * f iff for x being set st x in I holds
b5 /. x = (F /. x) (*) f );

:: deftheorem Def6 defines * CAT_3:def 6 :
for C being Category
for I being set
for F being Function of I, the carrier' of C
for f being Morphism of C
for b5 being Function of I, the carrier' of C holds
( b5 = f * F iff for x being set st x in I holds
b5 /. x = f (*) (F /. x) );

theorem Th14: :: CAT_3:14
for x1, x2 being set
for C being Category
for p1, p2, f being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) * f = (x1,x2) --> ((p1 (*) f),(p2 (*) f))
proof end;

theorem Th15: :: CAT_3:15
for x1, x2 being set
for C being Category
for f, p1, p2 being Morphism of C st x1 <> x2 holds
f * ((x1,x2) --> (p1,p2)) = (x1,x2) --> ((f (*) p1),(f (*) p2))
proof end;

theorem Th16: :: CAT_3:16
for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C st doms F = I --> (cod f) holds
( doms (F * f) = I --> (dom f) & cods (F * f) = cods F )
proof end;

theorem Th17: :: CAT_3:17
for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C st cods F = I --> (dom f) holds
( doms (f * F) = doms F & cods (f * F) = I --> (cod f) )
proof end;

definition
let C be Category;
let I be set ;
let F, G be Function of I, the carrier' of C;
func F "*" G -> Function of I, the carrier' of C means :Def7: :: CAT_3:def 7
for x being set st x in I holds
it /. x = (F /. x) (*) (G /. x);
correctness
existence
ex b1 being Function of I, the carrier' of C st
for x being set st x in I holds
b1 /. x = (F /. x) (*) (G /. x)
;
uniqueness
for b1, b2 being Function of I, the carrier' of C st ( for x being set st x in I holds
b1 /. x = (F /. x) (*) (G /. x) ) & ( for x being set st x in I holds
b2 /. x = (F /. x) (*) (G /. x) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def7 defines "*" CAT_3:def 7 :
for C being Category
for I being set
for F, G, b5 being Function of I, the carrier' of C holds
( b5 = F "*" G iff for x being set st x in I holds
b5 /. x = (F /. x) (*) (G /. x) );

theorem Th18: :: CAT_3:18
for I being set
for C being Category
for F, G being Function of I, the carrier' of C st doms F = cods G holds
( doms (F "*" G) = doms G & cods (F "*" G) = cods F )
proof end;

theorem :: CAT_3:19
for x1, x2 being set
for C being Category
for p1, p2, q1, q2 being Morphism of C st x1 <> x2 holds
((x1,x2) --> (p1,p2)) "*" ((x1,x2) --> (q1,q2)) = (x1,x2) --> ((p1 (*) q1),(p2 (*) q2))
proof end;

theorem :: CAT_3:20
for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C holds F * f = F "*" (I --> f)
proof end;

theorem :: CAT_3:21
for I being set
for C being Category
for f being Morphism of C
for F being Function of I, the carrier' of C holds f * F = (I --> f) "*" F
proof end;

begin

definition
let C be Category;
let a, b be Object of C;
let IT be Morphism of a,b;
attr IT is retraction means :Def8: :: CAT_3:def 8
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st IT * g = id b );
attr IT is coretraction means :Def9: :: CAT_3:def 9
( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st g * IT = id a );
end;

:: deftheorem Def8 defines retraction CAT_3:def 8 :
for C being Category
for a, b being Object of C
for IT being Morphism of a,b holds
( IT is retraction iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st IT * g = id b ) );

:: deftheorem Def9 defines coretraction CAT_3:def 9 :
for C being Category
for a, b being Object of C
for IT being Morphism of a,b holds
( IT is coretraction iff ( Hom (a,b) <> {} & Hom (b,a) <> {} & ex g being Morphism of b,a st g * IT = id a ) );

theorem Th22: :: CAT_3:22
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is retraction holds
f is epi
proof end;

theorem :: CAT_3:23
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is coretraction holds
f is monic
proof end;

theorem :: CAT_3:24
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 retraction & g is retraction holds
g * f is retraction
proof end;

theorem :: CAT_3:25
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 coretraction & g is coretraction holds
g * f is coretraction
proof end;

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

theorem :: CAT_3:27
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 (b,c) <> {} & Hom (c,b) <> {} & g * f is coretraction holds
f is coretraction
proof end;

theorem :: CAT_3:28
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is retraction & f is monic holds
f is invertible
proof end;

theorem Th29: :: CAT_3:29
for C being Category
for a, b being Object of C
for f being Morphism of a,b st f is coretraction & f is epi holds
f is invertible
proof end;

theorem :: CAT_3:30
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is invertible iff ( f is retraction & f is coretraction ) )
proof end;

definition
let C be Category;
let a, b be Object of C;
assume Z: Hom (a,b) <> {} ;
let D be Category;
let T be Functor of C,D;
let f be Morphism of a,b;
func T /. f -> Morphism of T . a,T . b equals :Def10: :: CAT_3:def 10
T . f;
coherence
T . f is Morphism of T . a,T . b
proof end;
end;

:: deftheorem Def10 defines /. CAT_3:def 10 :
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for D being Category
for T being Functor of C,D
for f being Morphism of a,b holds T /. f = T . f;

Lm1: for C, D being Category
for T being Functor of C,D
for a, b, c being Object of C st Hom (a,b) <> {} & Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds T /. (g * f) = (T /. g) * (T /. f)

proof end;

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

proof end;

theorem :: CAT_3:31
for C, D being Category
for a, b being Object of C
for f being Morphism of a,b
for T being Functor of C,D st f is retraction holds
T /. f is retraction
proof end;

theorem :: CAT_3:32
for C, D being Category
for a, b being Object of C
for f being Morphism of a,b
for T being Functor of C,D st f is coretraction holds
T /. f is coretraction
proof end;

theorem :: CAT_3:33
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is retraction iff f opp is coretraction )
proof end;

theorem :: CAT_3:34
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f is coretraction iff f opp is retraction )
proof end;

begin

definition
let C be Category;
let a, b be Object of C;
assume A1: b is terminal ;
func term (a,b) -> Morphism of a,b means :: CAT_3:def 11
verum;
existence
ex b1 being Morphism of a,b st verum
;
uniqueness
for b1, b2 being Morphism of a,b holds b1 = b2
proof end;
end;

:: deftheorem defines term CAT_3:def 11 :
for C being Category
for a, b being Object of C st b is terminal holds
for b4 being Morphism of a,b holds
( b4 = term (a,b) iff verum );

theorem Th35: :: CAT_3:35
for C being Category
for b, a being Object of C st b is terminal holds
( dom (term (a,b)) = a & cod (term (a,b)) = b )
proof end;

theorem Th36: :: CAT_3:36
for C being Category
for b, a being Object of C
for f being Morphism of C st b is terminal & dom f = a & cod f = b holds
term (a,b) = f
proof end;

theorem :: CAT_3:37
for C being Category
for a, b being Object of C
for f being Morphism of a,b st b is terminal holds
term (a,b) = f
proof end;

begin

definition
let C be Category;
let a, b be Object of C;
assume A1: a is initial ;
func init (a,b) -> Morphism of a,b means :: CAT_3:def 12
verum;
existence
ex b1 being Morphism of a,b st verum
;
uniqueness
for b1, b2 being Morphism of a,b holds b1 = b2
proof end;
end;

:: deftheorem defines init CAT_3:def 12 :
for C being Category
for a, b being Object of C st a is initial holds
for b4 being Morphism of a,b holds
( b4 = init (a,b) iff verum );

theorem Th38: :: CAT_3:38
for C being Category
for a, b being Object of C st a is initial holds
( dom (init (a,b)) = a & cod (init (a,b)) = b )
proof end;

theorem Th39: :: CAT_3:39
for C being Category
for a, b being Object of C
for f being Morphism of C st a is initial & dom f = a & cod f = b holds
init (a,b) = f
proof end;

theorem :: CAT_3:40
for C being Category
for a, b being Object of C
for f being Morphism of a,b st a is initial holds
init (a,b) = f
proof end;

begin

definition
let C be Category;
let a be Object of C;
let I be set ;
mode Projections_family of a,I -> Function of I, the carrier' of C means :Def13: :: CAT_3:def 13
doms it = I --> a;
existence
ex b1 being Function of I, the carrier' of C st doms b1 = I --> a
proof end;
end;

:: deftheorem Def13 defines Projections_family CAT_3:def 13 :
for C being Category
for a being Object of C
for I being set
for b4 being Function of I, the carrier' of C holds
( b4 is Projections_family of a,I iff doms b4 = I --> a );

theorem Th41: :: CAT_3:41
for I, x being set
for C being Category
for a being Object of C
for F being Projections_family of a,I st x in I holds
dom (F /. x) = a
proof end;

theorem Th42: :: CAT_3:42
for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds F is Projections_family of a, {}
proof end;

theorem Th43: :: CAT_3:43
for y being set
for C being Category
for a being Object of C
for f being Morphism of C st dom f = a holds
y .--> f is Projections_family of a,{y}
proof end;

theorem Th44: :: CAT_3:44
for x1, x2 being set
for C being Category
for a being Object of C
for p1, p2 being Morphism of C st dom p1 = a & dom p2 = a holds
(x1,x2) --> (p1,p2) is Projections_family of a,{x1,x2}
proof end;

theorem Th45: :: CAT_3:45
for I being set
for C being Category
for a being Object of C
for f being Morphism of C
for F being Projections_family of a,I st cod f = a holds
F * f is Projections_family of dom f,I
proof end;

theorem :: CAT_3:46
for I being set
for C being Category
for a being Object of C
for F being Function of I, the carrier' of C
for G being Projections_family of a,I st doms F = cods G holds
F "*" G is Projections_family of a,I
proof end;

theorem :: CAT_3:47
for I being set
for C being Category
for f being Morphism of C
for F being Projections_family of cod f,I holds (f opp) * (F opp) = (F * f) opp
proof end;

definition
let C be Category;
let a be Object of C;
let I be set ;
let F be Function of I, the carrier' of C;
pred a is_a_product_wrt F means :Def14: :: CAT_3:def 14
( F is Projections_family of a,I & ( for b being Object of C
for F9 being Projections_family of b,I st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) );
end;

:: deftheorem Def14 defines is_a_product_wrt CAT_3:def 14 :
for C being Category
for a being Object of C
for I being set
for F being Function of I, the carrier' of C holds
( a is_a_product_wrt F iff ( F is Projections_family of a,I & ( for b being Object of C
for F9 being Projections_family of b,I st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,a) & ( for k being Morphism of C st k in Hom (b,a) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) ) ) );

theorem Th48: :: CAT_3:48
for I being set
for C being Category
for c, d being Object of C
for F being Projections_family of c,I
for F9 being Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 & cods F = cods F9 holds
c,d are_isomorphic
proof end;

theorem Th49: :: CAT_3:49
for I being set
for C being Category
for c being Object of C
for F being Projections_family of c,I st c is_a_product_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((cod (F /. x1)),(cod (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = cod (F /. x) & Hom (c,d) <> {} holds
for f being Morphism of c,d st f = F /. x holds
f is retraction
proof end;

theorem Th50: :: CAT_3:50
for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds
( a is_a_product_wrt F iff a is terminal )
proof end;

theorem Th51: :: CAT_3:51
for I being set
for C being Category
for a, b being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F holds
for f being Morphism of b,a st dom f = b & cod f = a & f is invertible holds
b is_a_product_wrt F * f
proof end;

theorem :: CAT_3:52
for y being set
for C being Category
for a being Object of C holds a is_a_product_wrt y .--> (id a)
proof end;

theorem :: CAT_3:53
for I being set
for C being Category
for a being Object of C
for F being Projections_family of a,I st a is_a_product_wrt F & ( for x being set st x in I holds
cod (F /. x) is terminal ) holds
a is terminal
proof end;

definition
let C be Category;
let c be Object of C;
let p1, p2 be Morphism of C;
pred c is_a_product_wrt p1,p2 means :Def15: :: CAT_3:def 15
( dom p1 = c & dom p2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds
ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) ) );
end;

:: deftheorem Def15 defines is_a_product_wrt CAT_3:def 15 :
for C being Category
for c being Object of C
for p1, p2 being Morphism of C holds
( c is_a_product_wrt p1,p2 iff ( dom p1 = c & dom p2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom (d,(cod p1)) & g in Hom (d,(cod p2)) holds
ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( p1 (*) k = f & p2 (*) k = g ) iff h = k ) ) ) ) ) );

theorem Th54: :: CAT_3:54
for x1, x2 being set
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st x1 <> x2 holds
( c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2) --> (p1,p2) )
proof end;

theorem :: CAT_3:55
for C being Category
for c, a, b being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds
for p1 being Morphism of c,a
for p2 being Morphism of c,b holds
( c is_a_product_wrt p1,p2 iff for d being Object of C st Hom (d,a) <> {} & Hom (d,b) <> {} holds
( Hom (d,c) <> {} & ( for f being Morphism of d,a
for g being Morphism of d,b ex h being Morphism of d,c st
for k being Morphism of d,c holds
( ( p1 * k = f & p2 * k = g ) iff h = k ) ) ) )
proof end;

theorem :: CAT_3:56
for C being Category
for c, d being Object of C
for p1, p2, q1, q2 being Morphism of C st c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 & cod p1 = cod q1 & cod p2 = cod q2 holds
c,d are_isomorphic
proof end;

theorem :: CAT_3:57
for C being Category
for c, a, b being Object of C
for p1 being Morphism of c,a
for p2 being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} & c is_a_product_wrt p1,p2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( p1 is retraction & p2 is retraction )
proof end;

theorem Th58: :: CAT_3:58
for C being Category
for c being Object of C
for p1, p2, h being Morphism of C st c is_a_product_wrt p1,p2 & h in Hom (c,c) & p1 (*) h = p1 & p2 (*) h = p2 holds
h = id c
proof end;

theorem :: CAT_3:59
for C being Category
for d, c being Object of C
for p1, p2 being Morphism of C
for f being Morphism of d,c st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible holds
d is_a_product_wrt p1 (*) f,p2 (*) f
proof end;

theorem :: CAT_3:60
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p2 is terminal holds
c, cod p1 are_isomorphic
proof end;

theorem :: CAT_3:61
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st c is_a_product_wrt p1,p2 & cod p1 is terminal holds
c, cod p2 are_isomorphic
proof end;

begin

definition
let C be Category;
let c be Object of C;
let I be set ;
mode Injections_family of c,I -> Function of I, the carrier' of C means :Def16: :: CAT_3:def 16
cods it = I --> c;
existence
ex b1 being Function of I, the carrier' of C st cods b1 = I --> c
proof end;
end;

:: deftheorem Def16 defines Injections_family CAT_3:def 16 :
for C being Category
for c being Object of C
for I being set
for b4 being Function of I, the carrier' of C holds
( b4 is Injections_family of c,I iff cods b4 = I --> c );

theorem Th62: :: CAT_3:62
for I, x being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st x in I holds
cod (F /. x) = c
proof end;

theorem :: CAT_3:63
for C being Category
for a being Object of C
for F being Function of {}, the carrier' of C holds F is Injections_family of a, {}
proof end;

theorem Th64: :: CAT_3:64
for y being set
for C being Category
for a being Object of C
for f being Morphism of C st cod f = a holds
y .--> f is Injections_family of a,{y}
proof end;

theorem Th65: :: CAT_3:65
for x1, x2 being set
for C being Category
for c being Object of C
for p1, p2 being Morphism of C st cod p1 = c & cod p2 = c holds
(x1,x2) --> (p1,p2) is Injections_family of c,{x1,x2}
proof end;

theorem Th66: :: CAT_3:66
for I being set
for C being Category
for b being Object of C
for f being Morphism of C
for F being Injections_family of b,I st dom f = b holds
f * F is Injections_family of cod f,I
proof end;

theorem :: CAT_3:67
for I being set
for C being Category
for b being Object of C
for F being Injections_family of b,I
for G being Function of I, the carrier' of C st doms F = cods G holds
F "*" G is Injections_family of b,I
proof end;

theorem Th68: :: CAT_3:68
for I being set
for C being Category
for c being Object of C
for F being Function of I, the carrier' of C holds
( F is Projections_family of c,I iff F opp is Injections_family of c opp ,I )
proof end;

theorem Th69: :: CAT_3:69
for I being set
for C being Category
for F being Function of I, the carrier' of (C opp)
for c being Object of (C opp) holds
( F is Injections_family of c,I iff opp F is Projections_family of opp c,I )
proof end;

theorem :: CAT_3:70
for I being set
for C being Category
for f being Morphism of C
for F being Injections_family of dom f,I holds (F opp) * (f opp) = (f * F) opp
proof end;

definition
let C be Category;
let c be Object of C;
let I be set ;
let F be Function of I, the carrier' of C;
pred c is_a_coproduct_wrt F means :Def17: :: CAT_3:def 17
( F is Injections_family of c,I & ( for d being Object of C
for F9 being Injections_family of d,I st doms F = doms F9 holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( for x being set st x in I holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) ) );
end;

:: deftheorem Def17 defines is_a_coproduct_wrt CAT_3:def 17 :
for C being Category
for c being Object of C
for I being set
for F being Function of I, the carrier' of C holds
( c is_a_coproduct_wrt F iff ( F is Injections_family of c,I & ( for d being Object of C
for F9 being Injections_family of d,I st doms F = doms F9 holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( for x being set st x in I holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) ) ) );

theorem :: CAT_3:71
for I being set
for C being Category
for c being Object of C
for F being Function of I, the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
proof end;

theorem Th72: :: CAT_3:72
for I being set
for C being Category
for c, d being Object of C
for F being Injections_family of c,I
for F9 being Injections_family of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9 holds
c,d are_isomorphic
proof end;

theorem Th73: :: CAT_3:73
for I being set
for C being Category
for c being Object of C
for F being Injections_family of c,I st c is_a_coproduct_wrt F & ( for x1, x2 being set st x1 in I & x2 in I holds
Hom ((dom (F /. x1)),(dom (F /. x2))) <> {} ) holds
for x being set st x in I holds
for d being Object of C st d = dom (F /. x) & Hom (d,c) <> {} holds
for f being Morphism of d,c st f = F /. x holds
f is coretraction
proof end;

theorem Th74: :: CAT_3:74
for I being set
for C being Category
for a, b being Object of C
for f being Morphism of a,b
for F being Injections_family of a,I st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible holds
b is_a_coproduct_wrt f * F
proof end;

theorem Th75: :: CAT_3:75
for C being Category
for a being Object of C
for F being Injections_family of a, {} holds
( a is_a_coproduct_wrt F iff a is initial )
proof end;

theorem :: CAT_3:76
for y being set
for C being Category
for a being Object of C holds a is_a_coproduct_wrt y .--> (id a)
proof end;

theorem :: CAT_3:77
for I being set
for C being Category
for a being Object of C
for F being Injections_family of a,I st a is_a_coproduct_wrt F & ( for x being set st x in I holds
dom (F /. x) is initial ) holds
a is initial
proof end;

definition
let C be Category;
let c be Object of C;
let i1, i2 be Morphism of C;
pred c is_a_coproduct_wrt i1,i2 means :Def18: :: CAT_3:def 18
( cod i1 = c & cod i2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) );
end;

:: deftheorem Def18 defines is_a_coproduct_wrt CAT_3:def 18 :
for C being Category
for c being Object of C
for i1, i2 being Morphism of C holds
( c is_a_coproduct_wrt i1,i2 iff ( cod i1 = c & cod i2 = c & ( for d being Object of C
for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) ) ) );

theorem :: CAT_3:78
for C being Category
for c being Object of C
for p1, p2 being Morphism of C holds
( c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp ,p2 opp )
proof end;

theorem Th79: :: CAT_3:79
for x1, x2 being set
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st x1 <> x2 holds
( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )
proof end;

theorem :: CAT_3:80
for C being Category
for c, d being Object of C
for i1, i2, j1, j2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 & dom i1 = dom j1 & dom i2 = dom j2 holds
c,d are_isomorphic
proof end;

theorem :: CAT_3:81
for C being Category
for a, c, b being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
for i1 being Morphism of a,c
for i2 being Morphism of b,c holds
( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for g being Morphism of b,d ex h being Morphism of c,d st
for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k ) ) ) )
proof end;

theorem :: CAT_3:82
for C being Category
for a, c, b being Object of C
for i1 being Morphism of a,c
for i2 being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} & c is_a_coproduct_wrt i1,i2 & Hom (a,b) <> {} & Hom (b,a) <> {} holds
( i1 is coretraction & i2 is coretraction )
proof end;

theorem Th83: :: CAT_3:83
for C being Category
for c being Object of C
for i1, i2, h being Morphism of C st c is_a_coproduct_wrt i1,i2 & h in Hom (c,c) & h (*) i1 = i1 & h (*) i2 = i2 holds
h = id c
proof end;

theorem :: CAT_3:84
for C being Category
for c, d being Object of C
for i1, i2 being Morphism of C
for f being Morphism of c,d st c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible holds
d is_a_coproduct_wrt f (*) i1,f (*) i2
proof end;

theorem :: CAT_3:85
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i2 is initial holds
dom i1,c are_isomorphic
proof end;

theorem :: CAT_3:86
for C being Category
for c being Object of C
for i1, i2 being Morphism of C st c is_a_coproduct_wrt i1,i2 & dom i1 is initial holds
dom i2,c are_isomorphic
proof end;