:: CAT_4 semantic presentation

definition

let C be Category;
let a, b be Object of C;
canceled;
redefine pred a,b are_isomorphic means :: CAT_4:def 2
( Hom a,b <> {} & Hom b,a <> {} & ex f being Morphism of a,b ex f' being Morphism of b,a st
( f * f' = id b & f' * f = id a ) );
compatibility by CAT_1:81;

end;

:: deftheorem CAT_4:def 1 :

:: deftheorem defines are_isomorphic CAT_4:def 2 :

definition

let C be Category;
attr C is with_finite_product means :: CAT_4:def 3
for I being finite set
for F being Function of I,the Objects of C ex a being Object of C ex F' being Projections_family of a,I st
( cods F' = F & a is_a_product_wrt F' );

end;

:: deftheorem defines with_finite_product CAT_4:def 3 :

notation

let C be Category;
synonym C has_finite_product for with_finite_product C;

end;

theorem Th1: :: CAT_4:1

for C being Category holds
( C has_finite_product iff ( ex a being Object of C st a is terminal & ( for a, b being Object of C ex c being Object of C ex p1, p2 being Morphism of C st
( dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b & c is_a_product_wrt p1,p2 ) ) ) )

proof end;

definition

attr c₁ is strict;
struct ProdCatStr -> CatStr ;
aggr ProdCatStr(# Objects, Morphisms, Dom, Cod, Comp, Id, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ;
sel TerminalObj c₁ -> Element of the Objects of c₁;
sel CatProd c₁ -> Function of [:the Objects of c₁,the Objects of c₁:],the Objects of c₁;
sel Proj1 c₁ -> Function of [:the Objects of c₁,the Objects of c₁:],the Morphisms of c₁;
sel Proj2 c₁ -> Function of [:the Objects of c₁,the Objects of c₁:],the Morphisms of c₁;

end;

definition

let C be ProdCatStr ;
func [1] C -> Object of C equals :: CAT_4:def 4
the TerminalObj of C;
correctness ;
let a, b be Object of C;
func a [x] b -> Object of C equals :: CAT_4:def 5
the CatProd of C . [a,b];
correctness ;
func pr1 a,b -> Morphism of C equals :: CAT_4:def 6
the Proj1 of C . [a,b];
correctness ;
func pr2 a,b -> Morphism of C equals :: CAT_4:def 7
the Proj2 of C . [a,b];
correctness ;

end;

:: deftheorem defines [1] CAT_4:def 4 :

:: deftheorem defines [x] CAT_4:def 5 :

:: deftheorem defines pr1 CAT_4:def 6 :

:: deftheorem defines pr2 CAT_4:def 7 :

definition

let o, m be set ;
func c1Cat o,m -> strict ProdCatStr equals :: CAT_4:def 8
ProdCatStr(# {o},{m},({m} --> o),({m} --> o),(m,m .--> m),({o} --> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #);
correctness ;

end;

:: deftheorem defines c1Cat CAT_4:def 8 :

theorem :: CAT_4:2

for o, m being set holds CatStr(# the Objects of (c1Cat o,m),the Morphisms of (c1Cat o,m),the Dom of (c1Cat o,m),the Cod of (c1Cat o,m),the Comp of (c1Cat o,m),the Id of (c1Cat o,m) #) = 1Cat o,m ;

Lm1: for o, m being set holds c1Cat o,m is Category-like

proof end;

registration

cluster Category-like strict ProdCatStr ;
existence

proof end;

end;

registration

let o, m be set ;
cluster c1Cat o,m -> Category-like strict ;
coherence by Lm1;

end;

theorem Th3: :: CAT_4:3

for o, m being set
for a being Object of (c1Cat o,m) holds a = o by TARSKI:def 1;

theorem Th4: :: CAT_4:4

for o, m being set
for a, b being Object of (c1Cat o,m) holds a = b

proof end;

theorem Th5: :: CAT_4:5

for o, m being set
for f being Morphism of (c1Cat o,m) holds f = m by TARSKI:def 1;

theorem Th6: :: CAT_4:6

for o, m being set
for f, g being Morphism of (c1Cat o,m) holds f = g

proof end;

theorem Th7: :: CAT_4:7

for o, m being set
for a, b being Object of (c1Cat o,m)
for f being Morphism of (c1Cat o,m) holds f in Hom a,b

proof end;

theorem :: CAT_4:8

for o, m being set
for a, b being Object of (c1Cat o,m)
for f being Morphism of (c1Cat o,m) holds f is Morphism of a,b

proof end;

theorem :: CAT_4:9

for o, m being set
for a, b being Object of (c1Cat o,m) holds Hom a,b <> {} by Th7;

theorem Th10: :: CAT_4:10

for o, m being set
for a being Object of (c1Cat o,m) holds a is terminal

proof end;

theorem Th11: :: CAT_4:11

for o, m being set
for c being Object of (c1Cat o,m)
for p1, p2 being Morphism of (c1Cat o,m) holds c is_a_product_wrt p1,p2

proof end;

definition

let IT be Category-like ProdCatStr ;
attr IT is Cartesian means :Def9: :: CAT_4:def 9
( the TerminalObj of IT is terminal & ( for a, b being Object of IT holds
( cod (the Proj1 of IT . [a,b]) = a & cod (the Proj2 of IT . [a,b]) = b & the CatProd of IT . [a,b] is_a_product_wrt the Proj1 of IT . [a,b],the Proj2 of IT . [a,b] ) ) );

end;

:: deftheorem Def9 defines Cartesian CAT_4:def 9 :

theorem Th12: :: CAT_4:12

for o, m being set holds c1Cat o,m is Cartesian

proof end;

registration

cluster Category-like strict Cartesian ProdCatStr ;
existence

proof end;

end;

definition

mode Cartesian_category is Category-like Cartesian ProdCatStr ;

end;

theorem Th13: :: CAT_4:13

for C being Cartesian_category holds [1] C is terminal by Def9;

theorem Th14: :: CAT_4:14

for C being Cartesian_category
for a being Object of C
for f1, f2 being Morphism of a, [1] C holds f1 = f2

proof end;

theorem Th15: :: CAT_4:15

for C being Cartesian_category
for a being Object of C holds Hom a,([1] C) <> {}

proof end;

definition

let C be Cartesian_category;
let a be Object of C;
func term a -> Morphism of a, [1] C means :: CAT_4:def 10
verum;
existence ;
uniqueness by Th14;

end;

:: deftheorem defines term CAT_4:def 10 :

theorem Th16: :: CAT_4:16

for C being Cartesian_category
for a being Object of C holds term a = term a,([1] C)

proof end;

theorem :: CAT_4:17

for C being Cartesian_category
for a being Object of C holds
( dom (term a) = a & cod (term a) = [1] C )

proof end;

theorem :: CAT_4:18

for C being Cartesian_category
for a being Object of C holds Hom a,([1] C) = {(term a)}

proof end;

theorem Th19: :: CAT_4:19

for C being Cartesian_category
for a, b being Object of C holds
( dom (pr1 a,b) = a [x] b & cod (pr1 a,b) = a )

proof end;

theorem Th20: :: CAT_4:20

for C being Cartesian_category
for a, b being Object of C holds
( dom (pr2 a,b) = a [x] b & cod (pr2 a,b) = b )

proof end;

definition

let C be Cartesian_category;
let a, b be Object of C;
:: original: pr1
redefine func pr1 a,b -> Morphism of a [x] b,a;
coherence

proof end;

:: original: pr2
redefine func pr2 a,b -> Morphism of a [x] b,b;
coherence

proof end;

end;

theorem Th21: :: CAT_4:21

for C being Cartesian_category
for a, b being Object of C holds
( Hom (a [x] b),a <> {} & Hom (a [x] b),b <> {} )

proof end;

theorem Th22: :: CAT_4:22

for C being Cartesian_category
for a, b being Object of C holds a [x] b is_a_product_wrt pr1 a,b, pr2 a,b by Def9;

theorem :: CAT_4:23

for C being Cartesian_category holds C has_finite_product

proof end;

theorem :: CAT_4:24

for C being Cartesian_category
for a, b being Object of C st Hom a,b <> {} & Hom b,a <> {} holds
( pr1 a,b is retraction & pr2 a,b is retraction )

proof end;

definition

let C be Cartesian_category;
let a, b, c be Object of C;
let f be Morphism of c,a;
let g be Morphism of c,b;
assume A1: ( Hom c,a <> {} & Hom c,b <> {} ) ;
func <:f,g:> -> Morphism of c,a [x] b means :Def11: :: CAT_4:def 11
( (pr1 a,b) * it = f & (pr2 a,b) * it = g );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines <: CAT_4:def 11 :

theorem Th25: :: CAT_4:25

for C being Cartesian_category
for c, a, b being Object of C st Hom c,a <> {} & Hom c,b <> {} holds
Hom c,(a [x] b) <> {}

proof end;

theorem Th26: :: CAT_4:26

for C being Cartesian_category
for a, b being Object of C holds <:(pr1 a,b),(pr2 a,b):> = id (a [x] b)

proof end;

theorem Th27: :: CAT_4:27

for C being Cartesian_category
for c, a, b, d being Object of C
for f being Morphism of c,a
for g being Morphism of c,b
for h being Morphism of d,c st Hom c,a <> {} & Hom c,b <> {} & Hom d,c <> {} holds
<:(f * h),(g * h):> = <:f,g:> * h

proof end;

theorem Th28: :: CAT_4:28

for C being Cartesian_category
for c, a, b being Object of C
for f, k being Morphism of c,a
for g, h being Morphism of c,b st Hom c,a <> {} & Hom c,b <> {} & <:f,g:> = <:k,h:> holds
( f = k & g = h )

proof end;

theorem :: CAT_4:29

for C being Cartesian_category
for c, a, b being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom c,a <> {} & Hom c,b <> {} & ( f is monic or g is monic ) holds
<:f,g:> is monic

proof end;

theorem Th30: :: CAT_4:30

for C being Cartesian_category
for a being Object of C holds
( Hom a,(a [x] ([1] C)) <> {} & Hom a,(([1] C) [x] a) <> {} )

proof end;

definition

let C be Cartesian_category;
let a be Object of C;
func lambda a -> Morphism of ([1] C) [x] a,a equals :: CAT_4:def 12
pr2 ([1] C),a;
correctness ;
func lambda' a -> Morphism of a,([1] C) [x] a equals :: CAT_4:def 13
<:(term a),(id a):>;
correctness ;
func rho a -> Morphism of a [x] ([1] C),a equals :: CAT_4:def 14
pr1 a,([1] C);
correctness ;
func rho' a -> Morphism of a,a [x] ([1] C) equals :: CAT_4:def 15
<:(id a),(term a):>;
correctness ;

end;

:: deftheorem defines lambda CAT_4:def 12 :

:: deftheorem defines lambda' CAT_4:def 13 :

:: deftheorem defines rho CAT_4:def 14 :

:: deftheorem defines rho' CAT_4:def 15 :

theorem Th31: :: CAT_4:31

for C being Cartesian_category
for a being Object of C holds
( (lambda a) * (lambda' a) = id a & (lambda' a) * (lambda a) = id (([1] C) [x] a) & (rho a) * (rho' a) = id a & (rho' a) * (rho a) = id (a [x] ([1] C)) )

proof end;

theorem :: CAT_4:32

for C being Cartesian_category
for a being Object of C holds
( a,a [x] ([1] C) are_isomorphic & a,([1] C) [x] a are_isomorphic )

proof end;

definition

let C be Cartesian_category;
let a, b be Object of C;
func Switch a,b -> Morphism of a [x] b,b [x] a equals :: CAT_4:def 16
<:(pr2 a,b),(pr1 a,b):>;
correctness ;

end;

:: deftheorem defines Switch CAT_4:def 16 :

theorem Th33: :: CAT_4:33

for C being Cartesian_category
for a, b being Object of C holds Hom (a [x] b),(b [x] a) <> {}

proof end;

theorem Th34: :: CAT_4:34

for C being Cartesian_category
for a, b being Object of C holds (Switch a,b) * (Switch b,a) = id (b [x] a)

proof end;

theorem :: CAT_4:35

for C being Cartesian_category
for a, b being Object of C holds a [x] b,b [x] a are_isomorphic

proof end;

definition

let C be Cartesian_category;
let a be Object of C;
func Delta a -> Morphism of a,a [x] a equals :: CAT_4:def 17
<:(id a),(id a):>;
correctness ;

end;

:: deftheorem defines Delta CAT_4:def 17 :

theorem :: CAT_4:36

for C being Cartesian_category
for a being Object of C holds Hom a,(a [x] a) <> {}

proof end;

theorem :: CAT_4:37

for C being Cartesian_category
for a, b being Object of C
for f being Morphism of a,b st Hom a,b <> {} holds
<:f,f:> = (Delta b) * f

proof end;

definition

let C be Cartesian_category;
let a, b, c be Object of C;
func Alpha a,b,c -> Morphism of (a [x] b) [x] c,a [x] (b [x] c) equals :: CAT_4:def 18
<:((pr1 a,b) * (pr1 (a [x] b),c)),<:((pr2 a,b) * (pr1 (a [x] b),c)),(pr2 (a [x] b),c):>:>;
correctness ;
func Alpha' a,b,c -> Morphism of a [x] (b [x] c),(a [x] b) [x] c equals :: CAT_4:def 19
<:<:(pr1 a,(b [x] c)),((pr1 b,c) * (pr2 a,(b [x] c))):>,((pr2 b,c) * (pr2 a,(b [x] c))):>;
correctness ;

end;

:: deftheorem defines Alpha CAT_4:def 18 :

:: deftheorem defines Alpha' CAT_4:def 19 :

theorem Th38: :: CAT_4:38

for C being Cartesian_category
for a, b, c being Object of C holds
( Hom ((a [x] b) [x] c),(a [x] (b [x] c)) <> {} & Hom (a [x] (b [x] c)),((a [x] b) [x] c) <> {} )

proof end;

theorem Th39: :: CAT_4:39

for C being Cartesian_category
for a, b, c being Object of C holds
( (Alpha a,b,c) * (Alpha' a,b,c) = id (a [x] (b [x] c)) & (Alpha' a,b,c) * (Alpha a,b,c) = id ((a [x] b) [x] c) )

proof end;

theorem :: CAT_4:40

for C being Cartesian_category
for a, b, c being Object of C holds (a [x] b) [x] c,a [x] (b [x] c) are_isomorphic

proof end;

definition

let C be Cartesian_category;
let a, b, c, d be Object of C;
let f be Morphism of a,b;
let g be Morphism of c,d;
func f [x] g -> Morphism of a [x] c,b [x] d equals :: CAT_4:def 20
<:(f * (pr1 a,c)),(g * (pr2 a,c)):>;
correctness ;

end;

:: deftheorem defines [x] CAT_4:def 20 :

theorem :: CAT_4:41

for C being Cartesian_category
for a, c, b, d being Object of C st Hom a,c <> {} & Hom b,d <> {} holds
Hom (a [x] b),(c [x] d) <> {}

proof end;

theorem :: CAT_4:42

for C being Cartesian_category
for a, b being Object of C holds (id a) [x] (id b) = id (a [x] b)

proof end;

theorem Th43: :: CAT_4:43

for C being Cartesian_category
for a, b, c, d, e being Object of C
for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for k being Morphism of e,c st Hom a,b <> {} & Hom c,d <> {} & Hom e,a <> {} & Hom e,c <> {} holds
(f [x] h) * <:g,k:> = <:(f * g),(h * k):>

proof end;

theorem :: CAT_4:44

for C being Cartesian_category
for c, a, b being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom c,a <> {} & Hom c,b <> {} holds
<:f,g:> = (f [x] g) * (Delta c)

proof end;

theorem :: CAT_4:45

for C being Cartesian_category
for a, b, c, d, e, s being Object of C
for f being Morphism of a,b
for h being Morphism of c,d
for g being Morphism of e,a
for k being Morphism of s,c st Hom a,b <> {} & Hom c,d <> {} & Hom e,a <> {} & Hom s,c <> {} holds
(f [x] h) * (g [x] k) = (f * g) [x] (h * k)

proof end;

definition

let C be Category;
attr C is with_finite_coproduct means :: CAT_4:def 21
for I being finite set
for F being Function of I,the Objects of C ex a being Object of C ex F' being Injections_family of a,I st
( doms F' = F & a is_a_coproduct_wrt F' );

end;

:: deftheorem defines with_finite_coproduct CAT_4:def 21 :

notation

let C be Category;
synonym C has_finite_coproduct for with_finite_coproduct C;

end;

theorem Th46: :: CAT_4:46

for C being Category holds
( C has_finite_coproduct iff ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) )

proof end;

definition

attr c₁ is strict;
struct CoprodCatStr -> CatStr ;
aggr CoprodCatStr(# Objects, Morphisms, Dom, Cod, Comp, Id, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ;
sel Initial c₁ -> Element of the Objects of c₁;
sel Coproduct c₁ -> Function of [:the Objects of c₁,the Objects of c₁:],the Objects of c₁;
sel Incl1 c₁ -> Function of [:the Objects of c₁,the Objects of c₁:],the Morphisms of c₁;
sel Incl2 c₁ -> Function of [:the Objects of c₁,the Objects of c₁:],the Morphisms of c₁;

end;

definition

let C be CoprodCatStr ;
func [0] C -> Object of C equals :: CAT_4:def 22
the Initial of C;
correctness ;
let a, b be Object of C;
func a + b -> Object of C equals :: CAT_4:def 23
the Coproduct of C . [a,b];
correctness ;
func in1 a,b -> Morphism of C equals :: CAT_4:def 24
the Incl1 of C . [a,b];
correctness ;
func in2 a,b -> Morphism of C equals :: CAT_4:def 25
the Incl2 of C . [a,b];
correctness ;

end;

:: deftheorem defines [0] CAT_4:def 22 :

:: deftheorem defines + CAT_4:def 23 :

:: deftheorem defines in1 CAT_4:def 24 :

:: deftheorem defines in2 CAT_4:def 25 :

definition

let o, m be set ;
func c1Cat* o,m -> strict CoprodCatStr equals :: CAT_4:def 26
CoprodCatStr(# {o},{m},({m} --> o),({m} --> o),(m,m .--> m),({o} --> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #);
correctness ;

end;

:: deftheorem defines c1Cat* CAT_4:def 26 :

theorem :: CAT_4:47

for o, m being set holds CatStr(# the Objects of (c1Cat* o,m),the Morphisms of (c1Cat* o,m),the Dom of (c1Cat* o,m),the Cod of (c1Cat* o,m),the Comp of (c1Cat* o,m),the Id of (c1Cat* o,m) #) = 1Cat o,m ;

Lm2: for o, m being set holds c1Cat* o,m is Category-like

proof end;

registration

cluster Category-like strict CoprodCatStr ;
existence

proof end;

end;

registration

let o, m be set ;
cluster c1Cat* o,m -> Category-like strict ;
coherence by Lm2;

end;

theorem Th48: :: CAT_4:48

for o, m being set
for a being Object of (c1Cat* o,m) holds a = o by TARSKI:def 1;

theorem Th49: :: CAT_4:49

for o, m being set
for a, b being Object of (c1Cat* o,m) holds a = b

proof end;

theorem Th50: :: CAT_4:50

for o, m being set
for f being Morphism of (c1Cat* o,m) holds f = m by TARSKI:def 1;

theorem Th51: :: CAT_4:51

for o, m being set
for f, g being Morphism of (c1Cat* o,m) holds f = g

proof end;

theorem Th52: :: CAT_4:52

for o, m being set
for a, b being Object of (c1Cat* o,m)
for f being Morphism of (c1Cat* o,m) holds f in Hom a,b

proof end;

theorem :: CAT_4:53

for o, m being set
for a, b being Object of (c1Cat* o,m)
for f being Morphism of (c1Cat* o,m) holds f is Morphism of a,b

proof end;

theorem :: CAT_4:54

for o, m being set
for a, b being Object of (c1Cat* o,m) holds Hom a,b <> {} by Th52;

theorem Th55: :: CAT_4:55

for o, m being set
for a being Object of (c1Cat* o,m) holds a is initial

proof end;

theorem Th56: :: CAT_4:56

for o, m being set
for c being Object of (c1Cat* o,m)
for i1, i2 being Morphism of (c1Cat* o,m) holds c is_a_coproduct_wrt i1,i2

proof end;

definition

let IT be Category-like CoprodCatStr ;
attr IT is Cocartesian means :Def27: :: CAT_4:def 27
( the Initial of IT is initial & ( for a, b being Object of IT holds
( dom (the Incl1 of IT . [a,b]) = a & dom (the Incl2 of IT . [a,b]) = b & the Coproduct of IT . [a,b] is_a_coproduct_wrt the Incl1 of IT . [a,b],the Incl2 of IT . [a,b] ) ) );

end;

:: deftheorem Def27 defines Cocartesian CAT_4:def 27 :

theorem Th57: :: CAT_4:57

for o, m being set holds c1Cat* o,m is Cocartesian

proof end;

registration

cluster Category-like strict Cocartesian CoprodCatStr ;
existence

proof end;

end;

definition

mode Cocartesian_category is Category-like Cocartesian CoprodCatStr ;

end;

theorem Th58: :: CAT_4:58

for C being Cocartesian_category holds [0] C is initial by Def27;

theorem Th59: :: CAT_4:59

for C being Cocartesian_category
for a being Object of C
for f1, f2 being Morphism of [0] C,a holds f1 = f2

proof end;

definition

let C be Cocartesian_category;
let a be Object of C;
func init a -> Morphism of [0] C,a means :: CAT_4:def 28
verum;
existence ;
uniqueness by Th59;

end;

:: deftheorem defines init CAT_4:def 28 :

theorem Th60: :: CAT_4:60

for C being Cocartesian_category
for a being Object of C holds Hom ([0] C),a <> {}

proof end;

theorem Th61: :: CAT_4:61

for C being Cocartesian_category
for a being Object of C holds init a = init ([0] C),a

proof end;

theorem :: CAT_4:62

for C being Cocartesian_category
for a being Object of C holds
( dom (init a) = [0] C & cod (init a) = a )

proof end;

theorem :: CAT_4:63

for C being Cocartesian_category
for a being Object of C holds Hom ([0] C),a = {(init a)}

proof end;

theorem Th64: :: CAT_4:64

for C being Cocartesian_category
for a, b being Object of C holds
( dom (in1 a,b) = a & cod (in1 a,b) = a + b )

proof end;

theorem Th65: :: CAT_4:65

for C being Cocartesian_category
for a, b being Object of C holds
( dom (in2 a,b) = b & cod (in2 a,b) = a + b )

proof end;

theorem Th66: :: CAT_4:66

for C being Cocartesian_category
for a, b being Object of C holds
( Hom a,(a + b) <> {} & Hom b,(a + b) <> {} )

proof end;

theorem Th67: :: CAT_4:67

for C being Cocartesian_category
for a, b being Object of C holds a + b is_a_coproduct_wrt in1 a,b, in2 a,b by Def27;

theorem :: CAT_4:68

for C being Cocartesian_category holds C has_finite_coproduct

proof end;

theorem :: CAT_4:69

for C being Cocartesian_category
for a, b being Object of C st Hom a,b <> {} & Hom b,a <> {} holds
( in1 a,b is coretraction & in2 a,b is coretraction )

proof end;

definition

let C be Cocartesian_category;
let a, b be Object of C;
:: original: in1
redefine func in1 a,b -> Morphism of a,a + b;
coherence

proof end;

:: original: in2
redefine func in2 a,b -> Morphism of b,a + b;
coherence

proof end;

end;

definition

let C be Cocartesian_category;
let a, b, c be Object of C;
let f be Morphism of a,c;
let g be Morphism of b,c;
assume A1: ( Hom a,c <> {} & Hom b,c <> {} ) ;
func [$f,g$] -> Morphism of a + b,c means :Def29: :: CAT_4:def 29
( it * (in1 a,b) = f & it * (in2 a,b) = g );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def29 defines [$ CAT_4:def 29 :

theorem Th70: :: CAT_4:70

for C being Cocartesian_category
for a, c, b being Object of C st Hom a,c <> {} & Hom b,c <> {} holds
Hom (a + b),c <> {}

proof end;

theorem Th71: :: CAT_4:71

for C being Cocartesian_category
for a, b being Object of C holds [$(in1 a,b),(in2 a,b)$] = id (a + b)

proof end;

theorem Th72: :: CAT_4:72

for C being Cocartesian_category
for a, c, b, d being Object of C
for f being Morphism of a,c
for g being Morphism of b,c
for h being Morphism of c,d st Hom a,c <> {} & Hom b,c <> {} & Hom c,d <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]

proof end;

theorem Th73: :: CAT_4:73

for C being Cocartesian_category
for a, c, b being Object of C
for f, k being Morphism of a,c
for g, h being Morphism of b,c st Hom a,c <> {} & Hom b,c <> {} & [$f,g$] = [$k,h$] holds
( f = k & g = h )

proof end;

theorem :: CAT_4:74

for C being Cocartesian_category
for a, c, b being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom a,c <> {} & Hom b,c <> {} & ( f is epi or g is epi ) holds
[$f,g$] is epi

proof end;

theorem :: CAT_4:75

for C being Cocartesian_category
for a being Object of C holds
( a,a + ([0] C) are_isomorphic & a,([0] C) + a are_isomorphic )

proof end;

theorem :: CAT_4:76

for C being Cocartesian_category
for a, b being Object of C holds a + b,b + a are_isomorphic

proof end;

theorem :: CAT_4:77

for C being Cocartesian_category
for a, b, c being Object of C holds (a + b) + c,a + (b + c) are_isomorphic

proof end;

definition

let C be Cocartesian_category;
let a be Object of C;
func nabla a -> Morphism of a + a,a equals :: CAT_4:def 30
[$(id a),(id a)$];
correctness ;

end;

:: deftheorem defines nabla CAT_4:def 30 :

definition

let C be Cocartesian_category;
let a, b, c, d be Object of C;
let f be Morphism of a,c;
let g be Morphism of b,d;
func f + g -> Morphism of a + b,c + d equals :: CAT_4:def 31
[$((in1 c,d) * f),((in2 c,d) * g)$];
correctness ;

end;

:: deftheorem defines + CAT_4:def 31 :

theorem :: CAT_4:78

for C being Cocartesian_category
for a, c, b, d being Object of C st Hom a,c <> {} & Hom b,d <> {} holds
Hom (a + b),(c + d) <> {}

proof end;

theorem :: CAT_4:79

for C being Cocartesian_category
for a, b being Object of C holds (id a) + (id b) = id (a + b)

proof end;

theorem Th80: :: CAT_4:80

for C being Cocartesian_category
for a, c, b, d, e being Object of C
for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for k being Morphism of d,e st Hom a,c <> {} & Hom b,d <> {} & Hom c,e <> {} & Hom d,e <> {} holds
[$g,k$] * (f + h) = [$(g * f),(k * h)$]

proof end;

theorem :: CAT_4:81

for C being Cocartesian_category
for a, c, b being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom a,c <> {} & Hom b,c <> {} holds
(nabla c) * (f + g) = [$f,g$]

proof end;

theorem :: CAT_4:82

for C being Cocartesian_category
for a, c, b, d, e, s being Object of C
for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for k being Morphism of d,s st Hom a,c <> {} & Hom b,d <> {} & Hom c,e <> {} & Hom d,s <> {} holds
(g + k) * (f + h) = (g * f) + (k * h)

proof end;