:: CAT_4 semantic presentation

definition

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

end;

:: deftheorem Def1 CAT_4:def 1 :

:: deftheorem Def2 defines are_isomorphic CAT_4:def 2 :

definition

let c₁ be Category;
attr a₁ is with_finite_product means :: CAT_4:def 3
for b₁ being finite set
for b₂ being Function of b₁,the Objects of a₁ ex b₃ being Object of a₁ex b₄ being Projections_family of b₃,b₁ st
( cods b₄ = b₂ & b₃ is_a_product_wrt b₄ );

end;

:: deftheorem Def3 defines with_finite_product CAT_4:def 3 :

notation

let c₁ be Category;
synonym c₁ has_finite_product for with_finite_product c₁;

end;

theorem Th1: :: CAT_4:1

for b₁ being Category holds
( b₁ has_finite_product iff ( ex b₂ being Object of b₁ st b₂ is terminal & ( for b₂, b₃ being Object of b₁ ex b₄ being Object of b₁ex b₅, b₆ being Morphism of b₁ st
( dom b₅ = b₄ & dom b₆ = b₄ & cod b₅ = b₂ & cod b₆ = b₃ & b₄ is_a_product_wrt b₅,b₆ ) ) ) )

proof end;

definition

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

end;

definition

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

end;

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

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

:: deftheorem Def6 defines pr1 CAT_4:def 6 :

:: deftheorem Def7 defines pr2 CAT_4:def 7 :

definition

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

end;

:: deftheorem Def8 defines c1Cat CAT_4:def 8 :

theorem Th2: :: CAT_4:2

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

Lemma2: for b₁, b₂ being set holds c1Cat b₁,b₂ is Category-like

proof end;

registration

cluster Category-like strict ProdCatStr ;
existence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster c1Cat a₁,a₂ -> Category-like strict ;
coherence by Lemma2;

end;

theorem Th3: :: CAT_4:3

for b₁, b₂ being set
for b₃ being Object of (c1Cat b₁,b₂) holds b₃ = b₁ by TARSKI:def 1;

theorem Th4: :: CAT_4:4

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat b₁,b₂) holds b₃ = b₄

proof end;

theorem Th5: :: CAT_4:5

for b₁, b₂ being set
for b₃ being Morphism of (c1Cat b₁,b₂) holds b₃ = b₂ by TARSKI:def 1;

theorem Th6: :: CAT_4:6

for b₁, b₂ being set
for b₃, b₄ being Morphism of (c1Cat b₁,b₂) holds b₃ = b₄

proof end;

theorem Th7: :: CAT_4:7

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat b₁,b₂)
for b₅ being Morphism of (c1Cat b₁,b₂) holds b₅ in Hom b₃,b₄

proof end;

theorem Th8: :: CAT_4:8

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat b₁,b₂)
for b₅ being Morphism of (c1Cat b₁,b₂) holds b₅ is Morphism of b₃,b₄

proof end;

theorem Th9: :: CAT_4:9

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat b₁,b₂) holds Hom b₃,b₄ <> {} by Th7;

theorem Th10: :: CAT_4:10

for b₁, b₂ being set
for b₃ being Object of (c1Cat b₁,b₂) holds b₃ is terminal

proof end;

theorem Th11: :: CAT_4:11

for b₁, b₂ being set
for b₃ being Object of (c1Cat b₁,b₂)
for b₄, b₅ being Morphism of (c1Cat b₁,b₂) holds b₃ is_a_product_wrt b₄,b₅

proof end;

definition

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

end;

:: deftheorem Def9 defines Cartesian CAT_4:def 9 :

theorem Th12: :: CAT_4:12

for b₁, b₂ being set holds c1Cat b₁,b₂ is Cartesian

proof end;

registration

cluster Category-like strict Cartesian ProdCatStr ;
existence

proof end;

end;

definition

mode Cartesian_category is Category-like Cartesian ProdCatStr ;

