:: Category Ens
:: by Czes{\l}aw Byli\'nski
::
:: Received August 1, 1991
:: Copyright (c) 1991 Association of Mizar Users

begin

definition

let V be non empty set ;
func Funcs V -> set equals :: ENS_1:def 1
union { (Funcs (A,B)) where A, B is Element of V : verum } ;
coherence
union { (Funcs (A,B)) where A, B is Element of V : verum } is set ;

end;

:: deftheorem defines Funcs ENS_1:def 1 :
for V being non empty set holds Funcs V = union { (Funcs (A,B)) where A, B is Element of V : verum } ;

registration

let V be non empty set ;
cluster Funcs V -> functional non empty ;
coherence
( Funcs V is functional & not Funcs V is empty )

proof end;

end;

theorem Th1: :: ENS_1:1

for V being non empty set
for f being set holds
( f in Funcs V iff ex A, B being Element of V st
( ( B = {} implies A = {} ) & f is Function of A,B ) )

proof end;

theorem :: ENS_1:2

for V being non empty set
for A, B being Element of V holds Funcs (A,B) c= Funcs V

proof end;

theorem Th3: :: ENS_1:3

for V being non empty set
for W being non empty Subset of V holds Funcs W c= Funcs V

proof end;

definition

let V be non empty set ;
func Maps V -> set equals :: ENS_1:def 2
{ [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;
coherence
{ [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } is set ;

end;

:: deftheorem defines Maps ENS_1:def 2 :
for V being non empty set holds Maps V = { [[A,B],f] where A, B is Element of V, f is Element of Funcs V : ( ( B = {} implies A = {} ) & f is Function of A,B ) } ;

registration

let V be non empty set ;
cluster Maps V -> non empty ;
coherence
not Maps V is empty

proof end;

end;

theorem Th4: :: ENS_1:4

for V being non empty set
for m being Element of Maps V ex f being Element of Funcs V ex A, B being Element of V st
( m = [[A,B],f] & ( B = {} implies A = {} ) & f is Function of A,B )

proof end;

theorem Th5: :: ENS_1:5

for V being non empty set
for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps V

proof end;

theorem :: ENS_1:6

for V being non empty set holds Maps V c= [:[:V,V:],(Funcs V):]

proof end;

theorem Th7: :: ENS_1:7

for V being non empty set
for W being non empty Subset of V holds Maps W c= Maps V

proof end;

Lm1: for x1, y1, x2, y2, x3, y3 being set st [[x1,x2],x3] = [[y1,y2],y3] holds
( x1 = y1 & x2 = y2 )

proof end;

registration

let V be non empty set ;
let m be Element of Maps V;
cluster m `2 -> Relation-like Function-like ;
coherence
( m `2 is Function-like & m `2 is Relation-like )

proof end;

end;

definition

let V be non empty set ;
let m be Element of Maps V;
canceled;
func dom m -> Element of V equals :: ENS_1:def 4
(m `1) `1 ;
coherence
(m `1) `1 is Element of V

proof end;

func cod m -> Element of V equals :: ENS_1:def 5
(m `1) `2 ;
coherence
(m `1) `2 is Element of V

proof end;

end;

:: deftheorem ENS_1:def 3 :
canceled;

:: deftheorem defines dom ENS_1:def 4 :
for V being non empty set
for m being Element of Maps V holds dom m = (m `1) `1 ;

:: deftheorem defines cod ENS_1:def 5 :
for V being non empty set
for m being Element of Maps V holds cod m = (m `1) `2 ;

theorem Th8: :: ENS_1:8

for V being non empty set
for m being Element of Maps V holds m = [[(dom m),(cod m)],(m `2)]

proof end;

Lm2: for V being non empty set
for m, m9 being Element of Maps V st m `2 = m9 `2 & dom m = dom m9 & cod m = cod m9 holds
m = m9

proof end;

theorem Th9: :: ENS_1:9

