:: Exponential Objects
:: by Marco Riccardi
::
:: Received August 15, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Th1: :: CAT_8:1

for C being associative composable CategoryStr
for f1, f2, f3 being morphism of C st f1 |> f2 & f2 |> f3 holds
(f1 (*) f2) (*) f3 = f1 (*) (f2 (*) f3)

proof end;

theorem Th2: :: CAT_8:2

for C being associative composable CategoryStr
for f1, f2, f3, f4 being morphism of C st f1 |> f2 & f2 |> f3 & f3 |> f4 holds
( ((f1 (*) f2) (*) f3) (*) f4 = (f1 (*) f2) (*) (f3 (*) f4) & ((f1 (*) f2) (*) f3) (*) f4 = (f1 (*) (f2 (*) f3)) (*) f4 & ((f1 (*) f2) (*) f3) (*) f4 = f1 (*) ((f2 (*) f3) (*) f4) & ((f1 (*) f2) (*) f3) (*) f4 = f1 (*) (f2 (*) (f3 (*) f4)) )

proof end;

theorem Th3: :: CAT_8:3

for C being composable CategoryStr
for f, f1, f2 being morphism of C st f1 |> f2 holds
( ( f1 (*) f2 |> f implies f2 |> f ) & ( f2 |> f implies f1 (*) f2 |> f ) & ( f |> f1 (*) f2 implies f |> f1 ) & ( f |> f1 implies f |> f1 (*) f2 ) )

proof end;

theorem Th4: :: CAT_8:4

for C being composable with_identities CategoryStr
for f1, f2 being morphism of C st f1 |> f2 holds
( ( f1 is identity implies f1 (*) f2 = f2 ) & ( f2 is identity implies f1 (*) f2 = f1 ) )

proof end;

theorem Th5: :: CAT_8:5

for C being non empty with_identities CategoryStr
for f being morphism of C ex f1, f2 being morphism of C st
( f1 is identity & f2 is identity & f1 |> f & f |> f2 )

proof end;

theorem Th6: :: CAT_8:6

for C being CategoryStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) = {f} holds
for g being Morphism of a,b holds f = g

proof end;

theorem Th7: :: CAT_8:7

for C being CategoryStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & ( for g being Morphism of a,b holds f = g ) holds
Hom (a,b) = {f}

proof end;

theorem Th8: :: CAT_8:8

for x being object
for C being CategoryStr st the carrier of C = {x} & the composition of C = {[[x,x],x]} holds
C is non empty category

proof end;

theorem Th9: :: CAT_8:9

for C1, C2 being category
for F being Functor of C1,C2 st F is isomorphism holds
F is bijective

proof end;

theorem Th10: :: CAT_8:10

for C1, C2, C3 being composable with_identities CategoryStr st C1 ~= C2 & C2 ~= C3 holds
C1 ~= C3

proof end;

theorem :: CAT_8:11

for C1, C2 being category st C1 ~= C2 holds
( C1 is empty iff C2 is empty )

proof end;

registration

let C1 be empty with_identities CategoryStr ;
let C2 be with_identities CategoryStr ;

cluster Function-like quasi_total -> covariant for Element of bool [: the carrier of C1, the carrier of C2:];

correctness
coherence
for b₁ being Functor of C1,C2 holds b₁ is covariant ;

proof end;

end;

theorem :: CAT_8:12

for C1, C2 being with_identities CategoryStr
for f being morphism of C1
for F being Functor of C1,C2 st F is covariant & f is identity holds
F . f is identity by CAT_6:def 22, CAT_6:def 25;

theorem Th13: :: CAT_8:13

for C1, C2 being with_identities CategoryStr
for f1, f2 being morphism of C1
for F being Functor of C1,C2 st F is covariant & f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) )

proof end;

theorem Th14: :: CAT_8:14

for C being Category
for f being Morphism of C
for g being morphism of (alter C) st f = g holds
( dom g = id (dom f) & cod g = id (cod f) )

proof end;

theorem Th15: :: CAT_8:15

ex f being morphism of (OrdC 1) st
( f is identity & Ob (OrdC 1) = {f} & Mor (OrdC 1) = {f} )

proof end;

theorem Th16: :: CAT_8:16

for C being non empty category
for f1, f2 being morphism of C st MORPHISM f1 = MORPHISM f2 holds
f1 = f2

proof end;

theorem Th17: :: CAT_8:17

for C being non empty category
for F1, F2 being covariant Functor of (OrdC 2),C
for f being morphism of (OrdC 2) st not f is identity & F1 . f = F2 . f holds
F1 = F2

proof end;

theorem Th18: :: CAT_8:18

ex f1, f2 being morphism of (OrdC 3) st
( not f1 is identity & not f2 is identity & cod f1 = dom f2 & Ob (OrdC 3) = {(dom f1),(cod f1),(cod f2)} & Mor (OrdC 3) = {(dom f1),(cod f1),(cod f2),f1,f2,(f2 (*) f1)} & dom f1, cod f1, cod f2,f1,f2,f2 (*) f1 are_mutually_distinct )

proof end;

definition

let C be non empty category;
let f1, f2 be morphism of C;
assume A1: f1 |> f2 ;

func COMPOSITION (f1,f2) -> covariant Functor of (OrdC 3),C means :Def1: :: CAT_8:def 1
for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( it . g1 = f1 & it . g2 = f2 );

correctness
existence
ex b₁ being covariant Functor of (OrdC 3),C st
for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₁ . g1 = f1 & b₁ . g2 = f2 );
uniqueness
for b₁, b₂ being covariant Functor of (OrdC 3),C st ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₁ . g1 = f1 & b₁ . g2 = f2 ) ) & ( for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₂ . g1 = f1 & b₂ . g2 = f2 ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def1 defines COMPOSITION CAT_8:def 1 :
for C being non empty category
for f1, f2 being morphism of C st f1 |> f2 holds
for b₄ being covariant Functor of (OrdC 3),C holds
( b₄ = COMPOSITION (f1,f2) iff for g1, g2 being morphism of (OrdC 3) st g1 |> g2 & not g1 is identity & not g2 is identity holds
( b₄ . g1 = f1 & b₄ . g2 = f2 ) );

definition

let C be CategoryStr ;
let a be Object of C;

attr a is terminal means :: CAT_8:def 2
for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g );

end;

:: deftheorem defines terminal CAT_8:def 2 :
for C being CategoryStr
for a being Object of C holds
( a is terminal iff for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g ) );

