:: Cartesian Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received October 27, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users


definition
let C be Category;
let a, b be Object of C;
redefine pred a,b are_isomorphic means :: CAT_4:def 1
( 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 ) );
compatibility
( 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 ) ) ) by CAT_1:48;
end;

:: deftheorem defines are_isomorphic CAT_4:def 1 :
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 ) ) );

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

:: deftheorem defines with_finite_product CAT_4:def 2 :
for C being Category holds
( C is with_finite_product iff for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Projections_family of a,I st
( cods F9 = F & a is_a_product_wrt F9 ) );

theorem Th1: :: CAT_4:1
for C being Category holds
( C is with_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 c1 is strict ;
struct ProdCatStr -> CatStr ;
aggr ProdCatStr(# carrier, carrier', Source, Target, Comp, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ;
sel TerminalObj c1 -> Element of the carrier of c1;
sel CatProd c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier of c1;
sel Proj1 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
sel Proj2 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
end;

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

definition
let C be non empty non void ProdCatStr ;
func [1] C -> Object of C equals :: CAT_4:def 3
 the TerminalObj of C;
correctness
coherence
the TerminalObj of C is Object of C;
;
let a, b be Object of C;
func a [x] b -> Object of C equals :: CAT_4:def 4
 the CatProd of C . (a,b);
correctness
coherence
the CatProd of C . (a,b) is Object of C;
;
func pr1 (a,b) -> Morphism of C equals :: CAT_4:def 5
 the Proj1 of C . (a,b);
correctness
coherence
the Proj1 of C . (a,b) is Morphism of C;
;
func pr2 (a,b) -> Morphism of C equals :: CAT_4:def 6
 the Proj2 of C . (a,b);
correctness
coherence
the Proj2 of C . (a,b) is Morphism of C;
;
end;

:: deftheorem defines [1] CAT_4:def 3 :
for C being non empty non void ProdCatStr holds [1] C = the TerminalObj of C;

:: deftheorem defines [x] CAT_4:def 4 :
for C being non empty non void ProdCatStr
for a, b being Object of C holds a [x] b = the CatProd of C . (a,b);

:: deftheorem defines pr1 CAT_4:def 5 :
for C being non empty non void ProdCatStr
for a, b being Object of C holds pr1 (a,b) = the Proj1 of C . (a,b);

:: deftheorem defines pr2 CAT_4:def 6 :
for C being non empty non void ProdCatStr
for a, b being Object of C holds pr2 (a,b) = the Proj2 of C . (a,b);

definition
let o, m be set ;
func c1Cat (o,m) -> strict ProdCatStr equals :: CAT_4:def 7
 ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
correctness
coherence
ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict ProdCatStr ;
;
end;

:: deftheorem defines c1Cat CAT_4:def 7 :
for o, m being set holds c1Cat (o,m) = ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);

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

theorem :: CAT_4:2
for o, m being set holds CatStr(# the carrier of (c1Cat (o,m)), the carrier' of (c1Cat (o,m)), the Source of (c1Cat (o,m)), the Target of (c1Cat (o,m)), the Comp of (c1Cat (o,m)) #) = 1Cat (o,m) ;

Lm1: for o, m being set holds c1Cat (o,m) is Category-like
proof end;

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

registration
let o, m be set ;
cluster c1Cat (o,m) -> non empty non void Category-like transitive associative reflexive with_identities strict ;
coherence
( c1Cat (o,m) is Category-like & c1Cat (o,m) is reflexive & c1Cat (o,m) is transitive & c1Cat (o,m) is associative & c1Cat (o,m) is with_identities & not c1Cat (o,m) is empty & not c1Cat (o,m) is void ) by Lm1;
end;

theorem Th3: :: CAT_4:3
for o, m being set
for a, b being Object of (c1Cat (o,m)) holds a = b
proof end;

theorem Th4: :: CAT_4:4
for o, m being set
for f, g being Morphism of (c1Cat (o,m)) holds f = g
proof end;

theorem Th5: :: CAT_4:5
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:6
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:7
for o, m being set
for a, b being Object of (c1Cat (o,m)) holds Hom (a,b) <> {} by Th5;

theorem Th8: :: CAT_4:8
for o, m being set
for a being Object of (c1Cat (o,m)) holds a is terminal
proof end;

theorem Th9: :: CAT_4:9
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 non empty non void Category-like transitive associative reflexive with_identities ProdCatStr ;
attr IT is Cartesian means :Def8: :: CAT_4:def 8
( 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 Def8 defines Cartesian CAT_4:def 8 :
for IT being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr holds
( IT is Cartesian iff ( 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) ) ) ) );