for V being non empty set
for m being Element of Maps V holds
( ( cod m <> {} or dom m = {} ) & m `2 is Function of (dom m),(cod m) )

proof end;

Lm3: for V being non empty set
for m being Element of Maps V holds
( dom (m `2) = dom m & rng (m `2) c= cod m )

proof end;

theorem Th10: :: ENS_1:10

for V being non empty set
for f being Function
for A, B being set st [[A,B],f] in Maps V holds
( ( B = {} implies A = {} ) & f is Function of A,B )

proof end;

definition

let V be non empty set ;
let A be Element of V;
func id$ A -> Element of Maps V equals :: ENS_1:def 6
[[A,A],(id A)];
coherence
[[A,A],(id A)] is Element of Maps V by Th5;

end;

:: deftheorem defines id$ ENS_1:def 6 :
for V being non empty set
for A being Element of V holds id$ A = [[A,A],(id A)];

theorem Th11: :: ENS_1:11

for V being non empty set
for A being Element of V holds
( (id$ A) `2 = id A & dom (id$ A) = A & cod (id$ A) = A )

proof end;

definition

let V be non empty set ;
let m1, m2 be Element of Maps V;
assume A1: cod m1 = dom m2 ;
func m2 * m1 -> Element of Maps V equals :Def7: :: ENS_1:def 7
[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];
coherence
[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of Maps V

proof end;

end;

:: deftheorem Def7 defines * ENS_1:def 7 :
for V being non empty set
for m1, m2 being Element of Maps V st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

theorem Th12: :: ENS_1:12

for V being non empty set
for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )

proof end;

theorem Th13: :: ENS_1:13

for V being non empty set
for m2, m1, m3 being Element of Maps V st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1

proof end;

theorem Th14: :: ENS_1:14

for V being non empty set
for m being Element of Maps V holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )

proof end;

definition

