:: ENS_1 semantic presentation

definition

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

end;

:: deftheorem Def1 defines Funcs ENS_1:def 1 :

registration

let c₁ be non empty set ;
cluster Funcs a₁ -> non empty functional ;
coherence

proof end;

end;

theorem Th1: :: ENS_1:1

for b₁ being non empty set
for b₂ being set holds
( b₂ in Funcs b₁ iff ex b₃, b₄ being Element of b₁ st
( ( b₄ = {} implies b₃ = {} ) & b₂ is Function of b₃,b₄ ) )

proof end;

theorem Th2: :: ENS_1:2

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds Funcs b₂,b₃ c= Funcs b₁

proof end;

theorem Th3: :: ENS_1:3

for b₁ being non empty set
for b₂ being non empty Subset of b₁ holds Funcs b₂ c= Funcs b₁

proof end;

definition

let c₁ be non empty set ;
func Maps c₁ -> set equals :: ENS_1:def 2
{ [[b₁,b₂],b₃] where B is Element of a₁, B is Element of a₁, B is Element of Funcs a₁ : ( ( b₂ = {} implies b₁ = {} ) & b₃ is Function of b₁,b₂ ) } ;
coherence ;

end;

:: deftheorem Def2 defines Maps ENS_1:def 2 :

registration

let c₁ be non empty set ;
cluster Maps a₁ -> non empty ;
coherence

proof end;

end;

theorem Th4: :: ENS_1:4

for b₁ being non empty set
for b₂ being Element of Maps b₁ ex b₃ being Element of Funcs b₁ex b₄, b₅ being Element of b₁ st
( b₂ = [[b₄,b₅],b₃] & ( b₅ = {} implies b₄ = {} ) & b₃ is Function of b₄,b₅ )

proof end;

theorem Th5: :: ENS_1:5

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being Function of b₂,b₃ st ( b₃ = {} implies b₂ = {} ) holds
[[b₂,b₃],b₄] in Maps b₁

proof end;

theorem Th6: :: ENS_1:6

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

proof end;

theorem Th7: :: ENS_1:7

for b₁ being non empty set
for b₂ being non empty Subset of b₁ holds Maps b₂ c= Maps b₁

proof end;

Lemma6: for b₁, b₂, b₃, b₄, b₅, b₆ being set st [[b₁,b₃],b₅] = [[b₂,b₄],b₆] holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

registration

let c₁ be non empty set ;
let c₂ be Element of Maps c₁;
cluster a₂ `2 -> Relation-like Function-like ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Element of Maps c₁;
canceled;
func dom c₂ -> Element of a₁ equals :: ENS_1:def 4
(a₂ `1 ) `1 ;
coherence

proof end;

func cod c₂ -> Element of a₁ equals :: ENS_1:def 5
(a₂ `1 ) `2 ;
coherence

proof end;

end;

:: deftheorem Def3 ENS_1:def 3 :

:: deftheorem Def4 defines dom ENS_1:def 4 :

:: deftheorem Def5 defines cod ENS_1:def 5 :

theorem Th8: :: ENS_1:8

for b₁ being non empty set
for b₂ being Element of Maps b₁ holds b₂ = [[(dom b₂),(cod b₂)],(b₂ `2 )]

proof end;

Lemma8: for b₁ being non empty set
for b₂, b₃ being Element of Maps b₁ st b₂ `2 = b₃ `2 & dom b₂ = dom b₃ & cod b₂ = cod b₃ holds
b₂ = b₃

proof end;

theorem Th9: :: ENS_1:9

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

proof end;

Lemma10: for b₁ being non empty set
for b₂ being Element of Maps b₁ holds
( dom (b₂ `2 ) = dom b₂ & rng (b₂ `2 ) c= cod b₂ )

proof end;

theorem Th10: :: ENS_1:10

for b₁ being non empty set
for b₂ being Function
for b₃, b₄ being set st [[b₃,b₄],b₂] in Maps b₁ holds
( ( b₄ = {} implies b₃ = {} ) & b₂ is Function of b₃,b₄ )

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
func id$ c₂ -> Element of Maps a₁ equals :: ENS_1:def 6
[[a₂,a₂],(id a₂)];
coherence