theorem Th10: :: CAT_4:10
for o, m being set holds c1Cat (o,m) is Cartesian by Th8, Th3, Th9;

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

definition
mode Cartesian_category is non empty non void Category-like transitive associative reflexive with_identities Cartesian ProdCatStr ;
end;

theorem :: CAT_4:11
for C being Cartesian_category holds [1] C is terminal by Def8;

theorem Th12: :: CAT_4:12
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 Th13: :: CAT_4:13
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 9
verum;
existence
ex b1 being Morphism of a, [1] C st verum ;
uniqueness
for b1, b2 being Morphism of a, [1] C holds b1 = b2 by Th12;
end;

:: deftheorem defines term CAT_4:def 9 :
for C being Cartesian_category
for a being Object of C
for b3 being Morphism of a, [1] C holds
( b3 = term a iff verum );

theorem Th14: :: CAT_4:14
for C being Cartesian_category
for a being Object of C holds term a = term (a,([1] C))
proof end;

theorem :: CAT_4:15
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:16
for C being Cartesian_category
for a being Object of C holds Hom (a,([1] C)) = {(term a)}
proof end;

theorem Th17: :: CAT_4:17
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 Th18: :: CAT_4:18
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
pr1 (a,b) is Morphism of a [x] b,a
proof end;
:: original: pr2
redefine func pr2 (a,b) -> Morphism of a [x] b,b;
coherence
pr2 (a,b) is Morphism of a [x] b,b
proof end;
end;

theorem Th19: :: CAT_4:19
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 :: CAT_4:20
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 Def8;

theorem :: CAT_4:21
for C being Cartesian_category holds C is with_finite_product
proof end;

