:: 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;

( 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;
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 ( 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 ) );

( 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;

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

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;

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

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 );

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

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

( 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 c_{1} is strict ;

struct ProdCatStr -> CatStr ;

aggr ProdCatStr(# carrier, carrier', Source, Target, Comp, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ;

sel TerminalObj c_{1} -> Element of the carrier of c_{1};

sel CatProd c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier of c_{1};

sel Proj1 c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier' of c_{1};

sel Proj2 c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier' of c_{1};

end;
struct ProdCatStr -> CatStr ;

aggr ProdCatStr(# carrier, carrier', Source, Target, Comp, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ;

sel TerminalObj c

sel CatProd c

sel Proj1 c

sel Proj2 c

registration
end;

definition

let C be non empty non void ProdCatStr ;

correctness

coherence

the TerminalObj of C is Object of C;

;

let a, b be Object of C;

correctness

coherence

the CatProd of C . (a,b) is Object of C;

;

correctness

coherence

the Proj1 of C . (a,b) is Morphism of C;

;

correctness

coherence

the Proj2 of C . (a,b) is Morphism of C;

;

end;
correctness

coherence

the TerminalObj of C is Object of C;

;

let a, b be Object of C;

correctness

coherence

the CatProd of C . (a,b) is Object of C;

;

correctness

coherence

the Proj1 of C . (a,b) is Morphism of C;

;

correctness

coherence

the Proj2 of C . (a,b) is Morphism of C;

;

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

for C being non empty non void ProdCatStr holds [1] C = the TerminalObj of C;

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);

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);

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);

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 ;

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;
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 ProdCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);

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 ;

;

:: 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) #);

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 ;

coherence

( not c1Cat (o,m) is empty & c1Cat (o,m) is trivial & not c1Cat (o,m) is void & c1Cat (o,m) is trivial' ) ;

end;
coherence

( not c1Cat (o,m) is empty & c1Cat (o,m) is trivial & not c1Cat (o,m) is void & c1Cat (o,m) is trivial' ) ;

theorem :: CAT_4:2

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

proof end;

registration

ex b_{1} being non empty non void ProdCatStr st

( b_{1} is strict & b_{1} is Category-like & b_{1} is reflexive & b_{1} is transitive & b_{1} is associative & b_{1} is with_identities & not b_{1} is void & not b_{1} is empty )
end;

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict for ProdCatStr ;

existence ex b

( b

proof end;

registration

let o, m be set ;

( 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;
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;

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)

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

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

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

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 ;

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) ) ) ) );

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) ) ) ) );

registration

ex b_{1} being non empty non void Category-like transitive associative reflexive with_identities ProdCatStr st

( b_{1} is strict & b_{1} is Cartesian )
end;

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict Cartesian for ProdCatStr ;

existence ex b

( b

proof end;

definition

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

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

for a being Object of C

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

proof end;

definition

let C be Cartesian_category;

let a be Object of C;

existence

ex b_{1} being Morphism of a, [1] C st verum
;

uniqueness

for b_{1}, b_{2} being Morphism of a, [1] C holds b_{1} = b_{2}
by Th12;

end;
let a be Object of C;

existence

ex b

uniqueness

for b

:: deftheorem defines term CAT_4:def 9 :

for C being Cartesian_category

for a being Object of C

for b_{3} being Morphism of a, [1] C holds

( b_{3} = term a iff verum );

for C being Cartesian_category

for a being Object of C

for b

( b

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 )

for a being Object of C holds

( dom (term a) = a & cod (term a) = [1] C )

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 )

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 )

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

redefine func pr2 (a,b) -> Morphism of a [x] b,b;

coherence

pr2 (a,b) is Morphism of a [x] b,b

end;
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: pr2redefine func pr2 (a,b) -> Morphism of a [x] b,b;

coherence

pr2 (a,b) is Morphism of a [x] b,b

proof 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) <> {} )

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;

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

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) <> {} ) ;

ex b_{1} being Morphism of c,a [x] b st

( (pr1 (a,b)) * b_{1} = f & (pr2 (a,b)) * b_{1} = g )

for b_{1}, b_{2} being Morphism of c,a [x] b st (pr1 (a,b)) * b_{1} = f & (pr2 (a,b)) * b_{1} = g & (pr1 (a,b)) * b_{2} = f & (pr2 (a,b)) * b_{2} = g holds

b_{1} = b_{2}

end;
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 ( (pr1 (a,b)) * it = f & (pr2 (a,b)) * it = g );

ex b