theorem :: CAT_8:19

for C being CategoryStr
for b being Object of C holds
( b is terminal iff for a being Object of C ex f being Morphism of a,b st Hom (a,b) = {f} )

proof end;

theorem Th20: :: CAT_8:20

for C being non empty with_identities CategoryStr
for a being Object of C st a is terminal holds
for h being Morphism of a,a holds id- a = h

proof end;

theorem :: CAT_8:21

for C being non empty composable with_identities CategoryStr
for a, b being Object of C st a is terminal & b is terminal holds
a,b are_isomorphic

proof end;

theorem :: CAT_8:22

for C being non empty category
for a, b being Object of C st b is terminal & a,b are_isomorphic holds
a is terminal

proof end;

theorem :: CAT_8:23

for C being composable with_identities CategoryStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & a is terminal holds
f is monomorphism

proof end;

definition

let C be category;

attr C is with_terminal_objects means :: CAT_8:def 3
ex a being Object of C st a is terminal ;

end;

:: deftheorem defines with_terminal_objects CAT_8:def 3 :
for C being category holds
( C is with_terminal_objects iff ex a being Object of C st a is terminal );

theorem Th24: :: CAT_8:24

OrdC 1 is with_terminal_objects

proof end;

registration

cluster associative composable with_identities with_terminal_objects for CategoryStr ;

correctness
existence
ex b₁ being category st b₁ is with_terminal_objects ;
by Th24;

end;

definition

let C be category;

attr C is terminal means :Def4: :: CAT_8:def 4
for B being category ex F being Functor of B,C st
( F is covariant & ( for G being Functor of B,C st G is covariant holds
F = G ) );

end;

:: deftheorem Def4 defines terminal CAT_8:def 4 :
for C being category holds
( C is terminal iff for B being category ex F being Functor of B,C st
( F is covariant & ( for G being Functor of B,C st G is covariant holds
F = G ) ) );

registration

cluster OrdC 1 -> non empty terminal ;

correctness
coherence
( not OrdC 1 is empty & OrdC 1 is terminal );

proof end;

end;

registration

cluster non empty strict associative composable with_identities terminal for CategoryStr ;

correctness
existence
ex b₁ being category st
( b₁ is strict & not b₁ is empty & b₁ is terminal );

proof end;

cluster strict associative composable with_identities non terminal for CategoryStr ;

correctness
existence
ex b₁ being category st
( b₁ is strict & not b₁ is terminal );

proof end;

end;

theorem Th25: :: CAT_8:25

for C, D being terminal category holds C ~= D

proof end;

theorem Th26: :: CAT_8:26

for C, D being category st C is terminal & C ~= D holds
D is terminal

proof end;

Lm1: for C being category st C is terminal holds
( not C is empty & C is trivial )

proof end;

theorem Th27: :: CAT_8:27

for C being category holds
( ( not C is empty & C is trivial ) iff C ~= OrdC 1 )

proof end;

theorem Th28: :: CAT_8:28

for C, D being non empty category st C is trivial & D is trivial holds
C ~= D

proof end;

registration

cluster non empty trivial associative composable with_identities -> terminal for CategoryStr ;

correctness
coherence
for b₁ being category st not b₁ is empty & b₁ is trivial holds
b₁ is terminal ;

proof end;

cluster associative composable with_identities terminal -> non empty trivial for CategoryStr ;

correctness
coherence
for b₁ being category st b₁ is terminal holds
( not b₁ is empty & b₁ is trivial );
by Lm1;

end;

definition

let C be category;

func C ->OrdC1 -> covariant Functor of C,(OrdC 1) means :: CAT_8:def 5
verum;

correctness
existence
ex b₁ being covariant Functor of C,(OrdC 1) st verum;
uniqueness
for b₁, b₂ being covariant Functor of C,(OrdC 1) holds b₁ = b₂;

proof end;

end;

:: deftheorem defines ->OrdC1 CAT_8:def 5 :
for C being category
for b₂ being covariant Functor of C,(OrdC 1) holds
( b₂ = C ->OrdC1 iff verum );

theorem Th29: :: CAT_8:29

for C, C1, C2 being category
for F1 being Functor of C,C1
for F2 being Functor of C,C2 st F1 is covariant & F2 is covariant holds
(C1 ->OrdC1) (*) F1 = (C2 ->OrdC1) (*) F2

proof end;

definition

let C be CategoryStr ;
let a be Object of C;

attr a is initial means :: CAT_8:def 6
for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g );

end;

:: deftheorem defines initial CAT_8:def 6 :
for C being CategoryStr
for a being Object of C holds
( a is initial iff for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g ) );

theorem :: CAT_8:30

for C being CategoryStr
for b being Object of C holds
( b is initial iff for a being Object of C ex f being Morphism of b,a st Hom (b,a) = {f} )

proof end;

theorem Th31: :: CAT_8:31

for C being non empty with_identities CategoryStr
for a being Object of C st a is initial holds
for h being Morphism of a,a holds id- a = h

proof end;

theorem :: CAT_8:32

for C being non empty composable with_identities CategoryStr
for a, b being Object of C st a is initial & b is initial holds
a,b are_isomorphic

proof end;

theorem :: CAT_8:33

for C being non empty category
for a, b being Object of C st b is initial & b,a are_isomorphic holds
a is initial

proof end;

theorem :: CAT_8:34

for C being composable with_identities CategoryStr
for a, b being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} & b is initial holds
f is epimorphism

proof end;

definition

let C be category;

attr C is with_initial_objects means :: CAT_8:def 7
ex a being Object of C st a is initial ;

end;

:: deftheorem defines with_initial_objects CAT_8:def 7 :
for C being category holds
( C is with_initial_objects iff ex a being Object of C st a is initial );

theorem Th35: :: CAT_8:35

OrdC 1 is with_initial_objects

proof end;

registration

cluster associative composable with_identities with_initial_objects for CategoryStr ;

correctness
existence
ex b₁ being category st b₁ is with_initial_objects ;
by Th35;

end;

definition

let C be category;

attr C is initial means :Def8: :: CAT_8:def 8
for C1 being category ex F being Functor of C,C1 st
( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
F = F1 ) );

end;

:: deftheorem Def8 defines initial CAT_8:def 8 :
for C being category holds
( C is initial iff for C1 being category ex F being Functor of C,C1 st
( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
F = F1 ) ) );

registration

cluster OrdC 0 -> empty initial ;

