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


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 for set ;
coherence
for b1 being set st b1 = m `2 holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

definition
let V be non empty set ;
let m be Element of Maps V;
func dom m -> Element of V equals :: ENS_1:def 3
(m `1) `1 ;
coherence
(m `1) `1 is Element of V
proof end;
func cod m -> Element of V equals :: ENS_1:def 4
(m `1) `2 ;
coherence
(m `1) `2 is Element of V
proof end;
end;

:: deftheorem defines dom ENS_1:def 3 :
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 4 :
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 5
[[A,A],(id A)];
coherence
[[A,A],(id A)] is Element of Maps V by Th5;
end;

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

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

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 :Def6: :: ENS_1:def 6
[[(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 Def6 defines * ENS_1:def 6 :
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 m1, m2 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 m1, m2, 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 7
 { [[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 7 :
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 8
 rng (m `2) = cod m;
end;

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

definition
let V be non empty set ;
func fDom V -> Function of (Maps V),V means :Def9: :: ENS_1:def 9
 for m being Element of Maps V holds it . m = dom m;
existence
ex b1 being Function of (Maps V),V st
for m being Element of Maps V holds b1 . m = dom m
proof end;
uniqueness
for b1, b2 being Function of (Maps V),V st ( for m being Element of Maps V holds b1 . m = dom m ) & ( for m being Element of Maps V holds b2 . m = dom m ) holds
b1 = b2
proof end;
func fCod V -> Function of (Maps V),V means :Def10: :: ENS_1:def 10
 for m being Element of Maps V holds it . m = cod m;