proof end;

end;

:: deftheorem Def6 defines id$ ENS_1:def 6 :

theorem Th11: :: ENS_1:11

for b₁ being non empty set
for b₂ being Element of b₁ holds
( (id$ b₂) `2 = id b₂ & dom (id$ b₂) = b₂ & cod (id$ b₂) = b₂ )

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of Maps c₁;
assume E13: cod c₂ = dom c₃ ;
func c₃ * c₂ -> Element of Maps a₁ equals :Def7: :: ENS_1:def 7
[[(dom a₂),(cod a₃)],((a₃ `2 ) * (a₂ `2 ))];
coherence

proof end;

end;

:: deftheorem Def7 defines * ENS_1:def 7 :

theorem Th12: :: ENS_1:12

for b₁ being non empty set
for b₂, b₃ being Element of Maps b₁ st dom b₂ = cod b₃ holds
( (b₂ * b₃) `2 = (b₂ `2 ) * (b₃ `2 ) & dom (b₂ * b₃) = dom b₃ & cod (b₂ * b₃) = cod b₂ )

proof end;

theorem Th13: :: ENS_1:13

for b₁ being non empty set
for b₂, b₃, b₄ being Element of Maps b₁ st dom b₂ = cod b₃ & dom b₄ = cod b₂ holds
b₄ * (b₂ * b₃) = (b₄ * b₂) * b₃

proof end;

theorem Th14: :: ENS_1:14

for b₁ being non empty set
for b₂ being Element of Maps b₁ holds
( b₂ * (id$ (dom b₂)) = b₂ & (id$ (cod b₂)) * b₂ = b₂ )

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be Element of c₁;
func Maps c₂,c₃ -> set equals :: ENS_1:def 8
{ [[a₂,a₃],b₁] where B is Element of Funcs a₁ : [[a₂,a₃],b₁] in Maps a₁ } ;
correctness ;

end;

:: deftheorem Def8 defines Maps ENS_1:def 8 :

theorem Th15: :: ENS_1:15

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being Function of b₂,b₃ st ( b₃ = {} implies b₂ = {} ) holds
[[b₂,b₃],b₄] in Maps b₂,b₃

proof end;