correctness
coherence
( OrdC 0 is empty & OrdC 0 is initial );

proof end;

end;

registration

cluster empty strict associative composable with_identities initial for CategoryStr ;

correctness
existence
ex b₁ being category st
( b₁ is strict & b₁ is empty & b₁ is initial );

proof end;

cluster strict associative composable with_identities non initial for CategoryStr ;

correctness
existence
ex b₁ being category st
( b₁ is strict & not b₁ is initial );

proof end;

end;

theorem :: CAT_8:36

for C, D being initial category holds C ~= D

proof end;

theorem :: CAT_8:37

for C, D being category st C is initial & C ~= D holds
D is initial

proof end;

registration

cluster empty associative composable with_identities -> initial for CategoryStr ;

correctness
coherence
for b₁ being category st b₁ is empty holds
b₁ is initial ;

proof end;

end;

definition

let C be category;

func OrdC0-> C -> covariant Functor of (OrdC 0),C means :: CAT_8:def 9
verum;

correctness
existence
ex b₁ being covariant Functor of (OrdC 0),C st verum;
uniqueness
for b₁, b₂ being covariant Functor of (OrdC 0),C holds b₁ = b₂;
;

end;

:: deftheorem defines OrdC0-> CAT_8:def 9 :
for C being category
for b₂ being covariant Functor of (OrdC 0),C holds
( b₂ = OrdC0-> C iff verum );

theorem :: CAT_8:38

for C, C1, C2 being category
for F1 being Functor of C1,C
for F2 being Functor of C2,C st F1 is covariant & F2 is covariant holds
F1 (*) (OrdC0-> C1) = F2 (*) (OrdC0-> C2) ;

definition

let C be category;
let a, b, c be Object of C;
let p1 be Morphism of c,a;
assume Hom (c,a) <> {} ;
let p2 be Morphism of c,b;
assume Hom (c,b) <> {} ;

pred c,p1,p2 is_product_of a,b means :Def10: :: CAT_8:def 10
for c1 being Object of C
for q1 being Morphism of c1,a
for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds
( Hom (c1,c) <> {} & ex h being Morphism of c1,c st
( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds
h = h1 ) ) );

end;

:: deftheorem Def10 defines is_product_of CAT_8:def 10 :
for C being category
for a, b, c being Object of C
for p1 being Morphism of c,a st Hom (c,a) <> {} holds
for p2 being Morphism of c,b st Hom (c,b) <> {} holds
( c,p1,p2 is_product_of a,b iff for c1 being Object of C
for q1 being Morphism of c1,a
for q2 being Morphism of c1,b st Hom (c1,a) <> {} & Hom (c1,b) <> {} holds
( Hom (c1,c) <> {} & ex h being Morphism of c1,c st
( p1 * h = q1 & p2 * h = q2 & ( for h1 being Morphism of c1,c st p1 * h1 = q1 & p2 * h1 = q2 holds
h = h1 ) ) ) );

theorem :: CAT_8:39

for C being non empty category
for c1, c2, a, b being Object of C
for p1 being Morphism of a,c1
for p2 being Morphism of a,c2
for q1 being Morphism of b,c1
for q2 being Morphism of b,c2 st Hom (a,c1) <> {} & Hom (a,c2) <> {} & Hom (b,c1) <> {} & Hom (b,c2) <> {} & a,p1,p2 is_product_of c1,c2 & b,q1,q2 is_product_of c1,c2 holds
a,b are_isomorphic

proof end;

theorem :: CAT_8:40

for C being category
for c1, c2, d being Object of C
for p1 being Morphism of d,c1
for p2 being Morphism of d,c2 st Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 holds
d,p2,p1 is_product_of c2,c1

proof end;

definition

let C be category;

attr C is with_binary_products means :Def11: :: CAT_8:def 11
for a, b being Object of C ex d being Object of C ex p1 being Morphism of d,a ex p2 being Morphism of d,b st
( Hom (d,a) <> {} & Hom (d,b) <> {} & d,p1,p2 is_product_of a,b );

end;

:: deftheorem Def11 defines with_binary_products CAT_8:def 11 :
for C being category holds
( C is with_binary_products iff for a, b being Object of C ex d being Object of C ex p1 being Morphism of d,a ex p2 being Morphism of d,b st
( Hom (d,a) <> {} & Hom (d,b) <> {} & d,p1,p2 is_product_of a,b ) );

theorem Th41: :: CAT_8:41

OrdC 1 is with_binary_products

proof end;

registration

cluster non empty associative composable with_identities with_binary_products for CategoryStr ;

correctness
existence
ex b₁ being category st
( b₁ is with_binary_products & not b₁ is empty );
by Th41;

end;

definition

let C be with_binary_products category;
let c1, c2 be Object of C;

mode categorical_product of c1,c2 -> triple object means :Def12: :: CAT_8:def 12
ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st
( it = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 );

correctness
existence
ex b₁ being triple object ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st
( b₁ = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 );

proof end;

end;

:: deftheorem Def12 defines categorical_product CAT_8:def 12 :
for C being with_binary_products category
for c1, c2 being Object of C
for b₄ being triple object holds
( b₄ is categorical_product of c1,c2 iff ex d being Object of C ex p1 being Morphism of d,c1 ex p2 being Morphism of d,c2 st
( b₄ = [d,p1,p2] & Hom (d,c1) <> {} & Hom (d,c2) <> {} & d,p1,p2 is_product_of c1,c2 ) );

definition

let C be with_binary_products category;
let c1, c2 be Object of C;

func c1 [x] c2 -> Object of C equals :: CAT_8:def 13
the categorical_product of c1,c2 `1_3 ;

correctness
coherence
the categorical_product of c1,c2 `1_3 is Object of C;

proof end;

end;

:: deftheorem defines [x] CAT_8:def 13 :
for C being with_binary_products category
for c1, c2 being Object of C holds c1 [x] c2 = the categorical_product of c1,c2 `1_3 ;

definition

let C be with_binary_products category;
let c1, c2 be Object of C;

func pr1 (c1,c2) -> Morphism of c1 [x] c2,c1 equals :: CAT_8:def 14
the categorical_product of c1,c2 `2_3 ;

correctness
coherence
the categorical_product of c1,c2 `2_3 is Morphism of c1 [x] c2,c1;

proof end;

func pr2 (c1,c2) -> Morphism of c1 [x] c2,c2 equals :: CAT_8:def 15
the categorical_product of c1,c2 `3_3 ;