existence
ex b1 being Function of (Maps V),V st
for m being Element of Maps V holds b1 . m = cod m
proof end;
uniqueness
for b1, b2 being Function of (Maps V),V st ( for m being Element of Maps V holds b1 . m = cod m ) & ( for m being Element of Maps V holds b2 . m = cod m ) holds
b1 = b2
proof end;
func fComp V -> PartFunc of [:(Maps V),(Maps V):],(Maps V) means :Def11: :: ENS_1:def 11
( ( 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 b1 being PartFunc of [:(Maps V),(Maps V):],(Maps V) st
( ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(Maps V),(Maps V):],(Maps V) st ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of Maps V holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of Maps V st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines fDom ENS_1:def 9 :
for V being non empty set
for b2 being Function of (Maps V),V holds
( b2 = fDom V iff for m being Element of Maps V holds b2 . m = dom m );

:: deftheorem Def10 defines fCod ENS_1:def 10 :
for V being non empty set
for b2 being Function of (Maps V),V holds
( b2 = fCod V iff for m being Element of Maps V holds b2 . m = cod m );

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

definition
let V be non empty set ;
func Ens V -> non empty non void strict CatStr equals :: ENS_1:def 13
 CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #);
coherence
CatStr(# V,(Maps V),(fDom V),(fCod V),(fComp V) #) is non empty non void strict CatStr ;
end;

:: deftheorem ENS_1:def 12 :
canceled;

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

registration
let V be non empty set ;
cluster Ens V -> non empty non void strict Category-like transitive associative reflexive with_identities ;
coherence
( Ens V is Category-like & Ens V is reflexive & Ens V is transitive & Ens V is associative & Ens V is with_identities )
proof end;
end;

theorem :: ENS_1:21
canceled;

::$CT
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 14
A;
coherence
A is Object of (Ens V) ;
end;

:: deftheorem defines @ ENS_1:def 14 :
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 15
a;
coherence
a is Element of V ;
end;

:: deftheorem defines @ ENS_1:def 15 :
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 16
m;
coherence
m is Morphism of (Ens V) ;
end;

:: deftheorem defines @ ENS_1:def 16 :
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 17
f;
coherence
f is Element of Maps V ;
end;

:: deftheorem defines @ ENS_1:def 17 :
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 Def9, Def10;

theorem Th26: :: 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 Th27: :: ENS_1:28
for V being non empty set
for f, g being Morphism of (Ens V) st dom g = cod f holds
g (*) f = (@ g) * (@ f)
proof end;

theorem Th28: :: ENS_1:29
for V being non empty set
for a being Object of (Ens V) holds id a = id$ (@ a)
proof end;

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 Th30: :: 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 Th30, CLASSES2:56;

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 Th33: :: 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 a, b being Object of (Ens V)
for f being Morphism of a,b st Hom (a,b) <> {} holds
( f is monic iff (@ f) `2 is one-to-one )
proof end;

theorem Th36: :: ENS_1:37
for V being non empty set
for a, b being Object of (Ens V)
for f being Morphism of a,b st Hom (a,b) <> {} & 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 a, b being Object of (Ens V) st Hom (a,b) <> {} holds
for f being Morphism of a,b st @ f is surjective holds
f is epi
proof end;

theorem :: ENS_1:39
for W being Universe
for a, b being Object of (Ens W) st Hom (a,b) <> {} holds
for f being Morphism of a,b st f is epi holds
@ f is surjective
proof end;

Lm7: for V being non empty set
for W being non empty Subset of V holds Ens W is Subcategory of Ens V
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;

definition
let C be Category;
func Hom C -> set equals :: ENS_1:def 18
 { (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 18 :
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 ;

:: hom-functors
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 :Def18: :: ENS_1:def 19
 for g being Morphism of C st g in Hom (a,(dom f)) holds
it . g = f (*) g;
existence
ex b1 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
b1 . g = f (*) g
proof end;
uniqueness
for b1, b2 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
b1 . g = f (*) g ) & ( for g being Morphism of C st g in Hom (a,(dom f)) holds
b2 . g = f (*) g ) holds
b1 = b2
proof end;
func hom (f,a) -> Function of (Hom ((cod f),a)),(Hom ((dom f),a)) means :Def19: :: ENS_1:def 20
 for g being Morphism of C st g in Hom ((cod f),a) holds
it . g = g (*) f;
existence
ex b1 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
b1 . g = g (*) f
proof end;
uniqueness
for b1, b2 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
b1 . g = g (*) f ) & ( for g being Morphism of C st g in Hom ((cod f),a) holds
b2 . g = g (*) f ) holds
b1 = b2
proof end;
end;

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

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

theorem Th42: :: 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 Th43: :: ENS_1:44
for C being Category
for a, c being Object of C holds hom ((id c),a) = id (Hom (c,a))
proof end;

theorem Th44: :: ENS_1:45
for C being Category
for a being Object of C
for f, g being Morphism of C st dom g = cod f holds
hom (a,(g (*) f)) = (hom (a,g)) * (hom (a,f))
proof end;

theorem Th45: :: ENS_1:46
for C being Category
for a being Object of C
for f, g being Morphism of C st dom g = cod f holds
hom ((g (*) f),a) = (hom (f,a)) * (hom (g,a))
proof end;

theorem Th46: :: 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 Th47: :: 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 :Def20: :: ENS_1:def 21
 for f being Morphism of C holds it . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))];
existence
ex b1 being Function of the carrier' of C,(Maps (Hom C)) st
for f being Morphism of C holds b1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))]
proof end;
uniqueness
for b1, b2 being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b1 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) & ( for f being Morphism of C holds b2 . f = [[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] ) holds
b1 = b2
proof end;
func hom-? a -> Function of the carrier' of C,(Maps (Hom C)) means :Def21: :: ENS_1:def 22
 for f being Morphism of C holds it . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))];
existence
ex b1 being Function of the carrier' of C,(Maps (Hom C)) st
for f being Morphism of C holds b1 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))]
proof end;
uniqueness
for b1, b2 being Function of the carrier' of C,(Maps (Hom C)) st ( for f being Morphism of C holds b1 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) & ( for f being Morphism of C holds b2 . f = [[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] ) holds
b1 = b2
proof end;
end;

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

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

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

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

Lm10: 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 (c,a) holds
(hom-? a) . (id c) = id d
proof end;

theorem Th48: :: 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 Th49: :: 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;

:: hom-bifunctor
theorem Th50: :: 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 :Def22: :: ENS_1:def 23
 for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
it . h = (g (*) h) (*) f;
existence
ex b1 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
b1 . h = (g (*) h) (*) f
proof end;
uniqueness
for b1, b2 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
b1 . h = (g (*) h) (*) f ) & ( for h being Morphism of C st h in Hom ((cod f),(dom g)) holds
b2 . h = (g (*) h) (*) f ) holds
b1 = b2
proof end;
end;

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

theorem Th51: :: 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 Th52: :: 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 Th53: :: 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 Th55: :: ENS_1:56
for C being Category
for f, g, f9, g9 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 :Def23: :: ENS_1:def 24
 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 b1 being Function of the carrier' of [:C,C:],(Maps (Hom C)) st
for f, g being Morphism of C holds b1 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))]
proof end;
uniqueness
for b1, b2 being Function of the carrier' of [:C,C:],(Maps (Hom C)) st ( for f, g being Morphism of C holds b1 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) & ( for f, g being Morphism of C holds b2 . [f,g] = [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] ) holds
b1 = b2
proof end;
end;

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

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

Lm11: 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 Th57: :: 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 :Def24: :: ENS_1:def 25
 hom?- a;
coherence
hom?- a is Functor of C, Ens V by A1, Th48;
func hom-? (V,a) -> Contravariant_Functor of C, Ens V equals :Def25: :: ENS_1:def 26
 hom-? a;
coherence
hom-? a is Contravariant_Functor of C, Ens V by A1, Th49;
end;

:: deftheorem Def24 defines hom?- ENS_1:def 25 :
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 Def25 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;

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 :Def26: :: ENS_1:def 27
 hom?? C;
coherence
hom?? C is Functor of [:(C opp),C:], Ens V by A1, Th57;
end;

:: deftheorem Def26 defines hom?? ENS_1:def 27 :
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;