end;

theorem Th13: :: CAT_4:13

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

theorem Th14: :: CAT_4:14

for b₁ being Cartesian_category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₂, [1] b₁ holds b₃ = b₄

proof end;

theorem Th15: :: CAT_4:15

for b₁ being Cartesian_category
for b₂ being Object of b₁ holds Hom b₂,([1] b₁) <> {}

proof end;

definition

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

end;

:: deftheorem Def10 defines term CAT_4:def 10 :

theorem Th16: :: CAT_4:16

for b₁ being Cartesian_category
for b₂ being Object of b₁ holds term b₂ = term b₂,([1] b₁)

proof end;

theorem Th17: :: CAT_4:17

for b₁ being Cartesian_category
for b₂ being Object of b₁ holds
( dom (term b₂) = b₂ & cod (term b₂) = [1] b₁ )

proof end;

theorem Th18: :: CAT_4:18

for b₁ being Cartesian_category
for b₂ being Object of b₁ holds Hom b₂,([1] b₁) = {(term b₂)}

proof end;

theorem Th19: :: CAT_4:19

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds
( dom (pr1 b₂,b₃) = b₂ [x] b₃ & cod (pr1 b₂,b₃) = b₂ )

proof end;

theorem Th20: :: CAT_4:20

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds
( dom (pr2 b₂,b₃) = b₂ [x] b₃ & cod (pr2 b₂,b₃) = b₃ )

proof end;

definition

let c₁ be Cartesian_category;
let c₂, c₃ be Object of c₁;
redefine func pr1 as pr1 c₂,c₃ -> Morphism of a₂ [x] a₃,a₂;
coherence

proof end;

redefine func pr2 as pr2 c₂,c₃ -> Morphism of a₂ [x] a₃,a₃;
coherence

proof end;

end;

theorem Th21: :: CAT_4:21

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds
( Hom (b₂ [x] b₃),b₂ <> {} & Hom (b₂ [x] b₃),b₃ <> {} )

proof end;

theorem Th22: :: CAT_4:22

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds b₂ [x] b₃ is_a_product_wrt pr1 b₂,b₃, pr2 b₂,b₃ by Def9;

theorem Th23: :: CAT_4:23

for b₁ being Cartesian_category holds b₁ has_finite_product

proof end;

theorem Th24: :: CAT_4:24

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

proof end;

definition

let c₁ be Cartesian_category;
let c₂, c₃, c₄ be Object of c₁;
let c₅ be Morphism of c₄,c₂;
let c₆ be Morphism of c₄,c₃;
assume E20: ( Hom c₄,c₂ <> {} & Hom c₄,c₃ <> {} ) ;
func <:c₅,c₆:> -> Morphism of a₄,a₂ [x] a₃ means :Def11: :: CAT_4:def 11
( (pr1 a₂,a₃) * a₇ = a₅ & (pr2 a₂,a₃) * a₇ = a₆ );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th25: :: CAT_4:25

for b₁ being Cartesian_category
for b₂, b₃, b₄ being Object of b₁ st Hom b₂,b₃ <> {} & Hom b₂,b₄ <> {} holds
Hom b₂,(b₃ [x] b₄) <> {}

proof end;

theorem Th26: :: CAT_4:26

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

proof end;

theorem Th27: :: CAT_4:27

for b₁ being Cartesian_category
for b₂, b₃, b₄, b₅ being Object of b₁
for b₆ being Morphism of b₂,b₃
for b₇ being Morphism of b₂,b₄
for b₈ being Morphism of b₅,b₂ st Hom b₂,b₃ <> {} & Hom b₂,b₄ <> {} & Hom b₅,b₂ <> {} holds
<:(b₆ * b₈),(b₇ * b₈):> = <:b₆,b₇:> * b₈

proof end;

theorem Th28: :: CAT_4:28