theorem :: CAT_4:22
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 :Def10: :: CAT_4:def 10
( (pr1 (a,b)) * it = f & (pr2 (a,b)) * it = g );
existence
ex b1 being Morphism of c,a [x] b st
( (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g )
proof end;
uniqueness
for b1, b2 being Morphism of c,a [x] b st (pr1 (a,b)) * b1 = f & (pr2 (a,b)) * b1 = g & (pr1 (a,b)) * b2 = f & (pr2 (a,b)) * b2 = g holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines <: CAT_4:def 10 :
for C being Cartesian_category
for a, b, c 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
for b7 being Morphism of c,a [x] b holds
( b7 = <:f,g:> iff ( (pr1 (a,b)) * b7 = f & (pr2 (a,b)) * b7 = g ) );

theorem Th23: :: CAT_4:23
for C being Cartesian_category
for a, b, c being Object of C st Hom (c,a) <> {} & Hom (c,b) <> {} holds
Hom (c,(a [x] b)) <> {}
proof end;

theorem Th24: :: CAT_4:24
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 Th25: :: CAT_4:25
for C being Cartesian_category
for a, b, c, 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 Th26: :: CAT_4:26
for C being Cartesian_category
for a, b, c 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:27
for C being Cartesian_category
for a, b, c 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 Th28: :: CAT_4:28
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 11
 pr2 (([1] C),a);
correctness
coherence
pr2 (([1] C),a) is Morphism of ([1] C) [x] a,a;
;
func lambda' a -> Morphism of a,([1] C) [x] a equals :: CAT_4:def 12
<:(term a),(id a):>;
correctness
coherence
<:(term a),(id a):> is Morphism of a,([1] C) [x] a;
;
func rho a -> Morphism of a [x] ([1] C),a equals :: CAT_4:def 13
 pr1 (a,([1] C));
correctness
coherence
pr1 (a,([1] C)) is Morphism of a [x] ([1] C),a;
;
func rho' a -> Morphism of a,a [x] ([1] C) equals :: CAT_4:def 14
<:(id a),(term a):>;
correctness
coherence
<:(id a),(term a):> is Morphism of a,a [x] ([1] C);
;
end;

:: deftheorem defines lambda CAT_4:def 11 :
for C being Cartesian_category
for a being Object of C holds lambda a = pr2 (([1] C),a);

:: deftheorem defines lambda' CAT_4:def 12 :
for C being Cartesian_category
for a being Object of C holds lambda' a = <:(term a),(id a):>;

:: deftheorem defines rho CAT_4:def 13 :
for C being Cartesian_category
for a being Object of C holds rho a = pr1 (a,([1] C));

:: deftheorem defines rho' CAT_4:def 14 :
for C being Cartesian_category
for a being Object of C holds rho' a = <:(id a),(term a):>;

theorem Th29: :: CAT_4:29
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:30
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 15
<:(pr2 (a,b)),(pr1 (a,b)):>;
correctness
coherence
<:(pr2 (a,b)),(pr1 (a,b)):> is Morphism of a [x] b,b [x] a;
;
end;

:: deftheorem defines Switch CAT_4:def 15 :
for C being Cartesian_category
for a, b being Object of C holds Switch (a,b) = <:(pr2 (a,b)),(pr1 (a,b)):>;

theorem Th31: :: CAT_4:31
for C being Cartesian_category
for a, b being Object of C holds Hom ((a [x] b),(b [x] a)) <> {}
proof end;

theorem Th32: :: CAT_4:32
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:33
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 16
<:(id a),(id a):>;
correctness
coherence
<:(id a),(id a):> is Morphism of a,a [x] a;
;
end;

:: deftheorem defines Delta CAT_4:def 16 :
for C being Cartesian_category
for a being Object of C holds Delta a = <:(id a),(id a):>;

theorem :: CAT_4:34
for C being Cartesian_category
for a being Object of C holds Hom (a,(a [x] a)) <> {}
proof end;

theorem :: CAT_4:35
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 17
<:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;
correctness
coherence
<:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:> is Morphism of (a [x] b) [x] c,a [x] (b [x] 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 [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;
correctness
coherence
<:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):> is Morphism of a [x] (b [x] c),(a [x] b) [x] c;
;
end;

:: deftheorem defines Alpha CAT_4:def 17 :
for C being Cartesian_category
for a, b, c being Object of C holds Alpha (a,b,c) = <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;

:: deftheorem defines Alpha' CAT_4:def 18 :
for C being Cartesian_category
for a, b, c being Object of C holds Alpha' (a,b,c) = <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;

theorem Th36: :: CAT_4:36
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 Th37: :: CAT_4:37
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:38
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 19
<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;
correctness
coherence
<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):> is Morphism of a [x] c,b [x] d;
;
end;

:: deftheorem defines [x] CAT_4:def 19 :
for C being Cartesian_category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of c,d holds f [x] g = <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;

theorem :: CAT_4:39
for C being Cartesian_category
for a, b, c, 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:40
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 Th41: :: CAT_4:41
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:42
for C being Cartesian_category
for a, b, c 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:43
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 20
 for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 );
end;

:: deftheorem defines with_finite_coproduct CAT_4:def 20 :
for C being Category holds
( C is with_finite_coproduct iff for I being finite set
for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) );