theorem Th16: :: ENS_1:16

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being Element of Maps b₁ st b₄ in Maps b₂,b₃ holds
b₄ = [[b₂,b₃],(b₄ `2 )]

proof end;

theorem Th17: :: ENS_1:17

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds Maps b₂,b₃ c= Maps b₁

proof end;

Lemma20: for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being Function st [[b₂,b₃],b₄] in Maps b₂,b₃ holds
( ( b₃ = {} implies b₂ = {} ) & b₄ is Function of b₂,b₃ )

proof end;

theorem Th18: :: ENS_1:18

for b₁ being non empty set holds Maps b₁ = union { (Maps b₂,b₃) where B is Element of b₁, B is Element of b₁ : verum }

proof end;

theorem Th19: :: ENS_1:19

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being Element of Maps b₁ holds
( b₄ in Maps b₂,b₃ iff ( dom b₄ = b₂ & cod b₄ = b₃ ) )

proof end;

theorem Th20: :: ENS_1:20

for b₁ being non empty set
for b₂, b₃ being Element of b₁
for b₄ being Element of Maps b₁ st b₄ in Maps b₂,b₃ holds
b₄ `2 in Funcs b₂,b₃

proof end;

Lemma23: for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃, b₄ being Element of b₂
for b₅, b₆ being Element of b₁ st b₃ = b₅ & b₄ = b₆ holds
Maps b₃,b₄ = Maps b₅,b₆

proof end;

definition

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

end;

:: deftheorem Def9 defines surjective ENS_1:def 9 :

notation

let c₁ be non empty set ;
let c₂ be Element of Maps c₁;
synonym c₂ is_a_surjection for surjective c₂c₂ is_a_surjection is_a_surjection ;

end;

definition

let c₁ be non empty set ;
func fDom c₁ -> Function of Maps a₁,a₁ means :Def10: :: ENS_1:def 10
for b₁ being Element of Maps a₁ holds a₂ . b₁ = dom b₁;
existence

proof end;

uniqueness

proof end;

func fCod c₁ -> Function of Maps a₁,a₁ means :Def11: :: ENS_1:def 11
for b₁ being Element of Maps a₁ holds a₂ . b₁ = cod b₁;
existence

proof end;

uniqueness

proof end;

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

proof end;

uniqueness

proof end;

func fId c₁ -> Function of a₁, Maps a₁ means :Def13: :: ENS_1:def 13
for b₁ being Element of a₁ holds a₂ . b₁ = id$ b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines fDom ENS_1:def 10 :

:: deftheorem Def11 defines fCod ENS_1:def 11 :

:: deftheorem Def12 defines fComp ENS_1:def 12 :

:: deftheorem Def13 defines fId ENS_1:def 13 :

definition

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

end;

:: deftheorem Def14 defines Ens ENS_1:def 14 :

theorem Th21: :: ENS_1:21

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

proof end;

registration

let c₁ be non empty set ;
cluster Ens a₁ -> strict Category-like ;
coherence by Th21;

end;

theorem Th22: :: ENS_1:22

for b₁ being non empty set
for b₂ being Element of b₁ holds b₂ is Object of (Ens b₁) ;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
func @ c₂ -> Object of (Ens a₁) equals :: ENS_1:def 15
a₂;
coherence ;

end;

:: deftheorem Def15 defines @ ENS_1:def 15 :

theorem Th23: :: ENS_1:23

for b₁ being non empty set
for b₂ being Object of (Ens b₁) holds b₂ is Element of b₁ ;

definition

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

end;

:: deftheorem Def16 defines @ ENS_1:def 16 :

theorem Th24: :: ENS_1:24

for b₁ being non empty set
for b₂ being Element of Maps b₁ holds b₂ is Morphism of (Ens b₁) ;

definition

let c₁ be non empty set ;
let c₂ be Element of Maps c₁;
func @ c₂ -> Morphism of (Ens a₁) equals :: ENS_1:def 17
a₂;
coherence ;

end;

:: deftheorem Def17 defines @ ENS_1:def 17 :

theorem Th25: :: ENS_1:25

for b₁ being non empty set
for b₂ being Morphism of (Ens b₁) holds b₂ is Element of Maps b₁ ;

definition

let c₁ be non empty set ;
let c₂ be Morphism of (Ens c₁);
func @ c₂ -> Element of Maps a₁ equals :: ENS_1:def 18
a₂;
coherence ;

end;

:: deftheorem Def18 defines @ ENS_1:def 18 :

theorem Th26: :: ENS_1:26

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

theorem Th27: :: ENS_1:27

for b₁ being non empty set
for b₂, b₃ being Object of (Ens b₁) holds Hom b₂,b₃ = Maps (@ b₂),(@ b₃)

proof end;

Lemma31: for b₁ being non empty set
for b₂, b₃ being Object of (Ens b₁) st Hom b₂,b₃ <> {} holds
Funcs (@ b₂),(@ b₃) <> {}

proof end;

theorem Th28: :: ENS_1:28

for b₁ being non empty set
for b₂, b₃ being Morphism of (Ens b₁) st dom b₂ = cod b₃ holds
b₂ * b₃ = (@ b₂) * (@ b₃)

proof end;

theorem Th29: :: ENS_1:29

for b₁ being non empty set
for b₂ being Object of (Ens b₁) holds id b₂ = id$ (@ b₂) by Def13;

theorem Th30: :: ENS_1:30

for b₁ being non empty set
for b₂ being Object of (Ens b₁) st b₂ = {} holds
b₂ is initial

proof end;

theorem Th31: :: ENS_1:31

for b₁ being non empty set
for b₂ being Object of (Ens b₁) st {} in b₁ & b₂ is initial holds
b₂ = {}

proof end;

theorem Th32: :: ENS_1:32

for b₁ being Universe
for b₂ being Object of (Ens b₁) st b₂ is initial holds
b₂ = {}

proof end;

theorem Th33: :: ENS_1:33

for b₁ being non empty set
for b₂ being Object of (Ens b₁) st ex b₃ being set st b₂ = {b₃} holds
b₂ is terminal

proof end;

theorem Th34: :: ENS_1:34

for b₁ being non empty set
for b₂ being Object of (Ens b₁) st b₁ <> {{} } & b₂ is terminal holds
ex b₃ being set st b₂ = {b₃}

proof end;

theorem Th35: :: ENS_1:35

for b₁ being Universe
for b₂ being Object of (Ens b₁) st b₂ is terminal holds
ex b₃ being set st b₂ = {b₃}

proof end;

theorem Th36: :: ENS_1:36

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

proof end;

theorem Th37: :: ENS_1:37

for b₁ being non empty set
for b₂ being Morphism of (Ens b₁) st b₂ is epi & ex b₃ being Element of b₁ex b₄, b₅ being set st
( b₄ in b₃ & b₅ in b₃ & b₄ <> b₅ ) holds
@ b₂ is surjective

proof end;

theorem Th38: :: ENS_1:38

for b₁ being non empty set
for b₂ being Morphism of (Ens b₁) st @ b₂ is surjective holds
b₂ is epi

proof end;

theorem Th39: :: ENS_1:39

for b₁ being Universe
for b₂ being Morphism of (Ens b₁) st b₂ is epi holds
@ b₂ is surjective

proof end;

theorem Th40: :: ENS_1:40

for b₁ being non empty set
for b₂ being non empty Subset of b₁ holds Ens b₂ is_full_subcategory_of Ens b₁

proof end;

definition

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

end;

:: deftheorem Def19 defines Hom ENS_1:def 19 :

registration

let c₁ be Category;
cluster Hom a₁ -> non empty ;
coherence

proof end;

end;

theorem Th41: :: ENS_1:41

for b₁ being Category
for b₂, b₃ being Object of b₁ holds Hom b₂,b₃ in Hom b₁ ;

theorem Th42: :: ENS_1:42

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Morphism of b₁ holds
( ( Hom b₂,(cod b₃) = {} implies Hom b₂,(dom b₃) = {} ) & ( Hom (dom b₃),b₂ = {} implies Hom (cod b₃),b₂ = {} ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

func hom c₃,c₂ -> Function of Hom (cod a₃),a₂, Hom (dom a₃),a₂ means :Def21: :: ENS_1:def 21
for b₁ being Morphism of a₁ st b₁ in Hom (cod a₃),a₂ holds
a₄ . b₁ = b₁ * a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines hom ENS_1:def 20 :

:: deftheorem Def21 defines hom ENS_1:def 21 :

theorem Th43: :: ENS_1:43

for b₁ being Category
for b₂, b₃ being Object of b₁ holds hom b₂,(id b₃) = id (Hom b₂,b₃)

proof end;

theorem Th44: :: ENS_1:44

for b₁ being Category
for b₂, b₃ being Object of b₁ holds hom (id b₂),b₃ = id (Hom b₂,b₃)

proof end;

theorem Th45: :: ENS_1:45

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st dom b₃ = cod b₄ holds
hom b₂,(b₃ * b₄) = (hom b₂,b₃) * (hom b₂,b₄)

proof end;

theorem Th46: :: ENS_1:46

for b₁ being Category
for b₂ being Object of b₁
for b₃, b₄ being Morphism of b₁ st dom b₃ = cod b₄ holds
hom (b₃ * b₄),b₂ = (hom b₄,b₂) * (hom b₃,b₂)

proof end;

theorem Th47: :: ENS_1:47

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Morphism of b₁ holds [[(Hom b₂,(dom b₃)),(Hom b₂,(cod b₃))],(hom b₂,b₃)] is Element of Maps (Hom b₁)

proof end;

theorem Th48: :: ENS_1:48

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Morphism of b₁ holds [[(Hom (cod b₃),b₂),(Hom (dom b₃),b₂)],(hom b₃,b₂)] is Element of Maps (Hom b₁)

proof end;

definition

let c₁ be Category;
let c₂ be Object of c₁;
func hom?- c₂ -> Function of the Morphisms of a₁, Maps (Hom a₁) means :Def22: :: ENS_1:def 22
for b₁ being Morphism of a₁ holds a₃ . b₁ = [[(Hom a₂,(dom b₁)),(Hom a₂,(cod b₁))],(hom a₂,b₁)];
existence

proof end;

uniqueness

proof end;

func hom-? c₂ -> Function of the Morphisms of a₁, Maps (Hom a₁) means :Def23: :: ENS_1:def 23
for b₁ being Morphism of a₁ holds a₃ . b₁ = [[(Hom (cod b₁),a₂),(Hom (dom b₁),a₂)],(hom b₁,a₂)];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines hom?- ENS_1:def 22 :

:: deftheorem Def23 defines hom-? ENS_1:def 23 :

Lemma47: for b₁ being non empty set
for b₂ being Category
for b₃ being Function of the Morphisms of b₂, Maps (Hom b₂) st Hom b₂ c= b₁ holds
b₃ is Function of the Morphisms of b₂,the Morphisms of (Ens b₁)

proof end;

Lemma48: for b₁ being non empty set
for b₂ being Category
for b₃, b₄ being Object of b₂ st Hom b₂ c= b₁ holds
for b₅ being Object of (Ens b₁) st b₅ = Hom b₃,b₄ holds
(hom?- b₃) . (id b₄) = id b₅

proof end;

Lemma49: for b₁ being non empty set
for b₂ being Category
for b₃, b₄ being Object of b₂ st Hom b₂ c= b₁ holds
for b₅ being Object of (Ens b₁) st b₅ = Hom b₃,b₄ holds
(hom-? b₄) . (id b₃) = id b₅

proof end;

theorem Th49: :: ENS_1:49

for b₁ being non empty set
for b₂ being Category
for b₃ being Object of b₂ st Hom b₂ c= b₁ holds
hom?- b₃ is Functor of b₂, Ens b₁

proof end;

theorem Th50: :: ENS_1:50

for b₁ being non empty set
for b₂ being Category
for b₃ being Object of b₂ st Hom b₂ c= b₁ holds
hom-? b₃ is Contravariant_Functor of b₂, Ens b₁

proof end;

theorem Th51: :: ENS_1:51

for b₁ being Category
for b₂, b₃ being Morphism of b₁ st Hom (dom b₂),(cod b₃) = {} holds
Hom (cod b₂),(dom b₃) = {}

proof end;

definition

let c₁ be Category;
let c₂, c₃ be Morphism of c₁;
func hom c₂,c₃ -> Function of Hom (cod a₂),(dom a₃), Hom (dom a₂),(cod a₃) means :Def24: :: ENS_1:def 24
for b₁ being Morphism of a₁ st b₁ in Hom (cod a₂),(dom a₃) holds
a₄ . b₁ = (a₃ * b₁) * a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines hom ENS_1:def 24 :

theorem Th52: :: ENS_1:52

for b₁ being Category
for b₂, b₃ being Morphism of b₁ holds [[(Hom (cod b₂),(dom b₃)),(Hom (dom b₂),(cod b₃))],(hom b₂,b₃)] is Element of Maps (Hom b₁)

proof end;

theorem Th53: :: ENS_1:53

for b₁ being Category
for b₂ being Object of b₁
for b₃ being Morphism of b₁ holds
( hom (id b₂),b₃ = hom b₂,b₃ & hom b₃,(id b₂) = hom b₃,b₂ )

proof end;

theorem Th54: :: ENS_1:54

for b₁ being Category
for b₂, b₃ being Object of b₁ holds hom (id b₂),(id b₃) = id (Hom b₂,b₃)

proof end;

theorem Th55: :: ENS_1:55

for b₁ being Category
for b₂, b₃ being Morphism of b₁ holds hom b₂,b₃ = (hom (dom b₂),b₃) * (hom b₂,(dom b₃))

proof end;

theorem Th56: :: ENS_1:56

for b₁ being Category
for b₂, b₃, b₄, b₅ being Morphism of b₁ st cod b₂ = dom b₃ & dom b₄ = cod b₅ holds
hom (b₃ * b₂),(b₄ * b₅) = (hom b₂,b₄) * (hom b₃,b₅)

proof end;

definition

let c₁ be Category;
func hom?? c₁ -> Function of the Morphisms of [:a₁,a₁:], Maps (Hom a₁) means :Def25: :: ENS_1:def 25
for b₁, b₂ being Morphism of a₁ holds a₂ . [b₁,b₂] = [[(Hom (cod b₁),(dom b₂)),(Hom (dom b₁),(cod b₂))],(hom b₁,b₂)];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def25 defines hom?? ENS_1:def 25 :

theorem Th57: :: ENS_1:57

for b₁ being Category
for b₂ being Object of b₁ holds
( hom?- b₂ = (curry (hom?? b₁)) . (id b₂) & hom-? b₂ = (curry' (hom?? b₁)) . (id b₂) )

proof end;

Lemma60: for b₁ being non empty set
for b₂ being Category
for b₃, b₄ being Object of b₂ st Hom b₂ c= b₁ holds
for b₅ being Object of (Ens b₁) st b₅ = Hom b₃,b₄ holds
(hom?? b₂) . [(id b₃),(id b₄)] = id b₅

proof end;

theorem Th58: :: ENS_1:58

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be Category;
let c₃ be Object of c₂;
assume E62: Hom c₂ c= c₁ ;
func hom?- c₁,c₃ -> Functor of a₂, Ens a₁ equals :Def26: :: ENS_1:def 26
hom?- a₃;
coherence by E62, Th49;
func hom-? c₁,c₃ -> Contravariant_Functor of a₂, Ens a₁ equals :Def27: :: ENS_1:def 27
hom-? a₃;
coherence by E62, Th50;

end;

:: deftheorem Def26 defines hom?- ENS_1:def 26 :

:: deftheorem Def27 defines hom-? ENS_1:def 27 :

definition

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

end;

:: deftheorem Def28 defines hom?? ENS_1:def 28 :

theorem Th59: :: ENS_1:59

for b₁ being non empty set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Morphism of b₂ st Hom b₂ c= b₁ holds
(hom?- b₁,b₃) . b₄ = [[(Hom b₃,(dom b₄)),(Hom b₃,(cod b₄))],(hom b₃,b₄)]

proof end;

theorem Th60: :: ENS_1:60

for b₁ being non empty set
for b₂ being Category
for b₃, b₄ being Object of b₂ st Hom b₂ c= b₁ holds
(Obj (hom?- b₁,b₃)) . b₄ = Hom b₃,b₄

proof end;

theorem Th61: :: ENS_1:61

for b₁ being non empty set
for b₂ being Category
for b₃ being Object of b₂
for b₄ being Morphism of b₂ st Hom b₂ c= b₁ holds
(hom-? b₁,b₃) . b₄ = [[(Hom (cod b₄),b₃),(Hom (dom b₄),b₃)],(hom b₄,b₃)]

proof end;

theorem Th62: :: ENS_1:62

for b₁ being non empty set
for b₂ being Category
for b₃, b₄ being Object of b₂ st Hom b₂ c= b₁ holds
(Obj (hom-? b₁,b₃)) . b₄ = Hom b₄,b₃

proof end;

theorem Th63: :: ENS_1:63

for b₁ being non empty set
for b₂ being Category
for b₃, b₄ being Morphism of b₂ st Hom b₂ c= b₁ holds
(hom?? b₁,b₂) . [(b₃ opp ),b₄] = [[(Hom (cod b₃),(dom b₄)),(Hom (dom b₃),(cod b₄))],(hom b₃,b₄)]

proof end;

theorem Th64: :: ENS_1:64

for b₁ being non empty set
for b₂ being Category
for b₃, b₄ being Object of b₂ st Hom b₂ c= b₁ holds
(Obj (hom?? b₁,b₂)) . [(b₃ opp ),b₄] = Hom b₃,b₄

proof end;

theorem Th65: :: ENS_1:65

for b₁ being non empty set
for b₂ being Category
for b₃ being Object of b₂ st Hom b₂ c= b₁ holds
(hom?? b₁,b₂) ?- (b₃ opp ) = hom?- b₁,b₃

proof end;

theorem Th66: :: ENS_1:66

for b₁ being non empty set
for b₂ being Category
for b₃ being Object of b₂ st Hom b₂ c= b₁ holds
(hom?? b₁,b₂) -? b₃ = hom-? b₁,b₃

proof end;