for b₁ being Cartesian_category
for b₂, b₃, b₄ being Object of b₁
for b₅, b₆ being Morphism of b₂,b₃
for b₇, b₈ being Morphism of b₂,b₄ st Hom b₂,b₃ <> {} & Hom b₂,b₄ <> {} & <:b₅,b₇:> = <:b₆,b₈:> holds
( b₅ = b₆ & b₇ = b₈ )

proof end;

theorem Th29: :: CAT_4:29

for b₁ being Cartesian_category
for b₂, b₃, b₄ being Object of b₁
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₂,b₄ st Hom b₂,b₃ <> {} & Hom b₂,b₄ <> {} & ( b₅ is monic or b₆ is monic ) holds
<:b₅,b₆:> is monic

proof end;

theorem Th30: :: CAT_4:30

for b₁ being Cartesian_category
for b₂ being Object of b₁ holds
( Hom b₂,(b₂ [x] ([1] b₁)) <> {} & Hom b₂,(([1] b₁) [x] b₂) <> {} )

proof end;

definition

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

end;

:: deftheorem Def12 defines lambda CAT_4:def 12 :

:: deftheorem Def13 defines lambda' CAT_4:def 13 :

:: deftheorem Def14 defines rho CAT_4:def 14 :

:: deftheorem Def15 defines rho' CAT_4:def 15 :

theorem Th31: :: CAT_4:31

for b₁ being Cartesian_category
for b₂ being Object of b₁ holds
( (lambda b₂) * (lambda' b₂) = id b₂ & (lambda' b₂) * (lambda b₂) = id (([1] b₁) [x] b₂) & (rho b₂) * (rho' b₂) = id b₂ & (rho' b₂) * (rho b₂) = id (b₂ [x] ([1] b₁)) )

proof end;

theorem Th32: :: CAT_4:32

for b₁ being Cartesian_category
for b₂ being Object of b₁ holds
( b₂,b₂ [x] ([1] b₁) are_isomorphic & b₂,([1] b₁) [x] b₂ are_isomorphic )

proof end;

definition

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

end;

:: deftheorem Def16 defines Switch CAT_4:def 16 :

theorem Th33: :: CAT_4:33

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds Hom (b₂ [x] b₃),(b₃ [x] b₂) <> {}

proof end;

theorem Th34: :: CAT_4:34

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds (Switch b₂,b₃) * (Switch b₃,b₂) = id (b₃ [x] b₂)

proof end;

theorem Th35: :: CAT_4:35

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds b₂ [x] b₃,b₃ [x] b₂ are_isomorphic

proof end;

definition

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

end;

:: deftheorem Def17 defines Delta CAT_4:def 17 :

theorem Th36: :: CAT_4:36

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

proof end;

theorem Th37: :: CAT_4:37

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁
for b₄ being Morphism of b₂,b₃ st Hom b₂,b₃ <> {} holds
<:b₄,b₄:> = (Delta b₃) * b₄

proof end;

definition

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

end;

:: deftheorem Def18 defines Alpha CAT_4:def 18 :

:: deftheorem Def19 defines Alpha' CAT_4:def 19 :

theorem Th38: :: CAT_4:38

for b₁ being Cartesian_category
for b₂, b₃, b₄ being Object of b₁ holds
( Hom ((b₂ [x] b₃) [x] b₄),(b₂ [x] (b₃ [x] b₄)) <> {} & Hom (b₂ [x] (b₃ [x] b₄)),((b₂ [x] b₃) [x] b₄) <> {} )

proof end;

theorem Th39: :: CAT_4:39

for b₁ being Cartesian_category
for b₂, b₃, b₄ being Object of b₁ holds
( (Alpha b₂,b₃,b₄) * (Alpha' b₂,b₃,b₄) = id (b₂ [x] (b₃ [x] b₄)) & (Alpha' b₂,b₃,b₄) * (Alpha b₂,b₃,b₄) = id ((b₂ [x] b₃) [x] b₄) )

proof end;