theorem Th44: :: CAT_4:44
for C being Category holds
( C is with_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 c1 is strict ;
struct CoprodCatStr -> CatStr ;
aggr CoprodCatStr(# carrier, carrier', Source, Target, Comp, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ;
sel Initial c1 -> Element of the carrier of c1;
sel Coproduct c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier of c1;
sel Incl1 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
sel Incl2 c1 -> Function of [: the carrier of c1, the carrier of c1:], the carrier' of c1;
end;

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

definition
let C be non empty non void CoprodCatStr ;
func EmptyMS C -> Object of C equals :: CAT_4:def 21
 the Initial of C;
correctness
coherence
the Initial of C is Object of C;
;
let a, b be Object of C;
func a + b -> Object of C equals :: CAT_4:def 22
 the Coproduct of C . (a,b);
correctness
coherence
the Coproduct of C . (a,b) is Object of C;
;
func in1 (a,b) -> Morphism of C equals :: CAT_4:def 23
 the Incl1 of C . (a,b);
correctness
coherence
the Incl1 of C . (a,b) is Morphism of C;
;
func in2 (a,b) -> Morphism of C equals :: CAT_4:def 24
 the Incl2 of C . (a,b);
correctness
coherence
the Incl2 of C . (a,b) is Morphism of C;
;
end;

:: deftheorem defines EmptyMS CAT_4:def 21 :
for C being non empty non void CoprodCatStr holds EmptyMS C = the Initial of C;

:: deftheorem defines + CAT_4:def 22 :
for C being non empty non void CoprodCatStr
for a, b being Object of C holds a + b = the Coproduct of C . (a,b);

:: deftheorem defines in1 CAT_4:def 23 :
for C being non empty non void CoprodCatStr
for a, b being Object of C holds in1 (a,b) = the Incl1 of C . (a,b);

:: deftheorem defines in2 CAT_4:def 24 :
for C being non empty non void CoprodCatStr
for a, b being Object of C holds in2 (a,b) = the Incl2 of C . (a,b);

definition
let o, m be set ;
func c1Cat* (o,m) -> strict CoprodCatStr equals :: CAT_4:def 25
 CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);
correctness
coherence
CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #) is strict CoprodCatStr ;
;
end;

:: deftheorem defines c1Cat* CAT_4:def 25 :
for o, m being set holds c1Cat* (o,m) = CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);

theorem :: CAT_4:45
canceled;

::$CT
registration
let o, m be set ;
cluster c1Cat* (o,m) -> non empty trivial non void trivial' strict ;
coherence
( not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty & c1Cat* (o,m) is trivial & c1Cat* (o,m) is trivial' ) ;
end;

Lm2: for o, m being set holds c1Cat* (o,m) is Category-like
proof end;

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

registration
let o, m be set ;
cluster c1Cat* (o,m) -> non empty non void Category-like transitive associative reflexive with_identities strict ;
coherence
( c1Cat* (o,m) is Category-like & c1Cat* (o,m) is reflexive & c1Cat* (o,m) is transitive & c1Cat* (o,m) is associative & c1Cat* (o,m) is with_identities & not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty ) by Lm2;
end;

theorem Th45: :: CAT_4:46
for o, m being set
for a, b being Object of (c1Cat* (o,m)) holds a = b
proof end;

theorem Th46: :: CAT_4:47
for o, m being set
for f, g being Morphism of (c1Cat* (o,m)) holds f = g
proof end;

theorem Th47: :: CAT_4:48
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:49
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:50
for o, m being set
for a, b being Object of (c1Cat* (o,m)) holds Hom (a,b) <> {} by Th47;

theorem Th50: :: CAT_4:51
for o, m being set
for a being Object of (c1Cat* (o,m)) holds a is initial
proof end;

theorem Th51: :: CAT_4:52
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 non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr ;
attr IT is Cocartesian means :Def26: :: CAT_4:def 26
( 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 Def26 defines Cocartesian CAT_4:def 26 :
for IT being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr holds
( IT is Cocartesian iff ( 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) ) ) ) );

theorem Th52: :: CAT_4:53
for o, m being set holds c1Cat* (o,m) is Cocartesian by Th50, Th45, Th51;

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

definition
mode Cocartesian_category is non empty non void Category-like transitive associative reflexive with_identities Cocartesian CoprodCatStr ;
end;

theorem :: CAT_4:54
for C being Cocartesian_category holds EmptyMS C is initial by Def26;

theorem Th54: :: CAT_4:55
for C being Cocartesian_category
for a being Object of C
for f1, f2 being Morphism of EmptyMS C,a holds f1 = f2
proof end;

definition
let C be Cocartesian_category;
let a be Object of C;
func init a -> Morphism of EmptyMS C,a means :: CAT_4:def 27
verum;
existence
ex b1 being Morphism of EmptyMS C,a st verum ;
uniqueness
for b1, b2 being Morphism of EmptyMS C,a holds b1 = b2 by Th54;
end;

:: deftheorem defines init CAT_4:def 27 :
for C being Cocartesian_category
for a being Object of C
for b3 being Morphism of EmptyMS C,a holds
( b3 = init a iff verum );

theorem Th55: :: CAT_4:56
for C being Cocartesian_category
for a being Object of C holds Hom ((EmptyMS C),a) <> {}
proof end;

theorem Th56: :: CAT_4:57
for C being Cocartesian_category
for a being Object of C holds init a = init ((EmptyMS C),a)
proof end;