let V be non empty set ;
let A, B be Element of V;
func Maps (A,B) -> set equals :: ENS_1:def 8
{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;
correctness
coherence
{ [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } is set ;
;

end;

:: deftheorem defines Maps ENS_1:def 8 :
for V being non empty set
for A, B being Element of V holds Maps (A,B) = { [[A,B],f] where f is Element of Funcs V : [[A,B],f] in Maps V } ;

theorem Th15: :: ENS_1:15

for V being non empty set
for A, B being Element of V
for f being Function of A,B st ( B = {} implies A = {} ) holds
[[A,B],f] in Maps (A,B)

proof end;

theorem Th16: :: ENS_1:16

for V being non empty set
for A, B being Element of V
for m being Element of Maps V st m in Maps (A,B) holds
m = [[A,B],(m `2)]

proof end;

theorem Th17: :: ENS_1:17

for V being non empty set
for A, B being Element of V holds Maps (A,B) c= Maps V

proof end;

Lm4: for V being non empty set
for A, B being Element of V
for f being Function st [[A,B],f] in Maps (A,B) holds
( ( B = {} implies A = {} ) & f is Function of A,B )

proof end;

theorem :: ENS_1:18

for V being non empty set holds Maps V = union { (Maps (A,B)) where A, B is Element of V : verum }

proof end;

theorem Th19: :: ENS_1:19

for V being non empty set
for A, B being Element of V
for m being Element of Maps V holds
( m in Maps (A,B) iff ( dom m = A & cod m = B ) )

proof end;

theorem Th20: :: ENS_1:20

for V being non empty set
for A, B being Element of V
for m being Element of Maps V st m in Maps (A,B) holds
m `2 in Funcs (A,B)

proof end;

Lm5: for V being non empty set
for W being non empty Subset of V
for A, B being Element of W
for A9, B9 being Element of V st A = A9 & B = B9 holds
Maps (A,B) = Maps (A9,B9)

proof end;

definition

let V be non empty set ;
let m be Element of Maps V;
attr m is surjective means :: ENS_1:def 9
rng (m `2) = cod m;

end;

:: deftheorem defines surjective ENS_1:def 9 :
for V being non empty set
for m being Element of Maps V holds
( m is surjective iff rng (m `2) = cod m );

begin

definition

let V be non empty set ;
func fDom V -> Function of (Maps V),V means :Def10: :: ENS_1:def 10
for m being Element of Maps V holds it . m = dom m;
existence
ex b₁ being Function of (Maps V),V st
for m being Element of Maps V holds b₁ . m = dom m

proof end;

uniqueness
for b₁, b₂ being Function of (Maps V),V st ( for m being Element of Maps V holds b₁ . m = dom m ) & ( for m being Element of Maps V holds b₂ . m = dom m ) holds
b₁ = b₂

proof end;

func fCod V -> Function of (Maps V),V means :Def11: :: ENS_1:def 11
for m being Element of Maps V holds it . m = cod m;
existence
ex b₁ being Function of (Maps V),V st
for m being Element of Maps V holds b₁ . m = cod m

proof end;

uniqueness
for b₁, b₂ being Function of (Maps V),V st ( for m being Element of Maps V holds b₁ . m = cod m ) & ( for m being Element of Maps V holds b₂ . m = cod m ) holds
b₁ = b₂

proof end;

func fComp V -> PartFunc of [:(Maps V),(Maps V):],(Maps V) means :Def12: :: ENS_1:def 12
( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom it iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
it . [m2,m1] = m2 * m1 ) );
existence
ex b₁ being PartFunc of [:(Maps V),(Maps V):],(Maps V) st
( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₁ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₁ . [m2,m1] = m2 * m1 ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of [:(Maps V),(Maps V):],(Maps V) st ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₁ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₁ . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₂ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₂ . [m2,m1] = m2 * m1 ) holds
b₁ = b₂

proof end;

func fId V -> Function of V,(Maps V) means :Def13: :: ENS_1:def 13
for A being Element of V holds it . A = id$ A;
existence
ex b₁ being Function of V,(Maps V) st
for A being Element of V holds b₁ . A = id$ A

proof end;

uniqueness
for b₁, b₂ being Function of V,(Maps V) st ( for A being Element of V holds b₁ . A = id$ A ) & ( for A being Element of V holds b₂ . A = id$ A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines fDom ENS_1:def 10 :
for V being non empty set
for b₂ being Function of (Maps V),V holds
( b₂ = fDom V iff for m being Element of Maps V holds b₂ . m = dom m );

:: deftheorem Def11 defines fCod ENS_1:def 11 :
for V being non empty set
for b₂ being Function of (Maps V),V holds
( b₂ = fCod V iff for m being Element of Maps V holds b₂ . m = cod m );

:: deftheorem Def12 defines fComp ENS_1:def 12 :
for V being non empty set
for b₂ being PartFunc of [:(Maps V),(Maps V):],(Maps V) holds
( b₂ = fComp V iff ( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b₂ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b₂ . [m2,m1] = m2 * m1 ) ) );

:: deftheorem Def13 defines fId ENS_1:def 13 :
for V being non empty set
for b₂ being Function of V,(Maps V) holds
( b₂ = fId V iff for A being Element of V holds b₂ . A = id$ A );

definition

let V be non empty set ;
func Ens V -> CatStr equals :: ENS_1:def 14
CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #);
coherence
CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #) is CatStr ;

end;

:: deftheorem defines Ens ENS_1:def 14 :
for V being non empty set holds Ens V = CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #);

theorem Th21: :: ENS_1:21

for V being non empty set holds CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V),(fId V) #) is Category

proof end;

registration

let V be non empty set ;
cluster Ens V -> non empty non void strict Category-like ;
coherence
( Ens V is strict & Ens V is Category-like & not Ens V is void & not Ens V is empty ) by Th21;

end;

theorem :: ENS_1:22

for V being non empty set
for A being Element of V holds A is Object of (Ens V) ;

definition

let V be non empty set ;
let A be Element of V;
func @ A -> Object of (Ens V) equals :: ENS_1:def 15
A;
coherence
A is Object of (Ens V) ;

end;

:: deftheorem defines @ ENS_1:def 15 :
for V being non empty set
for A being Element of V holds @ A = A;

theorem :: ENS_1:23

for V being non empty set
for a being Object of (Ens V) holds a is Element of V ;

definition

let V be non empty set ;
let a be Object of (Ens V);
func @ a -> Element of V equals :: ENS_1:def 16
a;
coherence
a is Element of V ;

end;

:: deftheorem defines @ ENS_1:def 16 :
for V being non empty set
for a being Object of (Ens V) holds @ a = a;

theorem :: ENS_1:24

for V being non empty set
for m being Element of Maps V holds m is Morphism of (Ens V) ;

definition

let V be non empty set ;
let m be Element of Maps V;
func @ m -> Morphism of (Ens V) equals :: ENS_1:def 17
m;
coherence
m is Morphism of (Ens V) ;

end;

:: deftheorem defines @ ENS_1:def 17 :
for V being non empty set
for m being Element of Maps V holds @ m = m;

theorem :: ENS_1:25

for V being non empty set
for f being Morphism of (Ens V) holds f is Element of Maps V ;

definition

let V be non empty set ;
let f be Morphism of (Ens V);
func @ f -> Element of Maps V equals :: ENS_1:def 18
f;
coherence
f is Element of Maps V ;

end;

:: deftheorem defines @ ENS_1:def 18 :
for V being non empty set
for f being Morphism of (Ens V) holds @ f = f;

theorem :: ENS_1:26

for V being non empty set
for f being Morphism of (Ens V) holds
( dom f = dom (@ f) & cod f = cod (@ f) ) by Def10, Def11;

theorem Th27: :: ENS_1:27

for V being non empty set
for a, b being Object of (Ens V) holds Hom (a,b) = Maps ((@ a),(@ b))

proof end;

Lm6: for V being non empty set
for a, b being Object of (Ens V) st Hom (a,b) <> {} holds
Funcs ((@ a),(@ b)) <> {}

proof end;

theorem Th28: :: ENS_1:28

for V being non empty set
for g, f being Morphism of (Ens V) st dom g = cod f holds
g * f = (@ g) * (@ f)

proof end;

theorem :: ENS_1:29

for V being non empty set
for a being Object of (Ens V) holds id a = id$ (@ a) by Def13;

theorem :: ENS_1:30

for V being non empty set
for a being Object of (Ens V) st a = {} holds
a is initial

proof end;

theorem Th31: :: ENS_1:31

for V being non empty set
for a being Object of (Ens V) st {} in V & a is initial holds
a = {}

proof end;

theorem :: ENS_1:32

for W being Universe
for a being Object of (Ens W) st a is initial holds
a = {} by Th31, CLASSES2:62;

theorem :: ENS_1:33

for V being non empty set
for a being Object of (Ens V) st ex x being set st a = {x} holds
a is terminal

proof end;

theorem Th34: :: ENS_1:34

for V being non empty set
for a being Object of (Ens V) st V <> {{}} & a is terminal holds
ex x being set st a = {x}

proof end;

theorem :: ENS_1:35

for W being Universe
for a being Object of (Ens W) st a is terminal holds
ex x being set st a = {x}

proof end;

theorem :: ENS_1:36

for V being non empty set
for f being Morphism of (Ens V) holds
( f is monic iff (@ f) `2 is one-to-one )

proof end;

theorem Th37: :: ENS_1:37

for V being non empty set
for f being Morphism of (Ens V) st f is epi & ex A being Element of V ex x1, x2 being set st
( x1 in A & x2 in A & x1 <> x2 ) holds
@ f is surjective

proof end;

theorem :: ENS_1:38

for V being non empty set
for f being Morphism of (Ens V) st @ f is surjective holds
f is epi

proof end;

theorem :: ENS_1:39

for W being Universe
for f being Morphism of (Ens W) st f is epi holds
@ f is surjective

proof end;

theorem :: ENS_1:40

for V being non empty set
for W being non empty Subset of V holds Ens W is_full_subcategory_of Ens V

proof end;

begin

definition

let C be Category;
func Hom C -> set equals :: ENS_1:def 19
{ (Hom (a,b)) where a, b is Object of C : verum } ;
coherence
{ (Hom (a,b)) where a, b is Object of C : verum } is set ;

end;

:: deftheorem defines Hom ENS_1:def 19 :
for C being Category holds Hom C = { (Hom (a,b)) where a, b is Object of C : verum } ;

registration

let C be Category;
cluster Hom C -> non empty ;
coherence
not Hom C is empty

proof end;

end;

theorem :: ENS_1:41

for C being Category
for a, b being Object of C holds Hom (a,b) in Hom C ;

theorem :: ENS_1:42

for C being Category
for a being Object of C
for f being Morphism of C holds
( ( Hom (a,(cod f)) = {} implies Hom (a,(dom f)) = {} ) & ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) )

proof end;

definition

let C be Category;
let a be Object of C;
let f be Morphism of C;
func hom (a,f) -> Function of (Hom (a,(dom f))),(Hom (a,(cod f))) means :Def20: :: ENS_1:def 20
for g being Morphism of C st g in Hom (a,(dom f)) holds
it . g = f * g;
existence
ex b₁ being Function of (Hom (a,(dom f))),(Hom (a,(cod f))) st
for g being Morphism of C st g in Hom (a,(dom f)) holds
b₁ . g = f * g

proof end;

uniqueness
for b₁, b₂ being Function of (Hom (a,(dom f))),(Hom (a,(cod f))) st ( for g being Morphism of C st g in Hom (a,(dom f)) holds
b₁ . g = f * g ) & ( for g being Morphism of C st g in Hom (a,(dom f)) holds
b₂ . g = f * g ) holds
b₁ = b₂

proof end;

func hom (f,a) -> Function of (Hom ((cod f),a)),(Hom ((dom f),a)) means :Def21: :: ENS_1:def 21
for g being Morphism of C st g in Hom ((cod f),a) holds
it . g = g * f;
existence
ex b₁ being Function of (Hom ((cod f),a)),(Hom ((dom f),a)) st
for g being Morphism of C st g in Hom ((cod f),a) holds
b₁ . g = g * f

proof end;

uniqueness
for b₁, b₂ being Function of (Hom ((cod f),a)),(Hom ((dom f),a)) st ( for g being Morphism of C st g in Hom ((cod f),a) holds
b₁ . g = g * f ) & ( for g being Morphism of C st g in Hom ((cod f),a) holds
b₂ . g = g * f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines hom ENS_1:def 20 :
for C being Category
for a being Object of C
for f being Morphism of C
for b₄ being Function of (Hom (a,(dom f))),(Hom (a,(cod f))) holds
( b₄ = hom (a,f) iff for g being Morphism of C st g in Hom (a,(dom f)) holds
b₄ . g = f * g );

:: deftheorem Def21 defines hom ENS_1:def 21 :
for C being Category
for a being Object of C
for f being Morphism of C
for b₄ being Function of (Hom ((cod f),a)),(Hom ((dom f),a)) holds
( b₄ = hom (f,a) iff for g being Morphism of C st g in Hom ((cod f),a) holds
b₄ . g = g * f );

theorem Th43: :: ENS_1:43

for C being Category
for a, c being Object of C holds hom (a,(id c)) = id (Hom (a,c))

proof end;

theorem Th44: :: ENS_1:44

for C being Category
for c, a being Object of C holds hom ((id c),a) = id (Hom (c,a))

proof end;

theorem Th45: :: ENS_1:45

for C being Category
for a being Object of C
for g, f being Morphism of C st dom g = cod f holds
hom (a,(g * f)) = (hom (a,g)) * (hom (a,f))

proof end;

theorem Th46: :: ENS_1:46

for C being Category
for a being Object of C
for g, f being Morphism of C st dom g = cod f holds
hom ((g * f),a) = (hom (f,a)) * (hom (g,a))

proof end;

theorem Th47: :: ENS_1:47

for C being Category
for a being Object of C
for f being Morphism of C holds [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] is Element of Maps (Hom C)

proof end;

theorem Th48: :: ENS_1:48

for C being Category
for a being Object of C
for f being Morphism of C holds [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] is Element of Maps (Hom C)

proof end;

definition

let C be Category;
let a be Object of C;
func hom?- a -> Function of the carrier' of C,(Maps (Hom C)) means :Def22: :: ENS_1:def 22
for f being Morphism of C holds it . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))];
existence
ex b₁ being Function of the carrier' of C,(Maps (Hom C)) st
for f being Morphism of C holds b₁ . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]

proof end;

uniqueness
for b₁, b₂ being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b₁ . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) & ( for f being Morphism of C holds b₂ . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) holds
b₁ = b₂

proof end;

func hom-? a -> Function of the carrier' of C,(Maps (Hom C)) means :Def23: :: ENS_1:def 23
for f being Morphism of C holds it . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))];
existence
ex b₁ being Function of the carrier' of C,(Maps (Hom C)) st
for f being Morphism of C holds b₁ . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]

proof end;

uniqueness
for b₁, b₂ being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b₁ . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) & ( for f being Morphism of C holds b₂ . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines hom?- ENS_1:def 22 :
for C being Category
for a being Object of C
for b₃ being Function of the carrier' of C,(Maps (Hom C)) holds
( b₃ = hom?- a iff for f being Morphism of C holds b₃ . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] );

:: deftheorem Def23 defines hom-? ENS_1:def 23 :
for C being Category
for a being Object of C
for b₃ being Function of the carrier' of C,(Maps (Hom C)) holds
( b₃ = hom-? a iff for f being Morphism of C holds b₃ . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] );

Lm7: for V being non empty set
for C being Category
for T being Function of the carrier' of C,(Maps (Hom C)) st Hom C c= V holds
T is Function of the carrier' of C, the carrier' of (Ens V)

proof end;

Lm8: for V being non empty set
for C being Category
for a, c being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom (a,c) holds
(hom?- a) . (id c) = id d

proof end;

Lm9: for V being non empty set
for C being Category
for c, a being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom (c,a) holds
(hom-? a) . (id c) = id d

proof end;

theorem Th49: :: ENS_1:49

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom?- a is Functor of C, Ens V

proof end;

theorem Th50: :: ENS_1:50

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom-? a is Contravariant_Functor of C, Ens V

proof end;

theorem Th51: :: ENS_1:51

for C being Category
for f, f9 being Morphism of C st Hom ((dom f),(cod f9)) = {} holds
Hom ((cod f),(dom f9)) = {}

proof end;

definition

let C be Category;
let f, g be Morphism of C;
func hom (f,g) -> Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))) means :Def24: :: ENS_1:def 24
for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
it . h = (g * h) * f;
existence
ex b₁ being Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))) st
for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
b₁ . h = (g * h) * f

proof end;

uniqueness
for b₁, b₂ being Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))) st ( for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
b₁ . h = (g * h) * f ) & ( for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
b₂ . h = (g * h) * f ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def24 defines hom ENS_1:def 24 :
for C being Category
for f, g being Morphism of C
for b₄ being Function of (Hom ((cod f),(dom g))),(Hom ((dom f),(cod g))) holds
( b₄ = hom (f,g) iff for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
b₄ . h = (g * h) * f );

theorem Th52: :: ENS_1:52

for C being Category
for f, g being Morphism of C holds [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] is Element of Maps (Hom C)

proof end;

theorem Th53: :: ENS_1:53

for C being Category
for a being Object of C
for f being Morphism of C holds
( hom ((id a),f) = hom (a,f) & hom (f,(id a)) = hom (f,a) )

proof end;

theorem Th54: :: ENS_1:54

for C being Category
for a, b being Object of C holds hom ((id a),(id b)) = id (Hom (a,b))

proof end;

theorem :: ENS_1:55

for C being Category
for f, g being Morphism of C holds hom (f,g) = (hom ((dom f),g)) * (hom (f,(dom g)))

proof end;

theorem Th56: :: ENS_1:56

for C being Category
for g, f, g9, f9 being Morphism of C st cod g = dom f & dom g9 = cod f9 holds
hom ((f * g),(g9 * f9)) = (hom (g,g9)) * (hom (f,f9))

proof end;

definition

let C be Category;
func hom?? C -> Function of the carrier' of [:C,C:],(Maps (Hom C)) means :Def25: :: ENS_1:def 25
for f, g being Morphism of C holds it . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))];
existence
ex b₁ being Function of the carrier' of [:C,C:],(Maps (Hom C)) st
for f, g being Morphism of C holds b₁ . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

proof end;

uniqueness
for b₁, b₂ being Function of the carrier' of [:C,C:],(Maps (Hom C)) st ( for f, g being Morphism of C holds b₁ . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) & ( for f, g being Morphism of C holds b₂ . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def25 defines hom?? ENS_1:def 25 :
for C being Category
for b₂ being Function of the carrier' of [:C,C:],(Maps (Hom C)) holds
( b₂ = hom?? C iff for f, g being Morphism of C holds b₂ . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] );

theorem Th57: :: ENS_1:57

for C being Category
for a being Object of C holds
( hom?- a = (curry (hom?? C)) . (id a) & hom-? a = (curry' (hom?? C)) . (id a) )

proof end;

Lm10: for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
for d being Object of (Ens V) st d = Hom (a,b) holds
(hom?? C) . [(id a),(id b)] = id d

proof end;

theorem Th58: :: ENS_1:58

for V being non empty set
for C being Category st Hom C c= V holds
hom?? C is Functor of [:(C opp),C:], Ens V

proof end;

definition

let V be non empty set ;
let C be Category;
let a be Object of C;
assume A1: Hom C c= V ;
func hom?- (V,a) -> Functor of C, Ens V equals :Def26: :: ENS_1:def 26
hom?- a;
coherence
hom?- a is Functor of C, Ens V by A1, Th49;
func hom-? (V,a) -> Contravariant_Functor of C, Ens V equals :Def27: :: ENS_1:def 27
hom-? a;
coherence
hom-? a is Contravariant_Functor of C, Ens V by A1, Th50;

end;

:: deftheorem Def26 defines hom?- ENS_1:def 26 :
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom?- (V,a) = hom?- a;

:: deftheorem Def27 defines hom-? ENS_1:def 27 :
for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
hom-? (V,a) = hom-? a;

definition

let V be non empty set ;
let C be Category;
assume A1: Hom C c= V ;
func hom?? (V,C) -> Functor of [:(C opp),C:], Ens V equals :Def28: :: ENS_1:def 28
hom?? C;
coherence
hom?? C is Functor of [:(C opp),C:], Ens V by A1, Th58;

end;

:: deftheorem Def28 defines hom?? ENS_1:def 28 :
for V being non empty set
for C being Category st Hom C c= V holds
hom?? (V,C) = hom?? C;

theorem :: ENS_1:59

for V being non empty set
for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom?- (V,a)) . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]

proof end;

theorem :: ENS_1:60

for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?- (V,a))) . b = Hom (a,b)

proof end;

theorem :: ENS_1:61

for V being non empty set
for C being Category
for a being Object of C
for f being Morphism of C st Hom C c= V holds
(hom-? (V,a)) . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]

proof end;

theorem :: ENS_1:62

for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom-? (V,a))) . b = Hom (b,a)

proof end;

theorem :: ENS_1:63

for V being non empty set
for C being Category
for f, g being Morphism of C st Hom C c= V holds
(hom?? (V,C)) . [(f opp),g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]

proof end;

theorem :: ENS_1:64

for V being non empty set
for C being Category
for a, b being Object of C st Hom C c= V holds
(Obj (hom?? (V,C))) . [(a opp),b] = Hom (a,b)

proof end;

theorem :: ENS_1:65

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
(hom?? (V,C)) ?- (a opp) = hom?- (V,a)

proof end;

theorem :: ENS_1:66

for V being non empty set
for C being Category
for a being Object of C st Hom C c= V holds
(hom?? (V,C)) -? a = hom-? (V,a)

proof end;