theorem Th40: :: CAT_4:40

for b₁ being Cartesian_category
for b₂, b₃, b₄ being Object of b₁ holds (b₂ [x] b₃) [x] b₄,b₂ [x] (b₃ [x] b₄) are_isomorphic

proof end;

definition

let c₁ be Cartesian_category;
let c₂, c₃, c₄, c₅ be Object of c₁;
let c₆ be Morphism of c₂,c₃;
let c₇ be Morphism of c₄,c₅;
func c₆ [x] c₇ -> Morphism of a₂ [x] a₄,a₃ [x] a₅ equals :: CAT_4:def 20
<:(a₆ * (pr1 a₂,a₄)),(a₇ * (pr2 a₂,a₄)):>;
correctness ;

end;

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

theorem Th41: :: CAT_4:41

for b₁ being Cartesian_category
for b₂, b₃, b₄, b₅ being Object of b₁ st Hom b₂,b₃ <> {} & Hom b₄,b₅ <> {} holds
Hom (b₂ [x] b₄),(b₃ [x] b₅) <> {}

proof end;

theorem Th42: :: CAT_4:42

for b₁ being Cartesian_category
for b₂, b₃ being Object of b₁ holds (id b₂) [x] (id b₃) = id (b₂ [x] b₃)

proof end;

theorem Th43: :: CAT_4:43

for b₁ being Cartesian_category
for b₂, b₃, b₄, b₅, b₆ being Object of b₁
for b₇ being Morphism of b₂,b₃
for b₈ being Morphism of b₄,b₅
for b₉ being Morphism of b₆,b₂
for b₁₀ being Morphism of b₆,b₄ st Hom b₂,b₃ <> {} & Hom b₄,b₅ <> {} & Hom b₆,b₂ <> {} & Hom b₆,b₄ <> {} holds
(b₇ [x] b₈) * <:b₉,b₁₀:> = <:(b₇ * b₉),(b₈ * b₁₀):>

proof end;

theorem Th44: :: CAT_4:44

for b₁ being Cartesian_category
for b₂, b₃, b₄ being Object of b₁
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₂,b₄ st Hom b₂,b₃ <> {} & Hom b₂,b₄ <> {} holds
<:b₅,b₆:> = (b₅ [x] b₆) * (Delta b₂)

proof end;

theorem Th45: :: CAT_4:45

for b₁ being Cartesian_category
for b₂, b₃, b₄, b₅, b₆, b₇ being Object of b₁
for b₈ being Morphism of b₂,b₃
for b₉ being Morphism of b₄,b₅
for b₁₀ being Morphism of b₆,b₂
for b₁₁ being Morphism of b₇,b₄ st Hom b₂,b₃ <> {} & Hom b₄,b₅ <> {} & Hom b₆,b₂ <> {} & Hom b₇,b₄ <> {} holds
(b₈ [x] b₉) * (b₁₀ [x] b₁₁) = (b₈ * b₁₀) [x] (b₉ * b₁₁)

proof end;

definition

let c₁ be Category;
attr a₁ is with_finite_coproduct means :: CAT_4:def 21
for b₁ being finite set
for b₂ being Function of b₁,the Objects of a₁ ex b₃ being Object of a₁ex b₄ being Injections_family of b₃,b₁ st
( doms b₄ = b₂ & b₃ is_a_coproduct_wrt b₄ );

end;

:: deftheorem Def21 defines with_finite_coproduct CAT_4:def 21 :

notation

let c₁ be Category;
synonym c₁ has_finite_coproduct for with_finite_coproduct c₁;

end;

theorem Th46: :: CAT_4:46

for b₁ being Category holds
( b₁ has_finite_coproduct iff ( ex b₂ being Object of b₁ st b₂ is initial & ( for b₂, b₃ being Object of b₁ ex b₄ being Object of b₁ex b₅, b₆ being Morphism of b₁ st
( dom b₅ = b₂ & dom b₆ = b₃ & cod b₅ = b₄ & cod b₆ = b₄ & b₄ is_a_coproduct_wrt b₅,b₆ ) ) ) )