correctness
coherence
the categorical_product of c1,c2 `3_3 is Morphism of c1 [x] c2,c2;

proof end;

end;

:: deftheorem defines pr1 CAT_8:def 14 :
for C being with_binary_products category
for c1, c2 being Object of C holds pr1 (c1,c2) = the categorical_product of c1,c2 `2_3 ;

:: deftheorem defines pr2 CAT_8:def 15 :
for C being with_binary_products category
for c1, c2 being Object of C holds pr2 (c1,c2) = the categorical_product of c1,c2 `3_3 ;

theorem Th42: :: CAT_8:42

for C being with_binary_products category
for a, b being Object of C holds
( a [x] b, pr1 (a,b), pr2 (a,b) is_product_of a,b & Hom ((a [x] b),a) <> {} & Hom ((a [x] b),b) <> {} )

proof end;

theorem :: CAT_8:43

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

proof end;

theorem Th44: :: CAT_8:44

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

proof end;

definition

let C be with_binary_products category;
let a, b, c, d be Object of C;
let f be Morphism of a,b;
assume A1: Hom (a,b) <> {} ;
let g be Morphism of c,d;
assume A2: Hom (c,d) <> {} ;

func f [x] g -> Morphism of a [x] c,b [x] d means :Def16: :: CAT_8:def 16
( f * (pr1 (a,c)) = (pr1 (b,d)) * it & g * (pr2 (a,c)) = (pr2 (b,d)) * it );

correctness
existence
ex b₁ being Morphism of a [x] c,b [x] d st
( f * (pr1 (a,c)) = (pr1 (b,d)) * b₁ & g * (pr2 (a,c)) = (pr2 (b,d)) * b₁ );
uniqueness
for b₁, b₂ being Morphism of a [x] c,b [x] d st f * (pr1 (a,c)) = (pr1 (b,d)) * b₁ & g * (pr2 (a,c)) = (pr2 (b,d)) * b₁ & f * (pr1 (a,c)) = (pr1 (b,d)) * b₂ & g * (pr2 (a,c)) = (pr2 (b,d)) * b₂ holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def16 defines [x] CAT_8:def 16 :
for C being with_binary_products category
for a, b, c, d being Object of C
for f being Morphism of a,b st Hom (a,b) <> {} holds
for g being Morphism of c,d st Hom (c,d) <> {} holds
for b₈ being Morphism of a [x] c,b [x] d holds
( b₈ = f [x] g iff ( f * (pr1 (a,c)) = (pr1 (b,d)) * b₈ & g * (pr2 (a,c)) = (pr2 (b,d)) * b₈ ) );

definition

let C1, C2, D be category;
let P1 be Functor of D,C1;
assume P1 is covariant ;
let P2 be Functor of D,C2;
assume P2 is covariant ;

pred D,P1,P2 is_product_of C1,C2 means :Def17: :: CAT_8:def 17
for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant holds
ex H being Functor of D1,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) );

end;

:: deftheorem Def17 defines is_product_of CAT_8:def 17 :
for C1, C2, D being category
for P1 being Functor of D,C1 st P1 is covariant holds
for P2 being Functor of D,C2 st P2 is covariant holds
( D,P1,P2 is_product_of C1,C2 iff for D1 being category
for G1 being Functor of D1,C1
for G2 being Functor of D1,C2 st G1 is covariant & G2 is covariant holds
ex H being Functor of D1,D st
( H is covariant & P1 (*) H = G1 & P2 (*) H = G2 & ( for H1 being Functor of D1,D st H1 is covariant & P1 (*) H1 = G1 & P2 (*) H1 = G2 holds
H = H1 ) ) );

theorem :: CAT_8:45

for C1, C2, A, B being category
for P1 being Functor of A,C1
for P2 being Functor of A,C2
for Q1 being Functor of B,C1
for Q2 being Functor of B,C2 st P1 is covariant & P2 is covariant & Q1 is covariant & Q2 is covariant & A,P1,P2 is_product_of C1,C2 & B,Q1,Q2 is_product_of C1,C2 holds
A ~= B

proof end;

theorem :: CAT_8:46

for C1, C2, D being category
for P1 being Functor of D,C1
for P2 being Functor of D,C2 st P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 holds
D,P2,P1 is_product_of C2,C1

proof end;

notation

let C, C1, C2 be category;
let F1 be Functor of C1,C;
let F2 be Functor of C2,C;
synonym F1 [|x|] F2 for [|F1,F2|];

end;

theorem Th47: :: CAT_8:47

for C1, C2 being category holds (C1 ->OrdC1) [|x|] (C2 ->OrdC1), pr1 ((C1 ->OrdC1),(C2 ->OrdC1)), pr2 ((C1 ->OrdC1),(C2 ->OrdC1)) is_product_of C1,C2

proof end;

definition

let C1, C2 be category;

mode categorical_product of C1,C2 -> triple object means :Def18: :: CAT_8:def 18
ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( it = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 );

correctness
existence
ex b₁ being triple object ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( b₁ = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 );

proof end;

end;

:: deftheorem Def18 defines categorical_product CAT_8:def 18 :
for C1, C2 being category
for b₃ being triple object holds
( b₃ is categorical_product of C1,C2 iff ex D being strict category ex P1 being Functor of D,C1 ex P2 being Functor of D,C2 st
( b₃ = [D,P1,P2] & P1 is covariant & P2 is covariant & D,P1,P2 is_product_of C1,C2 ) );

definition

let C1, C2 be category;

func C1 [x] C2 -> strict category equals :: CAT_8:def 19
the categorical_product of C1,C2 `1_3 ;

correctness
coherence
the categorical_product of C1,C2 `1_3 is strict category;

proof end;

end;

:: deftheorem defines [x] CAT_8:def 19 :
for C1, C2 being category holds C1 [x] C2 = the categorical_product of C1,C2 `1_3 ;

definition

let C1, C2 be category;

func pr1 (C1,C2) -> Functor of (C1 [x] C2),C1 equals :: CAT_8:def 20
the categorical_product of C1,C2 `2_3 ;

correctness
coherence
the categorical_product of C1,C2 `2_3 is Functor of (C1 [x] C2),C1;

proof end;

func pr2 (C1,C2) -> Functor of (C1 [x] C2),C2 equals :: CAT_8:def 21
the categorical_product of C1,C2 `3_3 ;

correctness
coherence
the categorical_product of C1,C2 `3_3 is Functor of (C1 [x] C2),C2;

