:: by Grzegorz Bancerek

::

:: Received June 8, 1995

:: Copyright (c) 1995-2017 Association of Mizar Users

registration

let A be non empty set ;

existence

not for b_{1} being ManySortedSet of A holds b_{1} is V9()

end;
existence

not for b

proof end;

definition

let C be Categorial Category;

let f be Morphism of C;

:: original: `2

redefine func f `2 -> Functor of f `11 ,f `12 ;

coherence

f `2 is Functor of f `11 ,f `12

end;
let f be Morphism of C;

:: original: `2

redefine func f `2 -> Functor of f `11 ,f `12 ;

coherence

f `2 is Functor of f `11 ,f `12

proof end;

theorem :: INDEX_1:1

for C being Categorial Category

for f, g being Morphism of C st dom g = cod f holds

g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))]

for f, g being Morphism of C st dom g = cod f holds

g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))]

proof end;

theorem Th2: :: INDEX_1:2

for C being Category

for D, E being Categorial Category

for F being Functor of C,D

for G being Functor of C,E st F = G holds

Obj F = Obj G

for D, E being Categorial Category

for F being Functor of C,D

for G being Functor of C,E st F = G holds

Obj F = Obj G

proof end;

definition

let IT be Function;

end;
attr IT is Category-yielding means :Def1: :: INDEX_1:def 1

for x being set st x in dom IT holds

IT . x is Category;

for x being set st x in dom IT holds

IT . x is Category;

:: deftheorem Def1 defines Category-yielding INDEX_1:def 1 :

for IT being Function holds

( IT is Category-yielding iff for x being set st x in dom IT holds

IT . x is Category );

for IT being Function holds

( IT is Category-yielding iff for x being set st x in dom IT holds

IT . x is Category );

registration
end;

definition
end;

registration
end;

registration
end;

definition

let X be non empty set ;

let f be ManySortedCategory of X;

let x be Element of X;

:: original: .

redefine func f . x -> Category;

coherence

f . x is Category

end;
let f be ManySortedCategory of X;

let x be Element of X;

:: original: .

redefine func f . x -> Category;

coherence

f . x is Category

proof end;

registration

let f be Function;

let g be Category-yielding Function;

coherence

g * f is Category-yielding

end;
let g be Category-yielding Function;

coherence

g * f is Category-yielding

proof end;

:: carrier and Morphisms

definition

let F be Category-yielding Function;

ex b_{1} being non-empty Function st

( dom b_{1} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{1} . x = the carrier of C ) )

for b_{1}, b_{2} being non-empty Function st dom b_{1} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{1} . x = the carrier of C ) & dom b_{2} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{2} . x = the carrier of C ) holds

b_{1} = b_{2}

ex b_{1} being non-empty Function st

( dom b_{1} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{1} . x = the carrier' of C ) )

for b_{1}, b_{2} being non-empty Function st dom b_{1} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{1} . x = the carrier' of C ) & dom b_{2} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{2} . x = the carrier' of C ) holds

b_{1} = b_{2}

end;
func Objs F -> non-empty Function means :Def2: :: INDEX_1:def 2

( dom it = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

it . x = the carrier of C ) );

existence ( dom it = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

it . x = the carrier of C ) );

ex b