proof end;

definition

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

end;

definition

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

end;

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

:: deftheorem Def23 defines + CAT_4:def 23 :

:: deftheorem Def24 defines in1 CAT_4:def 24 :

:: deftheorem Def25 defines in2 CAT_4:def 25 :

definition

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

end;

:: deftheorem Def26 defines c1Cat* CAT_4:def 26 :

theorem Th47: :: CAT_4:47

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

Lemma33: for b₁, b₂ being set holds c1Cat* b₁,b₂ is Category-like

proof end;

registration

cluster Category-like strict CoprodCatStr ;
existence

proof end;

end;

registration

let c₁, c₂ be set ;
cluster c1Cat* a₁,a₂ -> Category-like strict ;
coherence by Lemma33;

end;

theorem Th48: :: CAT_4:48

for b₁, b₂ being set
for b₃ being Object of (c1Cat* b₁,b₂) holds b₃ = b₁ by TARSKI:def 1;

theorem Th49: :: CAT_4:49

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat* b₁,b₂) holds b₃ = b₄

proof end;

theorem Th50: :: CAT_4:50

for b₁, b₂ being set
for b₃ being Morphism of (c1Cat* b₁,b₂) holds b₃ = b₂ by TARSKI:def 1;

theorem Th51: :: CAT_4:51

for b₁, b₂ being set
for b₃, b₄ being Morphism of (c1Cat* b₁,b₂) holds b₃ = b₄

proof end;

theorem Th52: :: CAT_4:52

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat* b₁,b₂)
for b₅ being Morphism of (c1Cat* b₁,b₂) holds b₅ in Hom b₃,b₄

proof end;

theorem Th53: :: CAT_4:53

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat* b₁,b₂)
for b₅ being Morphism of (c1Cat* b₁,b₂) holds b₅ is Morphism of b₃,b₄

proof end;

theorem Th54: :: CAT_4:54

for b₁, b₂ being set
for b₃, b₄ being Object of (c1Cat* b₁,b₂) holds Hom b₃,b₄ <> {} by Th52;

theorem Th55: :: CAT_4:55

for b₁, b₂ being set
for b₃ being Object of (c1Cat* b₁,b₂) holds b₃ is initial

proof end;

theorem Th56: :: CAT_4:56

for b₁, b₂ being set
for b₃ being Object of (c1Cat* b₁,b₂)
for b₄, b₅ being Morphism of (c1Cat* b₁,b₂) holds b₃ is_a_coproduct_wrt b₄,b₅

proof end;

definition

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

end;

:: deftheorem Def27 defines Cocartesian CAT_4:def 27 :

theorem Th57: :: CAT_4:57

for b₁, b₂ being set holds c1Cat* b₁,b₂ is Cocartesian

proof end;

registration

cluster Category-like strict Cocartesian CoprodCatStr ;
existence

proof end;

end;

definition

mode Cocartesian_category is Category-like Cocartesian CoprodCatStr ;

end;

theorem Th58: :: CAT_4:58

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

theorem Th59: :: CAT_4:59

for b₁ being Cocartesian_category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of [0] b₁,b₂ holds b₃ = b₄

proof end;

definition

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

end;

:: deftheorem Def28 defines init CAT_4:def 28 :

theorem Th60: :: CAT_4:60

for b₁ being Cocartesian_category
for b₂ being Object of b₁ holds Hom ([0] b₁),b₂ <> {}

proof end;

theorem Th61: :: CAT_4:61

for b₁ being Cocartesian_category
for b₂ being Object of b₁ holds init b₂ = init ([0] b₁),b₂

proof end;

theorem Th62: :: CAT_4:62

for b₁ being Cocartesian_category
for b₂ being Object of b₁ holds
( dom (init b₂) = [0] b₁ & cod (init b₂) = b₂ )