( (pr1 (a,b)) * b

proof end;

uniqueness for b

b

proof 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 b_{7} being Morphism of c,a [x] b holds

( b_{7} = <:f,g:> iff ( (pr1 (a,b)) * b_{7} = f & (pr2 (a,b)) * b_{7} = g ) );

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 b

( b

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)) <> {}

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)

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

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 )

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

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)) <> {} )

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;

correctness

coherence

pr2 (([1] C),a) is Morphism of ([1] C) [x] a,a;

;

correctness

coherence

<:(term a),(id a):> is Morphism of a,([1] C) [x] a;

;

correctness

coherence

pr1 (a,([1] C)) is Morphism of a [x] ([1] C),a;

;

correctness

coherence

<:(id a),(term a):> is Morphism of a,a [x] ([1] C);

;

end;
let a be Object of C;

correctness

coherence

pr2 (([1] C),a) is Morphism of ([1] C) [x] a,a;

;

correctness

coherence

<:(term a),(id a):> is Morphism of a,([1] C) [x] a;

;

correctness

coherence

pr1 (a,([1] C)) is Morphism of a [x] ([1] C),a;

;

correctness

coherence

<:(id a),(term a):> is Morphism of a,a [x] ([1] C);

;

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

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

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));

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

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

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 )

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;

correctness

coherence

<:(pr2 (a,b)),(pr1 (a,b)):> is Morphism of a [x] b,b [x] a;

;

end;
let a, b be Object of C;

correctness

coherence

<:(pr2 (a,b)),(pr1 (a,b)):> is Morphism of a [x] b,b [x] a;

;

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

for C being Cartesian_category

for a, b being Object of C holds Switch (a,b) = <:(pr2 (a,b)),(pr1 (a,b)):>;

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)

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

proof end;

definition

let C be Cartesian_category;

let a be Object of C;

correctness

coherence

<:(id a),(id a):> is Morphism of a,a [x] a;

;

end;
let a be Object of C;

correctness

coherence

<:(id a),(id a):> is Morphism of a,a [x] a;

;

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

for C being Cartesian_category

for a being Object of C holds Delta a = <:(id a),(id a):>;

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

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;

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);

;

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;
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 <:((pr1 (a,b)) * (pr1 ((a [x] b),c))),<:((pr2 (a,b)) * (pr1 ((a [x] b),c))),(pr2 ((a [x] b),c)):>:>;

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 <:<:(pr1 (a,(b [x] c))),((pr1 (b,c)) * (pr2 (a,(b [x] c)))):>,((pr2 (b,c)) * (pr2 (a,(b [x] c)))):>;

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;

;

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

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

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)) <> {} )

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

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

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;

coherence

<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):> is Morphism of a [x] c,b [x] d;

;

end;
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 <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;

coherence

<:(f * (pr1 (a,c))),(g * (pr2 (a,c))):> is Morphism of a [x] c,b [x] d;

;

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

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)) <> {}

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

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)

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)

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;

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

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 );

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

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

( 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 c_{1} is strict ;

struct CoprodCatStr -> CatStr ;

aggr CoprodCatStr(# carrier, carrier', Source, Target, Comp, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ;

sel Initial c_{1} -> Element of the carrier of c_{1};

sel Coproduct c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier of c_{1};

sel Incl1 c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier' of c_{1};

sel Incl2 c_{1} -> Function of [: the carrier of c_{1}, the carrier of c_{1}:], the carrier' of c_{1};

end;
struct CoprodCatStr -> CatStr ;

aggr CoprodCatStr(# carrier, carrier', Source, Target, Comp, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ;

sel Initial c

sel Coproduct c

sel Incl1 c

sel Incl2 c

registration
end;

definition

let C be non empty non void CoprodCatStr ;

correctness

coherence

the Initial of C is Object of C;

;

let a, b be Object of C;

correctness

coherence

the Coproduct of C . (a,b) is Object of C;

;

correctness

coherence

the Incl1 of C . (a,b) is Morphism of C;

;

correctness

coherence

the Incl2 of C . (a,b) is Morphism of C;

;

end;
correctness

coherence

the Initial of C is Object of C;

;

let a, b be Object of C;

correctness

coherence

the Coproduct of C . (a,b) is Object of C;

;

correctness

coherence

the Incl1 of C . (a,b) is Morphism of C;

;

correctness

coherence

the Incl2 of C . (a,b) is Morphism of C;

;

:: deftheorem defines EmptyMS CAT_4:def 21 :

for C being non empty non void CoprodCatStr holds EmptyMS C = the Initial of C;

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);

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);

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);

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 ;

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;
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 CoprodCatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m),(Extract o),((o,o) :-> o),((o,o) :-> m),((o,o) :-> m) #);

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 ;

