:: CAT_4 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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
( a,b are_isomorphic iff ( 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 ) ) )
by CAT_1:81;
end;

:: deftheorem CAT_4:def 1 :
canceled;

:: deftheorem defines are_isomorphic CAT_4:def 2 :
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 f' being Morphism of b,a st
( f * f' = id b & f' * f = id a ) ) );

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 :
for C being Category holds
( C is with_finite_product iff 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' ) );

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

theorem Th1: :: CAT_4:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 c1 is strict;
struct ProdCatStr -> CatStr ;
aggr ProdCatStr(# Objects, Morphisms, Dom, Cod, Comp, Id, TerminalObj, CatProd, Proj1, Proj2 #) -> ProdCatStr ;
sel TerminalObj c1 -> Element of the Objects of c1;
sel CatProd c1 -> Function of [:the Objects of c1,the Objects of c1:],the Objects of c1;
sel Proj1 c1 -> Function of [:the Objects of c1,the Objects of c1:],the Morphisms of c1;
sel Proj2 c1 -> Function of [:the Objects of c1,the Objects of c1:],the Morphisms of c1;
end;

definition
let C be ProdCatStr ;
func [1] C -> Object of C equals :: CAT_4:def 4
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 5
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 6
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 7
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 4 :
for C being ProdCatStr holds [1] C = the TerminalObj of C;

:: deftheorem defines [x] CAT_4:def 5 :
for C being ProdCatStr
for a, b being Object of C holds a [x] b = the CatProd of C . [a,b];

:: deftheorem defines pr1 CAT_4:def 6 :
for C being ProdCatStr
for a, b being Object of C holds pr1 a,b = the Proj1 of C . [a,b];

:: deftheorem defines pr2 CAT_4:def 7 :
for C being 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 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
coherence
ProdCatStr(# {o},{m},({m} --> o),({m} --> o),(m,m .--> m),({o} --> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #) is strict ProdCatStr
;
;
end;

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

theorem :: CAT_4:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being ProdCatStr st
( b1 is strict & b1 is Category-like )
proof end;
end;

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

theorem Th3: :: CAT_4:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set
for a, b being Object of (c1Cat o,m) holds a = b
proof end;

theorem Th5: :: CAT_4:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set
for f, g being Morphism of (c1Cat o,m) holds f = g
proof end;

theorem Th7: :: CAT_4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set
for a being Object of (c1Cat o,m) holds a is terminal
proof end;

theorem Th11: :: CAT_4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for IT being Category-like 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 Th12: :: CAT_4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set holds c1Cat o,m is Cartesian
proof end;

registration
cluster Category-like strict Cartesian ProdCatStr ;
existence
ex b1 being Category-like ProdCatStr st
( b1 is strict & b1 is Cartesian )
proof end;
end;

definition
mode Cartesian_category is Category-like Cartesian ProdCatStr ;
end;

theorem Th13: :: CAT_4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cartesian_category holds [1] C is terminal by Def9;

theorem Th14: :: CAT_4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Morphism of a, [1] C st verum
;
uniqueness
for b1, b2 being Morphism of a, [1] C holds b1 = b2
by Th14;
end;

:: deftheorem defines term CAT_4:def 10 :
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 Th16: :: CAT_4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cartesian_category
for a being Object of C holds term a = term a,([1] C)
proof end;

theorem :: CAT_4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th21: :: CAT_4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cartesian_category holds C has_finite_product
proof end;

theorem :: CAT_4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 Def11 defines <: CAT_4:def 11 :
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 Th25: :: CAT_4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 13
<:(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 14
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 15
<:(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 12 :
for C being Cartesian_category
for a being Object of C holds lambda a = pr2 ([1] C),a;

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

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

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

theorem Th31: :: CAT_4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
coherence
<:(pr2 a,b),(pr1 a,b):> is Morphism of a [x] b,b [x] a
;
;
end;

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

theorem Th33: :: CAT_4:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
coherence
<:(id a),(id a):> is Morphism of a,a [x] a
;
;
end;

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

theorem :: CAT_4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cartesian_category
for a being Object of C holds Hom a,(a [x] a) <> {}
proof end;

theorem :: CAT_4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 19
<:<:(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 18 :
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 19 :
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 Th38: :: CAT_4:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 20 :
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:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for C being Category holds
( C is with_finite_coproduct iff 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' ) );

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

theorem Th46: :: CAT_4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 c1 is strict;
struct CoprodCatStr -> CatStr ;
aggr CoprodCatStr(# Objects, Morphisms, Dom, Cod, Comp, Id, Initial, Coproduct, Incl1, Incl2 #) -> CoprodCatStr ;
sel Initial c1 -> Element of the Objects of c1;
sel Coproduct c1 -> Function of [:the Objects of c1,the Objects of c1:],the Objects of c1;
sel Incl1 c1 -> Function of [:the Objects of c1,the Objects of c1:],the Morphisms of c1;
sel Incl2 c1 -> Function of [:the Objects of c1,the Objects of c1:],the Morphisms of c1;
end;

definition
let C be CoprodCatStr ;
func [0] C -> Object of C equals :: CAT_4:def 22
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 23
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 24
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 25
the Incl2 of C . [a,b];
correctness
coherence
the Incl2 of C . [a,b] is Morphism of C
;
;
end;

:: deftheorem defines [0] CAT_4:def 22 :
for C being CoprodCatStr holds [0] C = the Initial of C;

:: deftheorem defines + CAT_4:def 23 :
for C being CoprodCatStr
for a, b being Object of C holds a + b = the Coproduct of C . [a,b];

:: deftheorem defines in1 CAT_4:def 24 :
for C being CoprodCatStr
for a, b being Object of C holds in1 a,b = the Incl1 of C . [a,b];

:: deftheorem defines in2 CAT_4:def 25 :
for C being 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 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
coherence
CoprodCatStr(# {o},{m},({m} --> o),({m} --> o),(m,m .--> m),({o} --> m),(Extract o),(o,o :-> o),(o,o :-> m),(o,o :-> m) #) is strict CoprodCatStr
;
;
end;

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

theorem :: CAT_4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being CoprodCatStr st
( b1 is strict & b1 is Category-like )
proof end;
end;

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

theorem Th48: :: CAT_4:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set
for a, b being Object of (c1Cat* o,m) holds a = b
proof end;

theorem Th50: :: CAT_4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set
for f, g being Morphism of (c1Cat* o,m) holds f = g
proof end;

theorem Th52: :: CAT_4:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set
for a being Object of (c1Cat* o,m) holds a is initial
proof end;

theorem Th56: :: CAT_4:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for IT being Category-like 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 Th57: :: CAT_4:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, m being set holds c1Cat* o,m is Cocartesian
proof end;

registration
cluster Category-like strict Cocartesian CoprodCatStr ;
existence
ex b1 being Category-like CoprodCatStr st
( b1 is strict & b1 is Cocartesian )
proof end;
end;

definition
mode Cocartesian_category is Category-like Cocartesian CoprodCatStr ;
end;

theorem Th58: :: CAT_4:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cocartesian_category holds [0] C is initial by Def27;

theorem Th59: :: CAT_4:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Morphism of [0] C,a st verum
;
uniqueness
for b1, b2 being Morphism of [0] C,a holds b1 = b2
by Th59;
end;

:: deftheorem defines init CAT_4:def 28 :
for C being Cocartesian_category
for a being Object of C
for b3 being Morphism of [0] C,a holds
( b3 = init a iff verum );

theorem Th60: :: CAT_4:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cocartesian_category
for a being Object of C holds Hom ([0] C),a <> {}
proof end;

theorem Th61: :: CAT_4:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cocartesian_category
for a being Object of C holds init a = init ([0] C),a
proof end;

theorem :: CAT_4:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being Cocartesian_category holds C has_finite_coproduct
proof end;

theorem :: CAT_4:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :Def29: :: CAT_4:def 29
( 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 Def29 defines [$ CAT_4:def 29 :
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 Th70: :: CAT_4:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
coherence
[$(id a),(id a)$] is Morphism of a + a,a
;
;
end;

:: deftheorem defines nabla CAT_4:def 30 :
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 31
[$((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 31 :
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:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;