proof end;

end;

:: deftheorem defines pr1 CAT_8:def 20 :
for C1, C2 being category holds pr1 (C1,C2) = the categorical_product of C1,C2 `2_3 ;

:: deftheorem defines pr2 CAT_8:def 21 :
for C1, C2 being category holds pr2 (C1,C2) = the categorical_product of C1,C2 `3_3 ;

theorem Th48: :: CAT_8:48

for C1, C2 being category holds C1 [x] C2, pr1 (C1,C2), pr2 (C1,C2) is_product_of C1,C2

proof end;

registration

let C1, C2 be category;

cluster pr1 (C1,C2) -> covariant ;

correctness
coherence
pr1 (C1,C2) is covariant ;

proof end;

cluster pr2 (C1,C2) -> covariant ;

correctness
coherence
pr2 (C1,C2) is covariant ;

proof end;

end;

theorem Th49: :: CAT_8:49

for C1, C2 being category holds
( not C1 [x] C2 is empty iff ( not C1 is empty & not C2 is empty ) )

proof end;

registration

let C1 be empty category;
let C2 be category;

cluster C1 [x] C2 -> empty strict ;

correctness
coherence
C1 [x] C2 is empty ;
by Th49;

end;

registration

let C1 be category;
let C2 be empty category;

cluster C1 [x] C2 -> empty strict ;

correctness
coherence
C1 [x] C2 is empty ;
by Th49;

end;

registration

let C1, C2 be non empty category;

cluster C1 [x] C2 -> non empty strict ;

correctness
coherence
not C1 [x] C2 is empty ;
by Th49;

end;

definition

let C1, C2, D1, D2 be category;
let F1 be Functor of C1,D1;
let F2 be Functor of C2,D2;
assume A1: ( F1 is covariant & F2 is covariant ) ;

func F1 [x] F2 -> Functor of (C1 [x] C2),(D1 [x] D2) means :Def22: :: CAT_8:def 22
( it is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) it & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) it );

correctness
existence
ex b₁ being Functor of (C1 [x] C2),(D1 [x] D2) st
( b₁ is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b₁ & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b₁ );
uniqueness
for b₁, b₂ being Functor of (C1 [x] C2),(D1 [x] D2) st b₁ is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b₁ & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b₁ & b₂ is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b₂ & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b₂ holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def22 defines [x] CAT_8:def 22 :
for C1, C2, D1, D2 being category
for F1 being Functor of C1,D1
for F2 being Functor of C2,D2 st F1 is covariant & F2 is covariant holds
for b₇ being Functor of (C1 [x] C2),(D1 [x] D2) holds
( b₇ = F1 [x] F2 iff ( b₇ is covariant & F1 (*) (pr1 (C1,C2)) = (pr1 (D1,D2)) (*) b₇ & F2 (*) (pr2 (C1,C2)) = (pr2 (D1,D2)) (*) b₇ ) );

theorem Th50: :: CAT_8:50

for A1, A2, B1, B2, C1, C2 being category
for F1 being Functor of A1,B1
for F2 being Functor of A2,B2
for G1 being Functor of B1,C1
for G2 being Functor of B2,C2 st F1 is covariant & G1 is covariant & F2 is covariant & G2 is covariant holds
(G1 [x] G2) (*) (F1 [x] F2) = (G1 (*) F1) [x] (G2 (*) F2)

proof end;

theorem Th51: :: CAT_8:51

for C1, C2 being category holds (id C1) [x] (id C2) = id (C1 [x] C2)

proof end;

notation

let x, y be object ;
synonym KuratowskiPair (x,y) for [x,y];

end;

definition

let C1, C2 be category;
let f1 be morphism of C1;
let f2 be morphism of C2;

func [f1,f2] -> morphism of (C1 [x] C2) means :Def23: :: CAT_8:def 23
( (pr1 (C1,C2)) . it = f1 & (pr2 (C1,C2)) . it = f2 ) if ( not C1 is empty & not C2 is empty )
otherwise it = the morphism of (C1 [x] C2);