theorem :: CAT_4:58
for C being Cocartesian_category
for a being Object of C holds
( dom (init a) = EmptyMS C & cod (init a) = a )
proof end;

theorem :: CAT_4:59
for C being Cocartesian_category
for a being Object of C holds Hom ((EmptyMS C),a) = {(init a)}
proof end;

theorem Th59: :: CAT_4:60
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 Th60: :: CAT_4:61
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 Th61: :: CAT_4:62
for C being Cocartesian_category
for a, b being Object of C holds
( Hom (a,(a + b)) <> {} & Hom (b,(a + b)) <> {} )
proof end;

theorem :: CAT_4:63
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 Def26;

theorem :: CAT_4:64
for C being Cocartesian_category holds C is with_finite_coproduct
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
in1 (a,b) is Morphism of a,a + b
proof end;
:: original: in2
redefine func in2 (a,b) -> Morphism of b,a + b;
coherence
in2 (a,b) is Morphism of b,a + b
proof end;
end;

theorem :: CAT_4:65
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
in1 (a,b) is Morphism of a,a + b
proof end;
:: original: in2
redefine func in2 (a,b) -> Morphism of b,a + b;
coherence
in2 (a,b) is Morphism of b,a + b
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 :Def28: :: CAT_4:def 28
( it * (in1 (a,b)) = f & it * (in2 (a,b)) = g );
existence
ex b1 being Morphism of a + b,c st
( b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g )
proof end;
uniqueness
for b1, b2 being Morphism of a + b,c st b1 * (in1 (a,b)) = f & b1 * (in2 (a,b)) = g & b2 * (in1 (a,b)) = f & b2 * (in2 (a,b)) = g holds
b1 = b2
proof end;
end;

:: deftheorem Def28 defines [$ CAT_4:def 28 :
for C being Cocartesian_category
for a, b, c 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
for b7 being Morphism of a + b,c holds
( b7 = [$f,g$] iff ( b7 * (in1 (a,b)) = f & b7 * (in2 (a,b)) = g ) );

theorem Th65: :: CAT_4:66
for C being Cocartesian_category
for a, b, c being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
Hom ((a + b),c) <> {}
proof end;

theorem Th66: :: CAT_4:67
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 Th67: :: CAT_4:68
for C being Cocartesian_category
for a, b, c, 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 Th68: :: CAT_4:69
for C being Cocartesian_category
for a, b, c 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:70
for C being Cocartesian_category
for a, b, c 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:71
for C being Cocartesian_category
for a being Object of C holds
( a,a + (EmptyMS C) are_isomorphic & a,(EmptyMS C) + a are_isomorphic )
proof end;

theorem :: CAT_4:72
for C being Cocartesian_category
for a, b being Object of C holds a + b,b + a are_isomorphic
proof end;

theorem :: CAT_4:73
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 29
[$(id a),(id a)$];
correctness
coherence
[$(id a),(id a)$] is Morphism of a + a,a;
;
end;

:: deftheorem defines nabla CAT_4:def 29 :
for C being Cocartesian_category
for a being Object of C holds nabla a = [$(id a),(id a)$];

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 30
[$((in1 (c,d)) * f),((in2 (c,d)) * g)$];
correctness
coherence
[$((in1 (c,d)) * f),((in2 (c,d)) * g)$] is Morphism of a + b,c + d;
;
end;

:: deftheorem defines + CAT_4:def 30 :
for C being Cocartesian_category
for a, b, c, d being Object of C
for f being Morphism of a,c
for g being Morphism of b,d holds f + g = [$((in1 (c,d)) * f),((in2 (c,d)) * g)$];

theorem :: CAT_4:74
for C being Cocartesian_category
for a, b, c, d being Object of C st Hom (a,c) <> {} & Hom (b,d) <> {} holds
Hom ((a + b),(c + d)) <> {}
proof end;

theorem :: CAT_4:75
for C being Cocartesian_category
for a, b being Object of C holds (id a) + (id b) = id (a + b)
proof end;

theorem Th75: :: CAT_4:76
for C being Cocartesian_category
for a, b, c, 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:77
for C being Cocartesian_category
for a, b, c 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:78
for C being Cocartesian_category
for a, b, c, 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;