;

:: 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) #);

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) #);

::$CT

registration

let o, m be set ;

coherence

( not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty & c1Cat* (o,m) is trivial & c1Cat* (o,m) is trivial' ) ;

end;
coherence

( not c1Cat* (o,m) is void & not c1Cat* (o,m) is empty & c1Cat* (o,m) is trivial & c1Cat* (o,m) is trivial' ) ;

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

proof end;

registration

ex b_{1} being non empty non void CoprodCatStr st

( b_{1} is strict & b_{1} is Category-like & b_{1} is reflexive & b_{1} is transitive & b_{1} is associative & b_{1} is with_identities )
end;

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict for CoprodCatStr ;

existence ex b

( b

proof end;

registration

let o, m be set ;

( 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;
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;

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)

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

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

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

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 ;

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) ) ) ) );

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) ) ) ) );

registration

ex b_{1} being non empty non void Category-like transitive associative reflexive with_identities CoprodCatStr st

( b_{1} is strict & b_{1} is Cocartesian )
end;

cluster non empty non void V59() Category-like transitive associative reflexive with_identities strict Cocartesian for CoprodCatStr ;

existence ex b

( b

proof end;

definition

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

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

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;

existence

ex b_{1} being Morphism of EmptyMS C,a st verum
;

uniqueness

for b_{1}, b_{2} being Morphism of EmptyMS C,a holds b_{1} = b_{2}
by Th54;

end;
let a be Object of C;

existence

ex b

uniqueness

for b

:: deftheorem defines init CAT_4:def 27 :

for C being Cocartesian_category

for a being Object of C

for b_{3} being Morphism of EmptyMS C,a holds

( b_{3} = init a iff verum );

for C being Cocartesian_category

for a being Object of C

for b

( b

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 )

for a being Object of C holds

( dom (init a) = EmptyMS C & cod (init a) = 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 )

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 )

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)) <> {} )

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;

for a, b being Object of C holds a + b is_a_coproduct_wrt in1 (a,b), in2 (a,b) by Def26;

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

redefine func in2 (a,b) -> Morphism of b,a + b;

coherence

in2 (a,b) is Morphism of b,a + b

end;
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: in2redefine func in2 (a,b) -> Morphism of b,a + b;

coherence

in2 (a,b) is Morphism of b,a + b

proof 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 )

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

redefine func in2 (a,b) -> Morphism of b,a + b;

coherence

in2 (a,b) is Morphism of b,a + b

end;
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: in2redefine func in2 (a,b) -> Morphism of b,a + b;

coherence

in2 (a,b) is Morphism of b,a + b

proof 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) <> {} ) ;

ex b_{1} being Morphism of a + b,c st

( b_{1} * (in1 (a,b)) = f & b_{1} * (in2 (a,b)) = g )

for b_{1}, b_{2} being Morphism of a + b,c st b_{1} * (in1 (a,b)) = f & b_{1} * (in2 (a,b)) = g & b_{2} * (in1 (a,b)) = f & b_{2} * (in2 (a,b)) = g holds

b_{1} = b_{2}

end;
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 ( it * (in1 (a,b)) = f & it * (in2 (a,b)) = g );

ex b

( b

proof end;

uniqueness for b

b

proof 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 b_{7} being Morphism of a + b,c holds

( b_{7} = [$f,g$] iff ( b_{7} * (in1 (a,b)) = f & b_{7} * (in2 (a,b)) = g ) );

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 b

( b

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) <> {}

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)

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$]

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 )

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

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 )

for a being Object of C holds

( a,a + (EmptyMS C) are_isomorphic & a,(EmptyMS C) + 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

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;

correctness

coherence

[$(id a),(id a)$] is Morphism of a + a,a;

;

end;
let a be Object of C;

correctness

coherence

[$(id a),(id a)$] is Morphism of a + a,a;

;

:: 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)$];

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;

coherence

[$((in1 (c,d)) * f),((in2 (c,d)) * g)$] is Morphism of a + b,c + d;

;

end;
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 [$((in1 (c,d)) * f),((in2 (c,d)) * g)$];

coherence

[$((in1 (c,d)) * f),((in2 (c,d)) * g)$] is Morphism of a + b,c + d;

;

:: 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)$];

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)) <> {}

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 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)$]

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$]

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)

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;