correctness
consistency
for b₁ being morphism of (C1 [x] C2) holds verum;
existence
( ( for b₁ being morphism of (C1 [x] C2) holds verum ) & ( not C1 is empty & not C2 is empty implies ex b₁ being morphism of (C1 [x] C2) st
( (pr1 (C1,C2)) . b₁ = f1 & (pr2 (C1,C2)) . b₁ = f2 ) ) & ( ( C1 is empty or C2 is empty ) implies ex b₁ being morphism of (C1 [x] C2) st b₁ = the morphism of (C1 [x] C2) ) );
uniqueness
for b₁, b₂ being morphism of (C1 [x] C2) holds
( ( not C1 is empty & not C2 is empty & (pr1 (C1,C2)) . b₁ = f1 & (pr2 (C1,C2)) . b₁ = f2 & (pr1 (C1,C2)) . b₂ = f1 & (pr2 (C1,C2)) . b₂ = f2 implies b₁ = b₂ ) & ( ( C1 is empty or C2 is empty ) & b₁ = the morphism of (C1 [x] C2) & b₂ = the morphism of (C1 [x] C2) implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def23 defines [ CAT_8:def 23 :
for C1, C2 being category
for f1 being morphism of C1
for f2 being morphism of C2
for b₅ being morphism of (C1 [x] C2) holds
( ( not C1 is empty & not C2 is empty implies ( b₅ = [f1,f2] iff ( (pr1 (C1,C2)) . b₅ = f1 & (pr2 (C1,C2)) . b₅ = f2 ) ) ) & ( ( C1 is empty or C2 is empty ) implies ( b₅ = [f1,f2] iff b₅ = the morphism of (C1 [x] C2) ) ) );

theorem Th52: :: CAT_8:52

for C1, C2 being category
for f being morphism of (C1 [x] C2) ex f1 being morphism of C1 ex f2 being morphism of C2 st f = [f1,f2]

proof end;

Lm2: for C1, C2 being non empty category
for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds
[f1,f2] |> [g1,g2]

proof end;

theorem Th53: :: CAT_8:53

for C1, C2 being non empty category
for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 st [f1,f2] = [g1,g2] holds
( f1 = g1 & f2 = g2 )

proof end;

theorem Th54: :: CAT_8:54

for C1, C2 being category
for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 holds
( [f1,f2] |> [g1,g2] iff ( f1 |> g1 & f2 |> g2 ) )

proof end;

theorem Th55: :: CAT_8:55

for C1, C2 being category
for f1, g1 being morphism of C1
for f2, g2 being morphism of C2 st f1 |> g1 & f2 |> g2 holds
[f1,f2] (*) [g1,g2] = [(f1 (*) g1),(f2 (*) g2)]

proof end;

theorem Th56: :: CAT_8:56

for C1, C2 being category
for f1 being morphism of C1
for f2 being morphism of C2
for f being morphism of (C1 [x] C2) st f = [f1,f2] & not C1 is empty & not C2 is empty holds
( f is identity iff ( f1 is identity & f2 is identity ) )

proof end;

theorem Th57: :: CAT_8:57

for C1, C2 being non empty category
for D1, D2 being category
for F1 being Functor of C1,D1
for F2 being Functor of C2,D2
for c1 being morphism of C1
for c2 being morphism of C2 st F1 is covariant & F2 is covariant holds
(F1 [x] F2) . [c1,c2] = [(F1 . c1),(F2 . c2)]

proof end;

definition

let C1, C2 be category;
let F1, F2 be Functor of C1,C2;
let T be Functor of C1,C2;

pred T is_natural_transformation_of F1,F2 means :: CAT_8:def 24
for f1, f2 being morphism of C1 st f1 |> f2 holds
( T . f1 |> F1 . f2 & F2 . f1 |> T . f2 & T . (f1 (*) f2) = (T . f1) (*) (F1 . f2) & T . (f1 (*) f2) = (F2 . f1) (*) (T . f2) );

end;

:: deftheorem defines is_natural_transformation_of CAT_8:def 24 :
for C1, C2 being category
for F1, F2, T being Functor of C1,C2 holds
( T is_natural_transformation_of F1,F2 iff for f1, f2 being morphism of C1 st f1 |> f2 holds
( T . f1 |> F1 . f2 & F2 . f1 |> T . f2 & T . (f1 (*) f2) = (T . f1) (*) (F1 . f2) & T . (f1 (*) f2) = (F2 . f1) (*) (T . f2) ) );

theorem Th58: :: CAT_8:58

for C1, C2 being category
for F1, F2, T being Functor of C1,C2 st F1 is covariant & F2 is covariant holds
( T is_natural_transformation_of F1,F2 iff for f, f1, f2 being morphism of C1 st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( T . f1 |> F1 . f & F2 . f |> T . f2 & T . f = (T . f1) (*) (F1 . f) & T . f = (F2 . f) (*) (T . f2) ) )

proof end;

theorem :: CAT_8:59

for C1, C2 being non empty category
for F1, F2 being covariant Functor of C1,C2
for T being Function of (Ob C1),(Mor C2) holds
( ex T1 being Functor of C1,C2 st
( T = T1 | (Ob C1) & T1 is_natural_transformation_of F1,F2 ) iff ( ( for a being Object of C1 holds T . a in Hom ((F1 . a),(F2 . a)) ) & ( for a1, a2 being Object of C1
for f being Morphism of a1,a2 st Hom (a1,a2) <> {} holds
(T . a2) (*) (F1 . f) = (F2 . f) (*) (T . a1) ) ) )

proof end;

theorem :: CAT_8:60

for C, D being Category
for F1, F2 being Functor of C,D
for G1, G2, T being Functor of (alter C),(alter D) st F1 = G1 & F2 = G2 & T is_natural_transformation_of G1,G2 holds
(IdMap C) * T is natural_transformation of F1,F2

proof end;

definition

let C, D be category;
let F1, F2 be Functor of C,D;

pred F1 is_naturally_transformable_to F2 means :: CAT_8:def 25
ex T being Functor of C,D st T is_natural_transformation_of F1,F2;

end;

:: deftheorem defines is_naturally_transformable_to CAT_8:def 25 :
for C, D being category
for F1, F2 being Functor of C,D holds
( F1 is_naturally_transformable_to F2 iff ex T being Functor of C,D st T is_natural_transformation_of F1,F2 );

definition

let C, D be category;
let F1, F2 be Functor of C,D;
assume A1: F1 is_naturally_transformable_to F2 ;

mode natural_transformation of F1,F2 -> Functor of C,D means :Def26: :: CAT_8:def 26
it is_natural_transformation_of F1,F2;

correctness
existence
ex b₁ being Functor of C,D st b₁ is_natural_transformation_of F1,F2;
by A1;

end;

:: deftheorem Def26 defines natural_transformation CAT_8:def 26 :
for C, D being category
for F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F2 holds
for b₅ being Functor of C,D holds
( b₅ is natural_transformation of F1,F2 iff b₅ is_natural_transformation_of F1,F2 );

theorem Th61: :: CAT_8:61

for C, D being category
for F being Functor of C,D st F is covariant holds
F is_natural_transformation_of F,F

proof end;

Lm3: for C, D being category
for F, F1, F2 being Functor of C,D
for T1 being natural_transformation of F1,F
for T2 being natural_transformation of F,F2 st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) )

proof end;

definition

let C, D be category;
let F, F1, F2 be Functor of C,D;
assume that
A1: ( F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 ) and
A2: ( F is covariant & F1 is covariant & F2 is covariant ) ;
let T1 be natural_transformation of F1,F;
let T2 be natural_transformation of F,F2;

func T2 `*` T1 -> natural_transformation of F1,F2 means :Def27: :: CAT_8:def 27
for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
it . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1);

existence
ex b₁ being natural_transformation of F1,F2 st
for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
b₁ . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1)

proof end;

uniqueness
for b₁, b₂ being natural_transformation of F1,F2 st ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
b₁ . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
b₂ . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def27 defines `*` CAT_8:def 27 :
for C, D being category
for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
for T1 being natural_transformation of F1,F
for T2 being natural_transformation of F,F2
for b₈ being natural_transformation of F1,F2 holds
( b₈ = T2 `*` T1 iff for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
b₈ . f = ((T2 . f2) (*) (F . f)) (*) (T1 . f1) );

theorem Th62: :: CAT_8:62

for C, D being category
for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
F1 is_naturally_transformable_to F2

proof end;