proof end;

theorem Th63: :: CAT_4:63

for b₁ being Cocartesian_category
for b₂ being Object of b₁ holds Hom ([0] b₁),b₂ = {(init b₂)}

proof end;

theorem Th64: :: CAT_4:64

for b₁ being Cocartesian_category
for b₂, b₃ being Object of b₁ holds
( dom (in1 b₂,b₃) = b₂ & cod (in1 b₂,b₃) = b₂ + b₃ )

proof end;

theorem Th65: :: CAT_4:65

for b₁ being Cocartesian_category
for b₂, b₃ being Object of b₁ holds
( dom (in2 b₂,b₃) = b₃ & cod (in2 b₂,b₃) = b₂ + b₃ )

proof end;

theorem Th66: :: CAT_4:66

for b₁ being Cocartesian_category
for b₂, b₃ being Object of b₁ holds
( Hom b₂,(b₂ + b₃) <> {} & Hom b₃,(b₂ + b₃) <> {} )

proof end;

theorem Th67: :: CAT_4:67

for b₁ being Cocartesian_category
for b₂, b₃ being Object of b₁ holds b₂ + b₃ is_a_coproduct_wrt in1 b₂,b₃, in2 b₂,b₃ by Def27;

theorem Th68: :: CAT_4:68

for b₁ being Cocartesian_category holds b₁ has_finite_coproduct

proof end;

theorem Th69: :: CAT_4:69

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

proof end;

definition

let c₁ be Cocartesian_category;
let c₂, c₃ be Object of c₁;
redefine func in1 as in1 c₂,c₃ -> Morphism of a₂,a₂ + a₃;
coherence

proof end;

redefine func in2 as in2 c₂,c₃ -> Morphism of a₃,a₂ + a₃;
coherence

proof end;

end;

definition

let c₁ be Cocartesian_category;
let c₂, c₃, c₄ be Object of c₁;
let c₅ be Morphism of c₂,c₄;
let c₆ be Morphism of c₃,c₄;
assume E51: ( Hom c₂,c₄ <> {} & Hom c₃,c₄ <> {} ) ;
func [$c₅,c₆$] -> Morphism of a₂ + a₃,a₄ means :Def29: :: CAT_4:def 29
( a₇ * (in1 a₂,a₃) = a₅ & a₇ * (in2 a₂,a₃) = a₆ );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th70: :: CAT_4:70

for b₁ being Cocartesian_category
for b₂, b₃, b₄ being Object of b₁ st Hom b₂,b₃ <> {} & Hom b₄,b₃ <> {} holds
Hom (b₂ + b₄),b₃ <> {}

proof end;

theorem Th71: :: CAT_4:71

for b₁ being Cocartesian_category
for b₂, b₃ being Object of b₁ holds [$(in1 b₂,b₃),(in2 b₂,b₃)$] = id (b₂ + b₃)

proof end;

theorem Th72: :: CAT_4:72

for b₁ being Cocartesian_category
for b₂, b₃, b₄, b₅ being Object of b₁
for b₆ being Morphism of b₂,b₃
for b₇ being Morphism of b₄,b₃
for b₈ being Morphism of b₃,b₅ st Hom b₂,b₃ <> {} & Hom b₄,b₃ <> {} & Hom b₃,b₅ <> {} holds
[$(b₈ * b₆),(b₈ * b₇)$] = b₈ * [$b₆,b₇$]

proof end;

theorem Th73: :: CAT_4:73

for b₁ being Cocartesian_category
for b₂, b₃, b₄ being Object of b₁
for b₅, b₆ being Morphism of b₂,b₃
for b₇, b₈ being Morphism of b₄,b₃ st Hom b₂,b₃ <> {} & Hom b₄,b₃ <> {} & [$b₅,b₇$] = [$b₆,b₈$] holds
( b₅ = b₆ & b₇ = b₈ )

proof end;

theorem Th74: :: CAT_4:74