( dom b

for C being Category st C = F . x holds

b

proof end;

uniqueness for b

for C being Category st C = F . x holds

b

for C being Category st C = F . x holds

b

b

proof end;

func Mphs F -> non-empty Function means :Def3: :: INDEX_1:def 3

( dom it = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

it . x = the carrier' of C ) );

existence ( dom it = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

it . x = the carrier' of C ) );

ex b

( dom b

for C being Category st C = F . x holds

b

proof end;

uniqueness for b

for C being Category st C = F . x holds

b

for C being Category st C = F . x holds

b

b

proof end;

:: deftheorem Def2 defines Objs INDEX_1:def 2 :

for F being Category-yielding Function

for b_{2} being non-empty Function holds

( b_{2} = Objs F iff ( dom b_{2} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{2} . x = the carrier of C ) ) );

for F being Category-yielding Function

for b

( b

for C being Category st C = F . x holds

b

:: deftheorem Def3 defines Mphs INDEX_1:def 3 :

for F being Category-yielding Function

for b_{2} being non-empty Function holds

( b_{2} = Mphs F iff ( dom b_{2} = dom F & ( for x being object st x in dom F holds

for C being Category st C = F . x holds

b_{2} . x = the carrier' of C ) ) );

for F being Category-yielding Function

for b

( b

for C being Category st C = F . x holds

b

registration

let A be non empty set ;

let F be ManySortedCategory of A;

coherence

Objs F is A -defined

Mphs F is A -defined

end;
let F be ManySortedCategory of A;

coherence

Objs F is A -defined

proof end;

coherence Mphs F is A -defined

proof end;

registration

let A be non empty set ;

let F be ManySortedCategory of A;

coherence

Objs F is total

Mphs F is total

end;
let F be ManySortedCategory of A;

coherence

Objs F is total

proof end;

coherence Mphs F is total

proof end;

theorem :: INDEX_1:3

for X being set

for C being Category holds

( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )

for C being Category holds

( Objs (X --> C) = X --> the carrier of C & Mphs (X --> C) = X --> the carrier' of C )

proof end;

definition

let A, B be set ;

ex b_{1} being object ex f being ManySortedSet of A ex g being ManySortedSet of B st b_{1} = [f,g]

end;
mode ManySortedSet of A,B -> object means :Def4: :: INDEX_1:def 4

ex f being ManySortedSet of A ex g being ManySortedSet of B st it = [f,g];

existence ex f being ManySortedSet of A ex g being ManySortedSet of B st it = [f,g];

ex b

proof end;

:: deftheorem Def4 defines ManySortedSet INDEX_1:def 4 :

for A, B being set

for b_{3} being object holds

( b_{3} is ManySortedSet of A,B iff ex f being ManySortedSet of A ex g being ManySortedSet of B st b_{3} = [f,g] );

for A, B being set

for b

( b

definition

let A, B be set ;

let f be ManySortedSet of A;

let g be ManySortedSet of B;

:: original: [

redefine func [f,g] -> ManySortedSet of A,B;

coherence

[f,g] is ManySortedSet of A,B

end;
let f be ManySortedSet of A;

let g be ManySortedSet of B;

:: original: [

redefine func [f,g] -> ManySortedSet of A,B;

coherence

[f,g] is ManySortedSet of A,B

proof end;

registration

let A, B be set ;

let X be ManySortedSet of A,B;

coherence

for b_{1} being set st b_{1} = X `1 holds

( b_{1} is Function-like & b_{1} is Relation-like )

for b_{1} being set st b_{1} = X `2 holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let X be ManySortedSet of A,B;

coherence

for b

( b

proof end;

coherence for b

( b

proof end;

registration

let A, B be set ;

let X be ManySortedSet of A,B;

coherence

for b_{1} being Relation st b_{1} = X `1 holds

b_{1} is A -defined

for b_{1} being Relation st b_{1} = X `2 holds

b_{1} is B -defined

end;
let X be ManySortedSet of A,B;

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let A, B be set ;

let X be ManySortedSet of A,B;

coherence

for b_{1} being A -defined Function st b_{1} = X `1 holds

b_{1} is total

for b_{1} being B -defined Function st b_{1} = X `2 holds

b_{1} is total

end;
let X be ManySortedSet of A,B;

coherence

for b

b

proof end;

coherence for b

b

proof end;

:: deftheorem Def5 defines Category-yielding_on_first INDEX_1:def 5 :

for A, B being set

for IT being ManySortedSet of A,B holds

( IT is Category-yielding_on_first iff IT `1 is Category-yielding );

for A, B being set

for IT being ManySortedSet of A,B holds

( IT is Category-yielding_on_first iff IT `1 is Category-yielding );

:: deftheorem Def6 defines Function-yielding_on_second INDEX_1:def 6 :

for A, B being set

for IT being ManySortedSet of A,B holds

( IT is Function-yielding_on_second iff IT `2 is Function-yielding );

for A, B being set

for IT being ManySortedSet of A,B holds

( IT is Function-yielding_on_second iff IT `2 is Function-yielding );

registration

let A, B be set ;

existence

ex b_{1} being ManySortedSet of A,B st

( b_{1} is Category-yielding_on_first & b_{1} is Function-yielding_on_second )

end;
existence

ex b

( b

proof end;

registration

let A, B be set ;

let X be Category-yielding_on_first ManySortedSet of A,B;

coherence

for b_{1} being Function st b_{1} = X `1 holds

b_{1} is Category-yielding
by Def5;

end;
let X be Category-yielding_on_first ManySortedSet of A,B;

coherence

for b

b

registration

let A, B be set ;

let X be Function-yielding_on_second ManySortedSet of A,B;

coherence

for b_{1} being Function st b_{1} = X `2 holds

b_{1} is Function-yielding
by Def6;

end;
let X be Function-yielding_on_second ManySortedSet of A,B;

coherence

for b

b

definition

let A, B be set ;

let f be ManySortedCategory of A;

let g be ManySortedFunction of B;

:: original: [

redefine func [f,g] -> Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;

coherence

[f,g] is Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B

end;
let f be ManySortedCategory of A;

let g be ManySortedFunction of B;

:: original: [

redefine func [f,g] -> Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B;

coherence

[f,g] is Category-yielding_on_first Function-yielding_on_second ManySortedSet of A,B

proof end;

definition

let A be non empty set ;

let F, G be ManySortedCategory of A;

ex b_{1} being ManySortedFunction of A st

for a being Element of A holds b_{1} . a is Functor of F . a,G . a

end;
let F, G be ManySortedCategory of A;

mode ManySortedFunctor of F,G -> ManySortedFunction of A means :Def7: :: INDEX_1:def 7

for a being Element of A holds it . a is Functor of F . a,G . a;

existence for a being Element of A holds it . a is Functor of F . a,G . a;

ex b

for a being Element of A holds b

proof end;

:: deftheorem Def7 defines ManySortedFunctor INDEX_1:def 7 :

for A being non empty set

for F, G being ManySortedCategory of A

for b_{4} being ManySortedFunction of A holds

( b_{4} is ManySortedFunctor of F,G iff for a being Element of A holds b_{4} . a is Functor of F . a,G . a );

for A being non empty set

for F, G being ManySortedCategory of A

for b

( b

scheme :: INDEX_1:sch 1

LambdaMSFr{ F_{1}() -> non empty set , F_{2}() -> ManySortedCategory of F_{1}(), F_{3}() -> ManySortedCategory of F_{1}(), F_{4}( object ) -> set } :

LambdaMSFr{ F

ex F being ManySortedFunctor of F_{2}(),F_{3}() st

for a being Element of F_{1}() holds F . a = F_{4}(a)

provided
for a being Element of F

proof end;

definition

let A be non empty set ;

let F, G be ManySortedCategory of A;

let f be ManySortedFunctor of F,G;

let a be Element of A;

:: original: .

redefine func f . a -> Functor of F . a,G . a;

coherence

f . a is Functor of F . a,G . a by Def7;

end;
let F, G be ManySortedCategory of A;

let f be ManySortedFunctor of F,G;

let a be Element of A;

:: original: .

redefine func f . a -> Functor of F . a,G . a;

coherence

f . a is Functor of F . a,G . a by Def7;

definition

let A, B be non empty set ;

let F, G be Function of B,A;

ex b_{1} being Category-yielding_on_first ManySortedSet of A,B st b_{1} `2 is ManySortedFunctor of (b_{1} `1) * F,(b_{1} `1) * G

end;
let F, G be Function of B,A;

mode Indexing of F,G -> Category-yielding_on_first ManySortedSet of A,B means :Def8: :: INDEX_1:def 8

it `2 is ManySortedFunctor of (it `1) * F,(it `1) * G;

existence it `2 is ManySortedFunctor of (it `1) * F,(it `1) * G;

ex b

proof end;

:: deftheorem Def8 defines Indexing INDEX_1:def 8 :

for A, B being non empty set

for F, G being Function of B,A

for b_{5} being Category-yielding_on_first ManySortedSet of A,B holds

( b_{5} is Indexing of F,G iff b_{5} `2 is ManySortedFunctor of (b_{5} `1) * F,(b_{5} `1) * G );

for A, B being non empty set

for F, G being Function of B,A

for b

( b

theorem Th4: :: INDEX_1:4

for A, B being non empty set

for F, G being Function of B,A

for I being Indexing of F,G

for m being Element of B holds (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)

for F, G being Function of B,A

for I being Indexing of F,G

for m being Element of B holds (I `2) . m is Functor of (I `1) . (F . m),(I `1) . (G . m)

proof end;

theorem :: INDEX_1:5

definition

let A, B be non empty set ;

let F, G be Function of B,A;

let I be Indexing of F,G;

:: original: `2

redefine func I `2 -> ManySortedFunctor of (I `1) * F,(I `1) * G;

coherence

I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G by Def8;

end;
let F, G be Function of B,A;

let I be Indexing of F,G;

:: original: `2

redefine func I `2 -> ManySortedFunctor of (I `1) * F,(I `1) * G;

coherence

I `2 is ManySortedFunctor of (I `1) * F,(I `1) * G by Def8;

Lm1: now :: thesis: for A, B being non empty set

for F, G being Function of B,A

for I being Indexing of F,G ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

for F, G being Function of B,A

for I being Indexing of F,G ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

let A, B be non empty set ; :: thesis: for F, G being Function of B,A

for I being Indexing of F,G ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

let F, G be Function of B,A; :: thesis: for I being Indexing of F,G ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

let I be Indexing of F,G; :: thesis: ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

consider C being strict Categorial full Category such that

A1: the carrier of C = rng (I `1) by CAT_5:20;

take C = C; :: thesis: ( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

A2: dom (I `1) = A by PARTFUN1:def 2;

hence for a being Element of A holds (I `1) . a is Object of C by A1, FUNCT_1:def 3; :: thesis: for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C

let b be Element of B; :: thesis: [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C

A3: (I `2) . b is Functor of (I `1) . (F . b),(I `1) . (G . b) by Th4;

( (I `1) . (F . b) is Object of C & (I `1) . (G . b) is Object of C ) by A2, A1, FUNCT_1:def 3;

hence [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C by A3, CAT_5:def 8; :: thesis: verum

end;
for I being Indexing of F,G ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

let F, G be Function of B,A; :: thesis: for I being Indexing of F,G ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

let I be Indexing of F,G; :: thesis: ex C being strict Categorial full Category st

( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

consider C being strict Categorial full Category such that

A1: the carrier of C = rng (I `1) by CAT_5:20;

take C = C; :: thesis: ( ( for a being Element of A holds (I `1) . a is Object of C ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C ) )

A2: dom (I `1) = A by PARTFUN1:def 2;

hence for a being Element of A holds (I `1) . a is Object of C by A1, FUNCT_1:def 3; :: thesis: for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C

let b be Element of B; :: thesis: [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C

A3: (I `2) . b is Functor of (I `1) . (F . b),(I `1) . (G . b) by Th4;

( (I `1) . (F . b) is Object of C & (I `1) . (G . b) is Object of C ) by A2, A1, FUNCT_1:def 3;

hence [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of C by A3, CAT_5:def 8; :: thesis: verum

definition

let A, B be non empty set ;

let F, G be Function of B,A;

let I be Indexing of F,G;

ex b_{1} being Categorial Category st

( ( for a being Element of A holds (I `1) . a is Object of b_{1} ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b_{1} ) )

end;
let F, G be Function of B,A;

let I be Indexing of F,G;

mode TargetCat of I -> Categorial Category means :Def9: :: INDEX_1:def 9

( ( for a being Element of A holds (I `1) . a is Object of it ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of it ) );

existence ( ( for a being Element of A holds (I `1) . a is Object of it ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of it ) );

ex b

( ( for a being Element of A holds (I `1) . a is Object of b

proof end;

:: deftheorem Def9 defines TargetCat INDEX_1:def 9 :

for A, B being non empty set

for F, G being Function of B,A

for I being Indexing of F,G

for b_{6} being Categorial Category holds

( b_{6} is TargetCat of I iff ( ( for a being Element of A holds (I `1) . a is Object of b_{6} ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b_{6} ) ) );

for A, B being non empty set

for F, G being Function of B,A

for I being Indexing of F,G

for b

( b

registration

let A, B be non empty set ;

let F, G be Function of B,A;

let I be Indexing of F,G;

ex b_{1} being TargetCat of I st

( b_{1} is full & b_{1} is strict )

end;
let F, G be Function of B,A;

let I be Indexing of F,G;

cluster non empty non void V55() strict Category-like V68() V69() V70() with_identities with_triple-like_morphisms Categorial full for TargetCat of I;

existence ex b

( b

proof end;

definition

let A, B be non empty set ;

let F, G be Function of B,A;

let c be PartFunc of [:B,B:],B;

let i be Function of A,B;

given C being Category such that A1: C = CatStr(# A,B,F,G,c #) ;

ex b_{1} being Indexing of F,G st

( ( for a being Element of A holds (b_{1} `2) . (i . a) = id ((b_{1} `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds

(b_{1} `2) . (c . [m2,m1]) = ((b_{1} `2) . m2) * ((b_{1} `2) . m1) ) )

end;
let F, G be Function of B,A;

let c be PartFunc of [:B,B:],B;

let i be Function of A,B;

given C being Category such that A1: C = CatStr(# A,B,F,G,c #) ;

mode Indexing of F,G,c,i -> Indexing of F,G means :Def10: :: INDEX_1:def 10

( ( for a being Element of A holds (it `2) . (i . a) = id ((it `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds

(it `2) . (c . [m2,m1]) = ((it `2) . m2) * ((it `2) . m1) ) );

existence ( ( for a being Element of A holds (it `2) . (i . a) = id ((it `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds

(it `2) . (c . [m2,m1]) = ((it `2) . m2) * ((it `2) . m1) ) );

ex b

( ( for a being Element of A holds (b

(b

proof end;

:: deftheorem Def10 defines Indexing INDEX_1:def 10 :

for A, B being non empty set

for F, G being Function of B,A

for c being PartFunc of [:B,B:],B

for i being Function of A,B st ex C being Category st C = CatStr(# A,B,F,G,c #) holds

for b_{7} being Indexing of F,G holds

( b_{7} is Indexing of F,G,c,i iff ( ( for a being Element of A holds (b_{7} `2) . (i . a) = id ((b_{7} `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds

(b_{7} `2) . (c . [m2,m1]) = ((b_{7} `2) . m2) * ((b_{7} `2) . m1) ) ) );

for A, B being non empty set

for F, G being Function of B,A

for c being PartFunc of [:B,B:],B

for i being Function of A,B st ex C being Category st C = CatStr(# A,B,F,G,c #) holds

for b

( b

(b

definition

let C be Category;

mode Indexing of C is Indexing of the Source of C, the Target of C, the Comp of C, IdMap C;

mode coIndexing of C is Indexing of the Target of C, the Source of C, ~ the Comp of C, IdMap C;

end;
mode Indexing of C is Indexing of the Source of C, the Target of C, the Comp of C, IdMap C;

mode coIndexing of C is Indexing of the Target of C, the Source of C, ~ the Comp of C, IdMap C;

theorem Th6: :: INDEX_1:6

for C being Category

for I being Indexing of the Source of C, the Target of C holds

( I is Indexing of C iff ( ( for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) ) & ( for m1, m2 being Morphism of C st dom m2 = cod m1 holds

(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) ) ) )

for I being Indexing of the Source of C, the Target of C holds

( I is Indexing of C iff ( ( for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) ) & ( for m1, m2 being Morphism of C st dom m2 = cod m1 holds

(I `2) . (m2 (*) m1) = ((I `2) . m2) * ((I `2) . m1) ) ) )

proof end;

theorem Th7: :: INDEX_1:7

for C being Category

for I being Indexing of the Target of C, the Source of C holds

( I is coIndexing of C iff ( ( for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) ) & ( for m1, m2 being Morphism of C st dom m2 = cod m1 holds

(I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2) ) ) )

for I being Indexing of the Target of C, the Source of C holds

( I is coIndexing of C iff ( ( for a being Object of C holds (I `2) . (id a) = id ((I `1) . a) ) & ( for m1, m2 being Morphism of C st dom m2 = cod m1 holds

(I `2) . (m2 (*) m1) = ((I `2) . m1) * ((I `2) . m2) ) ) )

proof end;

Lm2: for C being Category holds IdMap C = IdMap (C opp)

proof end;

theorem :: INDEX_1:8

theorem :: INDEX_1:9

for C being Category

for I being Indexing of C

for c1, c2 being Object of C st not Hom (c1,c2) is empty holds

for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c1,(I `1) . c2

for I being Indexing of C

for c1, c2 being Object of C st not Hom (c1,c2) is empty holds

for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c1,(I `1) . c2

proof end;

theorem :: INDEX_1:10

for C being Category

for I being coIndexing of C

for c1, c2 being Object of C st not Hom (c1,c2) is empty holds

for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c2,(I `1) . c1

for I being coIndexing of C

for c1, c2 being Object of C st not Hom (c1,c2) is empty holds

for m being Morphism of c1,c2 holds (I `2) . m is Functor of (I `1) . c2,(I `1) . c1

proof end;

definition

let C be Category;

let I be Indexing of C;

let T be TargetCat of I;

ex b_{1} being Functor of C,T st

for f being Morphism of C holds b_{1} . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)]

for b_{1}, b_{2} being Functor of C,T st ( for f being Morphism of C holds b_{1} . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) & ( for f being Morphism of C holds b_{2} . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) holds

b_{1} = b_{2}

end;
let I be Indexing of C;

let T be TargetCat of I;

func I -functor (C,T) -> Functor of C,T means :Def11: :: INDEX_1:def 11

for f being Morphism of C holds it . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)];

existence for f being Morphism of C holds it . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)];

ex b

for f being Morphism of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines -functor INDEX_1:def 11 :

for C being Category

for I being Indexing of C

for T being TargetCat of I

for b_{4} being Functor of C,T holds

( b_{4} = I -functor (C,T) iff for f being Morphism of C holds b_{4} . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] );

for C being Category

for I being Indexing of C

for T being TargetCat of I

for b

( b

Lm3: for C being Category

for I being Indexing of C

for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1

proof end;

theorem Th11: :: INDEX_1:11

for C being Category

for I being Indexing of C

for T1, T2 being TargetCat of I holds

( I -functor (C,T1) = I -functor (C,T2) & Obj (I -functor (C,T1)) = Obj (I -functor (C,T2)) )

for I being Indexing of C

for T1, T2 being TargetCat of I holds

( I -functor (C,T1) = I -functor (C,T2) & Obj (I -functor (C,T1)) = Obj (I -functor (C,T2)) )

proof end;

theorem :: INDEX_1:12

theorem :: INDEX_1:13

definition

let C be Category;

let I be Indexing of C;

for b_{1}, b_{2} being strict TargetCat of I st ( for T being TargetCat of I holds b_{1} = Image (I -functor (C,T)) ) & ( for T being TargetCat of I holds b_{2} = Image (I -functor (C,T)) ) holds

b_{1} = b_{2}

ex b_{1} being strict TargetCat of I st

for T being TargetCat of I holds b_{1} = Image (I -functor (C,T))

end;
let I be Indexing of C;

func rng I -> strict TargetCat of I means :Def12: :: INDEX_1:def 12

for T being TargetCat of I holds it = Image (I -functor (C,T));

uniqueness for T being TargetCat of I holds it = Image (I -functor (C,T));

for b

b

proof end;

existence ex b

for T being TargetCat of I holds b

proof end;

:: deftheorem Def12 defines rng INDEX_1:def 12 :

for C being Category

for I being Indexing of C

for b_{3} being strict TargetCat of I holds

( b_{3} = rng I iff for T being TargetCat of I holds b_{3} = Image (I -functor (C,T)) );

for C being Category

for I being Indexing of C

for b

( b

theorem Th14: :: INDEX_1:14

for C being Category

for I being Indexing of C

for D being Categorial Category holds

( rng I is Subcategory of D iff D is TargetCat of I )

for I being Indexing of C

for D being Categorial Category holds

( rng I is Subcategory of D iff D is TargetCat of I )

proof end;

definition

let C be Category;

let I be Indexing of C;

let m be Morphism of C;

coherence

(I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m)

end;
let I be Indexing of C;

let m be Morphism of C;

coherence

(I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m)

proof end;

:: deftheorem defines . INDEX_1:def 13 :

for C being Category

for I being Indexing of C

for m being Morphism of C holds I . m = (I `2) . m;

for C being Category

for I being Indexing of C

for m being Morphism of C holds I . m = (I `2) . m;

definition

let C be Category;

let I be coIndexing of C;

let m be Morphism of C;

coherence

(I `2) . m is Functor of (I `1) . (cod m),(I `1) . (dom m)

end;
let I be coIndexing of C;

let m be Morphism of C;

coherence

(I `2) . m is Functor of (I `1) . (cod m),(I `1) . (dom m)

proof end;

:: deftheorem defines . INDEX_1:def 14 :

for C being Category

for I being coIndexing of C

for m being Morphism of C holds I . m = (I `2) . m;

for C being Category

for I being coIndexing of C

for m being Morphism of C holds I . m = (I `2) . m;

Lm4: now :: thesis: for C, D being Category

for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m

for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m

let C, D be Category; :: thesis: for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m

set F = the carrier of C --> D;

set G = the carrier' of C --> (id D);

set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];

let m be Morphism of C; :: thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def 2;

then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Source of C . m)

.= D by FUNCOP_1:7 ;

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def 2;

then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Target of C . m)

.= D by FUNCOP_1:7 ;

([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m

.= id D by FUNCOP_1:7 ;

hence ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m by A1, A2; :: thesis: verum

end;
set F = the carrier of C --> D;

set G = the carrier' of C --> (id D);

set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];

let m be Morphism of C; :: thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def 2;

then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Source of C . m)

.= D by FUNCOP_1:7 ;

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def 2;

then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Target of C . m)

.= D by FUNCOP_1:7 ;

([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m

.= id D by FUNCOP_1:7 ;

hence ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m by A1, A2; :: thesis: verum

Lm5: now :: thesis: for C, D being Category

for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m

for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m

let C, D be Category; :: thesis: for m being Morphism of C holds ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m

set F = the carrier of C --> D;

set G = the carrier' of C --> (id D);

set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];

let m be Morphism of C; :: thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def 2;

then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Source of C . m)

.= D by FUNCOP_1:7 ;

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def 2;

then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Target of C . m)

.= D by FUNCOP_1:7 ;

([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m

.= id D by FUNCOP_1:7 ;

hence ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m by A1, A2; :: thesis: verum

end;
set F = the carrier of C --> D;

set G = the carrier' of C --> (id D);

set H = [( the carrier of C --> D),( the carrier' of C --> (id D))];

let m be Morphism of C; :: thesis: ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) = the carrier' of C by PARTFUN1:def 2;

then A1: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Source of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Source of C . m)

.= D by FUNCOP_1:7 ;

dom (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) = the carrier' of C by PARTFUN1:def 2;

then A2: (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m = ([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) . ( the Target of C . m) by FUNCT_1:12

.= ( the carrier of C --> D) . ( the Target of C . m)

.= D by FUNCOP_1:7 ;

([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m = ( the carrier' of C --> (id D)) . m

.= id D by FUNCOP_1:7 ;

hence ([( the carrier of C --> D),( the carrier' of C --> (id D))] `2) . m is Functor of (([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Target of C) . m,(([( the carrier of C --> D),( the carrier' of C --> (id D))] `1) * the Source of C) . m by A1, A2; :: thesis: verum

theorem :: INDEX_1:15

for C, D being Category holds

( [( the carrier of C --> D),( the carrier' of C --> (id D))] is Indexing of C & [( the carrier of C --> D),( the carrier' of C --> (id D))] is coIndexing of C )

( [( the carrier of C --> D),( the carrier' of C --> (id D))] is Indexing of C & [( the carrier of C --> D),( the carrier' of C --> (id D))] is coIndexing of C )

proof end;

registration

let C be Category;

let D be Categorial Category;

let F be Functor of C,D;

coherence

Obj F is Category-yielding

end;
let D be Categorial Category;

let F be Functor of C,D;

coherence

Obj F is Category-yielding

proof end;

theorem Th16: :: INDEX_1:16

for C being Category

for D being Categorial Category

for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C

for D being Categorial Category

for F being Functor of C,D holds [(Obj F),(pr2 F)] is Indexing of C

proof end;

definition

let C be Category;

let D be Categorial Category;

let F be Functor of C,D;

coherence

[(Obj F),(pr2 F)] is Indexing of C by Th16;

end;
let D be Categorial Category;

let F be Functor of C,D;

coherence

[(Obj F),(pr2 F)] is Indexing of C by Th16;

:: deftheorem defines -indexing_of INDEX_1:def 15 :

for C being Category

for D being Categorial Category

for F being Functor of C,D holds F -indexing_of C = [(Obj F),(pr2 F)];

for C being Category

for D being Categorial Category

for F being Functor of C,D holds F -indexing_of C = [(Obj F),(pr2 F)];

theorem :: INDEX_1:17

for C being Category

for D being Categorial Category

for F being Functor of C,D holds D is TargetCat of F -indexing_of C

for D being Categorial Category

for F being Functor of C,D holds D is TargetCat of F -indexing_of C

proof end;

theorem Th18: :: INDEX_1:18

for C being Category

for D being Categorial Category

for F being Functor of C,D

for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)

for D being Categorial Category

for F being Functor of C,D

for T being TargetCat of F -indexing_of C holds F = (F -indexing_of C) -functor (C,T)

proof end;

theorem :: INDEX_1:19

for C being Category

for D, E being Categorial Category

for F being Functor of C,D

for G being Functor of C,E st F = G holds

F -indexing_of C = G -indexing_of C by Th2;

for D, E being Categorial Category

for F being Functor of C,D

for G being Functor of C,E st F = G holds

F -indexing_of C = G -indexing_of C by Th2;

theorem Th20: :: INDEX_1:20

for C being Category

for I being Indexing of C

for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2

for I being Indexing of C

for T being TargetCat of I holds pr2 (I -functor (C,T)) = I `2

proof end;

theorem :: INDEX_1:21

for C being Category

for I being Indexing of C

for T being TargetCat of I holds (I -functor (C,T)) -indexing_of C = I

for I being Indexing of C

for T being TargetCat of I holds (I -functor (C,T)) -indexing_of C = I

proof end;

Lm6: now :: thesis: for c, d being Category

for e being Subcategory of d

for f being Functor of c,e holds f is Functor of c,d

for e being Subcategory of d

for f being Functor of c,e holds f is Functor of c,d

let c, d be Category; :: thesis: for e being Subcategory of d

for f being Functor of c,e holds f is Functor of c,d

let e be Subcategory of d; :: thesis: for f being Functor of c,e holds f is Functor of c,d

let f be Functor of c,e; :: thesis: f is Functor of c,d

(incl e) * f = (id e) * f by CAT_2:def 5

.= f by FUNCT_2:17 ;

hence f is Functor of c,d ; :: thesis: verum

end;
for f being Functor of c,e holds f is Functor of c,d

let e be Subcategory of d; :: thesis: for f being Functor of c,e holds f is Functor of c,d

let f be Functor of c,e; :: thesis: f is Functor of c,d

(incl e) * f = (id e) * f by CAT_2:def 5

.= f by FUNCT_2:17 ;

hence f is Functor of c,d ; :: thesis: verum

definition

let C, D, E be Category;

let F be Functor of C,D;

let I be Indexing of E;

assume A1: Image F is Subcategory of E ;

ex b_{1} being Indexing of C st

for F9 being Functor of C,E st F9 = F holds

b_{1} = ((I -functor (E,(rng I))) * F9) -indexing_of C

for b_{1}, b_{2} being Indexing of C st ( for F9 being Functor of C,E st F9 = F holds

b_{1} = ((I -functor (E,(rng I))) * F9) -indexing_of C ) & ( for F9 being Functor of C,E st F9 = F holds

b_{2} = ((I -functor (E,(rng I))) * F9) -indexing_of C ) holds

b_{1} = b_{2}

end;
let F be Functor of C,D;

let I be Indexing of E;

assume A1: Image F is Subcategory of E ;

func I * F -> Indexing of C means :Def16: :: INDEX_1:def 16

for F9 being Functor of C,E st F9 = F holds

it = ((I -functor (E,(rng I))) * F9) -indexing_of C;

existence for F9 being Functor of C,E st F9 = F holds

it = ((I -functor (E,(rng I))) * F9) -indexing_of C;

ex b

for F9 being Functor of C,E st F9 = F holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def16 defines * INDEX_1:def 16 :

for C, D, E being Category

for F being Functor of C,D

for I being Indexing of E st Image F is Subcategory of E holds

for b_{6} being Indexing of C holds

( b_{6} = I * F iff for F9 being Functor of C,E st F9 = F holds

b_{6} = ((I -functor (E,(rng I))) * F9) -indexing_of C );

for C, D, E being Category

for F being Functor of C,D

for I being Indexing of E st Image F is Subcategory of E holds

for b

( b

b

theorem Th22: :: INDEX_1:22

for C, D1, D2, E being Category

for I being Indexing of E

for F being Functor of C,D1

for G being Functor of C,D2 st Image F is Subcategory of E & Image G is Subcategory of E & F = G holds

I * F = I * G

for I being Indexing of E

for F being Functor of C,D1

for G being Functor of C,D2 st Image F is Subcategory of E & Image G is Subcategory of E & F = G holds

I * F = I * G

proof end;

theorem Th23: :: INDEX_1:23

for C, D being Category

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I holds I * F = ((I -functor (D,T)) * F) -indexing_of C

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I holds I * F = ((I -functor (D,T)) * F) -indexing_of C

proof end;

theorem Th24: :: INDEX_1:24

for C, D being Category

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I holds T is TargetCat of I * F

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I holds T is TargetCat of I * F

proof end;

theorem :: INDEX_1:25

for C, D being Category

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I holds rng (I * F) is Subcategory of T

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I holds rng (I * F) is Subcategory of T

proof end;

theorem Th26: :: INDEX_1:26

for C, D, E being Category

for F being Functor of C,D

for G being Functor of D,E

for I being Indexing of E holds (I * G) * F = I * (G * F)

for F being Functor of C,D

for G being Functor of D,E

for I being Indexing of E holds (I * G) * F = I * (G * F)

proof end;

definition

let C be Category;

let I be Indexing of C;

let D be Categorial Category;

assume A1: D is TargetCat of I ;

let E be Categorial Category;

let F be Functor of D,E;

ex b_{1} being Indexing of C st

for T being TargetCat of I

for G being Functor of T,E st T = D & G = F holds

b_{1} = (G * (I -functor (C,T))) -indexing_of C

for b_{1}, b_{2} being Indexing of C st ( for T being TargetCat of I

for G being Functor of T,E st T = D & G = F holds

b_{1} = (G * (I -functor (C,T))) -indexing_of C ) & ( for T being TargetCat of I

for G being Functor of T,E st T = D & G = F holds

b_{2} = (G * (I -functor (C,T))) -indexing_of C ) holds

b_{1} = b_{2}

end;
let I be Indexing of C;

let D be Categorial Category;

assume A1: D is TargetCat of I ;

let E be Categorial Category;

let F be Functor of D,E;

func F * I -> Indexing of C means :Def17: :: INDEX_1:def 17

for T being TargetCat of I

for G being Functor of T,E st T = D & G = F holds

it = (G * (I -functor (C,T))) -indexing_of C;

existence for T being TargetCat of I

for G being Functor of T,E st T = D & G = F holds

it = (G * (I -functor (C,T))) -indexing_of C;

ex b

for T being TargetCat of I

for G being Functor of T,E st T = D & G = F holds

b

proof end;

uniqueness for b

for G being Functor of T,E st T = D & G = F holds

b

for G being Functor of T,E st T = D & G = F holds

b

b

proof end;

:: deftheorem Def17 defines * INDEX_1:def 17 :

for C being Category

for I being Indexing of C

for D being Categorial Category st D is TargetCat of I holds

for E being Categorial Category

for F being Functor of D,E

for b_{6} being Indexing of C holds

( b_{6} = F * I iff for T being TargetCat of I

for G being Functor of T,E st T = D & G = F holds

b_{6} = (G * (I -functor (C,T))) -indexing_of C );

for C being Category

for I being Indexing of C

for D being Categorial Category st D is TargetCat of I holds

for E being Categorial Category

for F being Functor of D,E

for b

( b

for G being Functor of T,E st T = D & G = F holds

b

theorem Th27: :: INDEX_1:27

for C being Category

for I being Indexing of C

for T being TargetCat of I

for D, E being Categorial Category

for F being Functor of T,D

for G being Functor of T,E st F = G holds

F * I = G * I

for I being Indexing of C

for T being TargetCat of I

for D, E being Categorial Category

for F being Functor of T,D

for G being Functor of T,E st F = G holds

F * I = G * I

proof end;

theorem Th28: :: INDEX_1:28

for C being Category

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D holds Image F is TargetCat of F * I

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D holds Image F is TargetCat of F * I

proof end;

theorem Th29: :: INDEX_1:29

for C being Category

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D holds D is TargetCat of F * I

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D holds D is TargetCat of F * I

proof end;

theorem :: INDEX_1:30

for C being Category

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D holds rng (F * I) is Subcategory of Image F

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D holds rng (F * I) is Subcategory of Image F

proof end;

theorem :: INDEX_1:31

for C being Category

for I being Indexing of C

for T being TargetCat of I

for D, E being Categorial Category

for F being Functor of T,D

for G being Functor of D,E holds (G * F) * I = G * (F * I)

for I being Indexing of C

for T being TargetCat of I

for D, E being Categorial Category

for F being Functor of T,D

for G being Functor of D,E holds (G * F) * I = G * (F * I)

proof end;

definition

let C, D be Category;

let I1 be Indexing of C;

let I2 be Indexing of D;

correctness

coherence

I2 * (I1 -functor (C,(rng I1))) is Indexing of C;

;

end;
let I1 be Indexing of C;

let I2 be Indexing of D;

correctness

coherence

I2 * (I1 -functor (C,(rng I1))) is Indexing of C;

;

:: deftheorem defines * INDEX_1:def 18 :

for C, D being Category

for I1 being Indexing of C

for I2 being Indexing of D holds I2 * I1 = I2 * (I1 -functor (C,(rng I1)));

for C, D being Category

for I1 being Indexing of C

for I2 being Indexing of D holds I2 * I1 = I2 * (I1 -functor (C,(rng I1)));

theorem Th32: :: INDEX_1:32

for C being Category

for D being Categorial Category

for I1 being Indexing of C

for I2 being Indexing of D

for T being TargetCat of I1 st D is TargetCat of I1 holds

I2 * I1 = I2 * (I1 -functor (C,T))

for D being Categorial Category

for I1 being Indexing of C

for I2 being Indexing of D

for T being TargetCat of I1 st D is TargetCat of I1 holds

I2 * I1 = I2 * (I1 -functor (C,T))

proof end;

theorem :: INDEX_1:33

for C being Category

for D being Categorial Category

for I1 being Indexing of C

for I2 being Indexing of D

for T being TargetCat of I2 st D is TargetCat of I1 holds

I2 * I1 = (I2 -functor (D,T)) * I1

for D being Categorial Category

for I1 being Indexing of C

for I2 being Indexing of D

for T being TargetCat of I2 st D is TargetCat of I1 holds

I2 * I1 = (I2 -functor (D,T)) * I1

proof end;

theorem Th34: :: INDEX_1:34

for C, D being Category

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I

for E being Categorial Category

for G being Functor of T,E holds (G * I) * F = G * (I * F)

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I

for E being Categorial Category

for G being Functor of T,E holds (G * I) * F = G * (I * F)

proof end;

theorem :: INDEX_1:35

for C being Category

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D

for J being Indexing of D holds (J * F) * I = J * (F * I)

for I being Indexing of C

for T being TargetCat of I

for D being Categorial Category

for F being Functor of T,D

for J being Indexing of D holds (J * F) * I = J * (F * I)

proof end;

theorem :: INDEX_1:36

for C being Category

for I being Indexing of C

for T1 being TargetCat of I

for J being Indexing of T1

for T2 being TargetCat of J

for D being Categorial Category

for F being Functor of T2,D holds (F * J) * I = F * (J * I)

for I being Indexing of C

for T1 being TargetCat of I

for J being Indexing of T1

for T2 being TargetCat of J

for D being Categorial Category

for F being Functor of T2,D holds (F * J) * I = F * (J * I)

proof end;

theorem Th37: :: INDEX_1:37

for C, D being Category

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I

for J being Indexing of T holds (J * I) * F = J * (I * F)

for F being Functor of C,D

for I being Indexing of D

for T being TargetCat of I

for J being Indexing of T holds (J * I) * F = J * (I * F)

proof end;

theorem :: INDEX_1:38

for C being Category

for I being Indexing of C

for D being TargetCat of I

for J being Indexing of D

for E being TargetCat of J

for K being Indexing of E holds (K * J) * I = K * (J * I)

for I being Indexing of C

for D being TargetCat of I

for J being Indexing of D

for E being TargetCat of J

for K being Indexing of E holds (K * J) * I = K * (J * I)

proof end;