Lm4: for C1, C2 being category
for X being set st not C1 is empty & C2 is empty & X = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } holds
( X = {} & { [[x2,x1],x3] where x1, x2, x3 is Element of X : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {} )

proof end;

Lm5: for C1, C2 being category
for X1, X2 being set st C1 is empty & X1 = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & X2 = [[{},{}],{}] holds
( X1 = {X2} & { [[x2,x1],x3] where x1, x2, x3 is Element of X1 : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {[[X2,X2],X2]} )

proof end;

definition

let C1, C2 be category;

func Functors (C1,C2) -> strict category means :Def28: :: CAT_8:def 28
( the carrier of it = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of it = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of it : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } );

existence
ex b₁ being strict category st
( the carrier of b₁ = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b₁ = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b₁ : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )

proof end;

uniqueness
for b₁, b₂ being strict category st the carrier of b₁ = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b₁ = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b₁ : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } & the carrier of b₂ = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b₂ = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b₂ : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } holds
b₁ = b₂ ;

end;

:: deftheorem Def28 defines Functors CAT_8:def 28 :
for C1, C2 being category
for b₃ being strict category holds
( b₃ = Functors (C1,C2) iff ( the carrier of b₃ = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b₃ = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b₃ : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ) );

registration

let C1 be non empty category;
let C2 be empty category;

cluster Functors (C1,C2) -> empty strict ;

correctness
coherence
Functors (C1,C2) is empty ;

proof end;

end;

registration

let C1 be empty category;
let C2 be category;

cluster Functors (C1,C2) -> non empty trivial strict ;

correctness
coherence
( not Functors (C1,C2) is empty & Functors (C1,C2) is trivial );

proof end;

end;

registration

let C1, C2 be non empty category;

cluster Functors (C1,C2) -> non empty strict ;

correctness
coherence
not Functors (C1,C2) is empty ;

proof end;

end;

theorem Th63: :: CAT_8:63

for C1, C2 being non empty category
for f1, f2 being morphism of (Functors (C1,C2)) holds
( f1 |> f2 iff ex F, F1, F2 being covariant Functor of C1,C2 ex T1 being natural_transformation of F1,F ex T2 being natural_transformation of F,F2 st
( f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1 (*) f2 = [[F1,F2],(T2 `*` T1)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds
( T2 . g2 |> T1 . g1 & (T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) ) )

proof end;

theorem Th64: :: CAT_8:64

for C1, C2 being non empty category
for f being morphism of (Functors (C1,C2)) holds
( f is identity iff ex F being covariant Functor of C1,C2 st f = [[F,F],F] )

proof end;

theorem Th65: :: CAT_8:65

for C1, C2 being non empty category
for f being morphism of (Functors (C1,C2)) ex F1, F2 being covariant Functor of C1,C2 ex T being natural_transformation of F1,F2 st
( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )

proof end;

definition

let C be non empty with_binary_products category;
let a, b, c be Object of C;
let e be Morphism of c [x] a,b;
assume Hom ((c [x] a),b) <> {} ;

pred c,e is_exponent_of a,b means :Def29: :: CAT_8:def 29
for d being Object of C
for f being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds
( Hom (d,c) <> {} & ex h being Morphism of d,c st
( f = e * (h [x] (id- a)) & ( for h1 being Morphism of d,c st f = e * (h1 [x] (id- a)) holds
h = h1 ) ) );

end;

:: deftheorem Def29 defines is_exponent_of CAT_8:def 29 :
for C being non empty with_binary_products category
for a, b, c being Object of C
for e being Morphism of c [x] a,b st Hom ((c [x] a),b) <> {} holds
( c,e is_exponent_of a,b iff for d being Object of C
for f being Morphism of d [x] a,b st Hom ((d [x] a),b) <> {} holds
( Hom (d,c) <> {} & ex h being Morphism of d,c st
( f = e * (h [x] (id- a)) & ( for h1 being Morphism of d,c st f = e * (h1 [x] (id- a)) holds
h = h1 ) ) ) );

theorem Th66: :: CAT_8:66

for C being with_binary_products category
for a1, a2, b1, b2, c1, c2 being Object of C
for f1 being Morphism of a1,b1
for f2 being Morphism of a2,b2
for g1 being Morphism of b1,c1
for g2 being Morphism of b2,c2 st Hom (a1,b1) <> {} & Hom (b1,c1) <> {} & Hom (a2,b2) <> {} & Hom (b2,c2) <> {} holds
(g1 [x] g2) * (f1 [x] f2) = (g1 * f1) [x] (g2 * f2)

proof end;

theorem Th67: :: CAT_8:67

for C being non empty with_binary_products category
for a, b being Object of C holds (id- a) [x] (id- b) = id- (a [x] b)

proof end;

theorem :: CAT_8:68

for C being non empty with_binary_products category
for a, b, c1, c2 being Object of C
for e1 being Morphism of c1 [x] a,b
for e2 being Morphism of c2 [x] a,b st Hom ((c1 [x] a),b) <> {} & Hom ((c2 [x] a),b) <> {} & c1,e1 is_exponent_of a,b & c2,e2 is_exponent_of a,b holds
c1,c2 are_isomorphic

proof end;

definition

let C be non empty with_binary_products category;

attr C is with_exponential_objects means :Def30: :: CAT_8:def 30
for a, b being Object of C ex c being Object of C ex e being Morphism of c [x] a,b st
( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

end;

:: deftheorem Def30 defines with_exponential_objects CAT_8:def 30 :
for C being non empty with_binary_products category holds
( C is with_exponential_objects iff for a, b being Object of C ex c being Object of C ex e being Morphism of c [x] a,b st
( Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b ) );

registration

cluster OrdC 1 -> with_binary_products ;

correctness
coherence
OrdC 1 is with_binary_products ;
by Th41;

end;

theorem Th69: :: CAT_8:69

OrdC 1 is with_exponential_objects

proof end;

registration

cluster non empty associative composable with_identities with_binary_products with_exponential_objects for CategoryStr ;

correctness
existence
ex b₁ being non empty with_binary_products category st b₁ is with_exponential_objects ;
by Th69;

end;

definition

let C be non empty with_binary_products with_exponential_objects category;
let a, b be Object of C;

mode categorical_exponent of a,b -> pair object means :Def31: :: CAT_8:def 31
ex c being Object of C ex e being Morphism of c [x] a,b st
( it = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

correctness
existence
ex b₁ being pair object ex c being Object of C ex e being Morphism of c [x] a,b st
( b₁ = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b );

proof end;

end;

:: deftheorem Def31 defines categorical_exponent CAT_8:def 31 :
for C being non empty with_binary_products with_exponential_objects category
for a, b being Object of C
for b₄ being pair object holds
( b₄ is categorical_exponent of a,b iff ex c being Object of C ex e being Morphism of c [x] a,b st
( b₄ = [c,e] & Hom ((c [x] a),b) <> {} & c,e is_exponent_of a,b ) );

definition

let C be non empty with_binary_products with_exponential_objects category;
let a, b be Object of C;

func b |^ a -> Object of C equals :: CAT_8:def 32
the categorical_exponent of a,b `1 ;

correctness
coherence
the categorical_exponent of a,b `1 is Object of C;

proof end;

end;

:: deftheorem defines |^ CAT_8:def 32 :
for C being non empty with_binary_products with_exponential_objects category
for a, b being Object of C holds b |^ a = the categorical_exponent of a,b `1 ;

definition

let C be non empty with_binary_products with_exponential_objects category;
let a, b be Object of C;

func eval (a,b) -> Morphism of (b |^ a) [x] a,b equals :: CAT_8:def 33
the categorical_exponent of a,b `2 ;

correctness
coherence
the categorical_exponent of a,b `2 is Morphism of (b |^ a) [x] a,b;

proof end;

end;

:: deftheorem defines eval CAT_8:def 33 :
for C being non empty with_binary_products with_exponential_objects category
for a, b being Object of C holds eval (a,b) = the categorical_exponent of a,b `2 ;

theorem Th70: :: CAT_8:70

for C being non empty with_binary_products with_exponential_objects category
for a, b being Object of C holds
( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b )

proof end;

theorem :: CAT_8:71

for C being non empty with_binary_products with_exponential_objects category
for a, b, c being Object of C st Hom ((c [x] a),b) <> {} holds
ex L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) st
( ( for f being Morphism of c [x] a,b
for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective )

proof end;

definition

let A, B, C be category;
let E be Functor of (C [x] A),B;
assume E is covariant ;

pred C,E is_exponent_of A,B means :Def34: :: CAT_8:def 34
for D being category
for F being Functor of (D [x] A),B st F is covariant holds
ex H being Functor of D,C st
( H is covariant & F = E (*) (H [x] (id A)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id A)) holds
H = H1 ) );

end;

:: deftheorem Def34 defines is_exponent_of CAT_8:def 34 :
for A, B, C being category
for E being Functor of (C [x] A),B st E is covariant holds
( C,E is_exponent_of A,B iff for D being category
for F being Functor of (D [x] A),B st F is covariant holds
ex H being Functor of D,C st
( H is covariant & F = E (*) (H [x] (id A)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id A)) holds
H = H1 ) ) );