for b₁ being Cocartesian_category
for b₂, b₃, b₄ being Object of b₁
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₄,b₃ st Hom b₂,b₃ <> {} & Hom b₄,b₃ <> {} & ( b₅ is epi or b₆ is epi ) holds
[$b₅,b₆$] is epi

proof end;

theorem Th75: :: CAT_4:75

for b₁ being Cocartesian_category
for b₂ being Object of b₁ holds
( b₂,b₂ + ([0] b₁) are_isomorphic & b₂,([0] b₁) + b₂ are_isomorphic )

proof end;

theorem Th76: :: CAT_4:76

for b₁ being Cocartesian_category
for b₂, b₃ being Object of b₁ holds b₂ + b₃,b₃ + b₂ are_isomorphic

proof end;

theorem Th77: :: CAT_4:77

for b₁ being Cocartesian_category
for b₂, b₃, b₄ being Object of b₁ holds (b₂ + b₃) + b₄,b₂ + (b₃ + b₄) are_isomorphic

proof end;

definition

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

end;

:: deftheorem Def30 defines nabla CAT_4:def 30 :

definition

let c₁ be Cocartesian_category;
let c₂, c₃, c₄, c₅ be Object of c₁;
let c₆ be Morphism of c₂,c₄;
let c₇ be Morphism of c₃,c₅;
func c₆ + c₇ -> Morphism of a₂ + a₃,a₄ + a₅ equals :: CAT_4:def 31
[$((in1 a₄,a₅) * a₆),((in2 a₄,a₅) * a₇)$];
correctness ;

end;

:: deftheorem Def31 defines + CAT_4:def 31 :

theorem Th78: :: CAT_4:78

for b₁ being Cocartesian_category
for b₂, b₃, b₄, b₅ being Object of b₁ st Hom b₂,b₃ <> {} & Hom b₄,b₅ <> {} holds
Hom (b₂ + b₄),(b₃ + b₅) <> {}

proof end;

theorem Th79: :: CAT_4:79

for b₁ being Cocartesian_category
for b₂, b₃ being Object of b₁ holds (id b₂) + (id b₃) = id (b₂ + b₃)

proof end;

theorem Th80: :: CAT_4:80

for b₁ being Cocartesian_category
for b₂, b₃, b₄, b₅, b₆ being Object of b₁
for b₇ being Morphism of b₂,b₃
for b₈ being Morphism of b₄,b₅
for b₉ being Morphism of b₃,b₆
for b₁₀ being Morphism of b₅,b₆ st Hom b₂,b₃ <> {} & Hom b₄,b₅ <> {} & Hom b₃,b₆ <> {} & Hom b₅,b₆ <> {} holds
[$b₉,b₁₀$] * (b₇ + b₈) = [$(b₉ * b₇),(b₁₀ * b₈)$]

proof end;

theorem Th81: :: CAT_4:81

for b₁ being Cocartesian_category
for b₂, b₃, b₄ being Object of b₁
for b₅ being Morphism of b₂,b₃
for b₆ being Morphism of b₄,b₃ st Hom b₂,b₃ <> {} & Hom b₄,b₃ <> {} holds
(nabla b₃) * (b₅ + b₆) = [$b₅,b₆$]

proof end;

theorem Th82: :: CAT_4:82

for b₁ being Cocartesian_category
for b₂, b₃, b₄, b₅, b₆, b₇ being Object of b₁
for b₈ being Morphism of b₂,b₃
for b₉ being Morphism of b₄,b₅
for b₁₀ being Morphism of b₃,b₆
for b₁₁ being Morphism of b₅,b₇ st Hom b₂,b₃ <> {} & Hom b₄,b₅ <> {} & Hom b₃,b₆ <> {} & Hom b₅,b₇ <> {} holds
(b₁₀ + b₁₁) * (b₈ + b₉) = (b₁₀ * b₈) + (b₁₁ * b₉)

proof end;