Lm6: for C, C1, C2 being non empty category st C = Functors (C1,C2) holds
ex E being Functor of (C [x] C1),C2 st
( E is covariant & ( for D being category
for F being Functor of (D [x] C1),C2 st F is covariant holds
ex H being Functor of D,C st
( H is covariant & F = E (*) (H [x] (id C1)) & ( for H1 being Functor of D,C st H1 is covariant & F = E (*) (H1 [x] (id C1)) holds
H = H1 ) ) ) )

proof end;

Lm7: for C1 being non empty category
for C2 being empty category
for E being Functor of ((OrdC 0) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 0,E is_exponent_of C1,C2

proof end;

Lm8: for C1 being empty category
for C2 being category
for E being Functor of ((OrdC 1) [x] C1),C2 st E = OrdC0-> C2 holds
OrdC 1,E is_exponent_of C1,C2

proof end;

definition

let C1, C2 be category;

mode categorical_exponent of C1,C2 -> pair object means :Def35: :: CAT_8:def 35
ex C being category ex E being Functor of (C [x] C1),C2 st
( it = [C,E] & E is covariant & C,E is_exponent_of C1,C2 );

existence
ex b₁ being pair object ex C being category ex E being Functor of (C [x] C1),C2 st
( b₁ = [C,E] & E is covariant & C,E is_exponent_of C1,C2 )

proof end;

end;

:: deftheorem Def35 defines categorical_exponent CAT_8:def 35 :
for C1, C2 being category
for b₃ being pair object holds
( b₃ is categorical_exponent of C1,C2 iff ex C being category ex E being Functor of (C [x] C1),C2 st
( b₃ = [C,E] & E is covariant & C,E is_exponent_of C1,C2 ) );

definition

let C1, C2 be category;

func C2 |^ C1 -> category equals :: CAT_8:def 36
the categorical_exponent of C1,C2 `1 ;

correctness
coherence
the categorical_exponent of C1,C2 `1 is category;

proof end;

end;

:: deftheorem defines |^ CAT_8:def 36 :
for C1, C2 being category holds C2 |^ C1 = the categorical_exponent of C1,C2 `1 ;

definition

let C1, C2 be category;

func eval (C1,C2) -> Functor of ((C2 |^ C1) [x] C1),C2 equals :: CAT_8:def 37
the categorical_exponent of C1,C2 `2 ;

correctness
coherence
the categorical_exponent of C1,C2 `2 is Functor of ((C2 |^ C1) [x] C1),C2;

proof end;

end;

:: deftheorem defines eval CAT_8:def 37 :
for C1, C2 being category holds eval (C1,C2) = the categorical_exponent of C1,C2 `2 ;

theorem Th72: :: CAT_8:72

for C1, C2 being category holds C2 |^ C1, eval (C1,C2) is_exponent_of C1,C2

proof end;

theorem Th73: :: CAT_8:73

for A, B, C1, C2 being category
for E1 being Functor of (C1 [x] A),B
for E2 being Functor of (C2 [x] A),B st E1 is covariant & E2 is covariant & C1,E1 is_exponent_of A,B & C2,E2 is_exponent_of A,B holds
C1 ~= C2

proof end;

registration

let C1, C2 be category;

cluster eval (C1,C2) -> covariant ;

correctness
coherence
eval (C1,C2) is covariant ;

proof end;

end;

registration

let C1 be non empty category;
let C2 be empty category;

cluster C2 |^ C1 -> empty ;

correctness
coherence
C2 |^ C1 is empty ;

proof end;

end;

registration

let C1 be empty category;
let C2 be category;

cluster C2 |^ C1 -> non empty trivial ;

correctness
coherence
( not C2 |^ C1 is empty & C2 |^ C1 is trivial );

proof end;

end;

registration

let C1, C2 be non empty category;

cluster C2 |^ C1 -> non empty ;

correctness
coherence
not C2 |^ C1 is empty ;

proof end;

end;

theorem :: CAT_8:74

for C1, C2 being category holds Functors (C1,C2) ~= C2 |^ C1

proof end;