:: Indexed Category
:: by Grzegorz Bancerek
::
:: Received June 8, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users


registration
let A be non empty set ;
cluster non empty Relation-like V9() A -defined Function-like total for set ;
existence
not for b1 being ManySortedSet of A holds b1 is V9()
proof end;
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
proof end;
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))]
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
proof end;

definition
let IT be Function;
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;
end;

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

registration
cluster Relation-like Function-like Category-yielding for set ;
existence
ex b1 being Function st b1 is Category-yielding
proof end;
end;

registration
let X be set ;
cluster Relation-like X -defined Function-like total Category-yielding for set ;
existence
ex b1 being ManySortedSet of X st b1 is Category-yielding
proof end;
end;

definition
let A be set ;
mode ManySortedCategory of A is Category-yielding ManySortedSet of A;
end;

definition
let C be Category;
mode ManySortedCategory of C is ManySortedCategory of the carrier of C;
end;

registration
let X be set ;
let x be Category;
cluster X --> x -> Category-yielding ;
coherence
X --> x is Category-yielding by FUNCOP_1:7;
end;

registration
let X be non empty set ;
cluster Relation-like X -defined Function-like total -> non empty for set ;
coherence
for b1 being ManySortedSet of X holds not b1 is empty ;
end;

registration
let f be Category-yielding Function;
cluster proj2 f -> categorial ;
coherence
rng f is categorial
proof end;
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
proof end;
end;

registration
let f be Function;
let g be Category-yielding Function;
cluster f * g -> Category-yielding ;
coherence
g * f is Category-yielding
proof end;
end;

:: carrier and Morphisms
definition
let F be Category-yielding Function;
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
ex b1 being non-empty Function st
( dom b1 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the carrier of C ) )
proof end;
uniqueness
for b1, b2 being non-empty Function st dom b1 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the carrier of C ) & dom b2 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the carrier of C ) holds
b1 = b2
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
ex b1 being non-empty Function st
( dom b1 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the carrier' of C ) )
proof end;
uniqueness
for b1, b2 being non-empty Function st dom b1 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b1 . x = the carrier' of C ) & dom b2 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the carrier' of C ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Objs INDEX_1:def 2 :
for F being Category-yielding Function
for b2 being non-empty Function holds
( b2 = Objs F iff ( dom b2 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the carrier of C ) ) );

:: deftheorem Def3 defines Mphs INDEX_1:def 3 :
for F being Category-yielding Function
for b2 being non-empty Function holds
( b2 = Mphs F iff ( dom b2 = dom F & ( for x being object st x in dom F holds
for C being Category st C = F . x holds
b2 . x = the carrier' of C ) ) );

registration
let A be non empty set ;
let F be ManySortedCategory of A;
cluster Objs F -> non-empty A -defined ;
coherence
Objs F is A -defined
proof end;
cluster Mphs F -> non-empty A -defined ;
coherence
Mphs F is A -defined
proof end;
end;

registration
let A be non empty set ;
let F be ManySortedCategory of A;
cluster Objs F -> non-empty total ;
coherence
Objs F is total
proof end;
cluster Mphs F -> non-empty total ;
coherence
Mphs F is total
proof end;
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 )
proof end;

definition
let A, B be set ;
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 b1 being object ex f being ManySortedSet of A ex g being ManySortedSet of B st b1 = [f,g]
proof end;
end;

:: deftheorem Def4 defines ManySortedSet INDEX_1:def 4 :
for A, B being set
for b3 being object holds
( b3 is ManySortedSet of A,B iff ex f being ManySortedSet of A ex g being ManySortedSet of B st b3 = [f,g] );

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
proof end;
end;

registration
let A, B be set ;
let X be ManySortedSet of A,B;
cluster X `1 -> Relation-like Function-like for set ;
coherence
for b1 being set st b1 = X `1 holds
( b1 is Function-like & b1 is Relation-like )
proof end;
cluster X `2 -> Relation-like Function-like for set ;
coherence
for b1 being set st b1 = X `2 holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

registration
let A, B be set ;
let X be ManySortedSet of A,B;
cluster X `1 -> A -defined for Relation;
coherence
for b1 being Relation st b1 = X `1 holds
b1 is A -defined
proof end;
cluster X `2 -> B -defined for Relation;
coherence
for b1 being Relation st b1 = X `2 holds
b1 is B -defined
proof end;
end;

registration
let A, B be set ;
let X be ManySortedSet of A,B;
cluster X `1 -> A -defined total for A -defined Function;
coherence
for b1 being A -defined Function st b1 = X `1 holds
b1 is total
proof end;
cluster X `2 -> B -defined total for B -defined Function;
coherence
for b1 being B -defined Function st b1 = X `2 holds
b1 is total
proof end;
end;

definition
let A, B be set ;
let IT be ManySortedSet of A,B;
attr IT is Category-yielding_on_first means :Def5: :: INDEX_1:def 5
IT `1 is Category-yielding ;
attr IT is Function-yielding_on_second means :Def6: :: INDEX_1:def 6
IT `2 is Function-yielding ;
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 );

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

registration
let A, B be set ;
cluster Category-yielding_on_first Function-yielding_on_second for ManySortedSet of A,B;
existence
ex b1 being ManySortedSet of A,B st
( b1 is Category-yielding_on_first & b1 is Function-yielding_on_second )
proof end;
end;

registration
let A, B be set ;
let X be Category-yielding_on_first ManySortedSet of A,B;
cluster X `1 -> Category-yielding for Function;
coherence
for b1 being Function st b1 = X `1 holds
b1 is Category-yielding by Def5;
end;

registration
let A, B be set ;
let X be Function-yielding_on_second ManySortedSet of A,B;
cluster X `2 -> Function-yielding for Function;
coherence
for b1 being Function st b1 = X `2 holds
b1 is Function-yielding by Def6;
end;

registration
let f be Function-yielding Function;
cluster proj2 f -> functional ;
coherence
rng f is functional
proof end;
end;

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
proof end;
end;

definition
let A be non empty set ;
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
ex b1 being ManySortedFunction of A st
for a being Element of A holds b1 . a is Functor of F . a,G . a
proof end;
end;

:: deftheorem Def7 defines ManySortedFunctor INDEX_1:def 7 :
for A being non empty set
for F, G being ManySortedCategory of A
for b4 being ManySortedFunction of A holds
( b4 is ManySortedFunctor of F,G iff for a being Element of A holds b4 . a is Functor of F . a,G . a );

scheme :: INDEX_1:sch 1
LambdaMSFr{ F1() -> non empty set , F2() -> ManySortedCategory of F1(), F3() -> ManySortedCategory of F1(), F4( object ) -> set } :
ex F being ManySortedFunctor of F2(),F3() st
for a being Element of F1() holds F . a = F4(a)
provided
A1: for a being Element of F1() holds F4(a) is Functor of F2() . a,F3() . a
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;

definition
let A, B be non empty set ;
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
ex b1 being Category-yielding_on_first ManySortedSet of A,B st b1 `2 is ManySortedFunctor of (b1 `1) * F,(b1 `1) * G
proof end;
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 b5 being Category-yielding_on_first ManySortedSet of A,B holds
( b5 is Indexing of F,G iff b5 `2 is ManySortedFunctor of (b5 `1) * F,(b5 `1) * G );

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)
proof end;

theorem :: INDEX_1:5
for C being Category
for I being Indexing of the Source of C, the Target of C
for m being Morphism of C holds (I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m) by Th4;

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;

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

definition
let A, B be non empty set ;
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
ex b1 being Categorial Category st
( ( for a being Element of A holds (I `1) . a is Object of b1 ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b1 ) )
proof end;
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 b6 being Categorial Category holds
( b6 is TargetCat of I iff ( ( for a being Element of A holds (I `1) . a is Object of b6 ) & ( for b being Element of B holds [[((I `1) . (F . b)),((I `1) . (G . b))],((I `2) . b)] is Morphism of b6 ) ) );

registration
let A, B be non empty set ;
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 b1 being TargetCat of I st
( b1 is full & b1 is strict )
proof end;
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 #) ;
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
ex b1 being Indexing of F,G st
( ( for a being Element of A holds (b1 `2) . (i . a) = id ((b1 `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b1 `2) . (c . [m2,m1]) = ((b1 `2) . m2) * ((b1 `2) . m1) ) )
proof end;
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 b7 being Indexing of F,G holds
( b7 is Indexing of F,G,c,i iff ( ( for a being Element of A holds (b7 `2) . (i . a) = id ((b7 `1) . a) ) & ( for m1, m2 being Element of B st F . m2 = G . m1 holds
(b7 `2) . (c . [m2,m1]) = ((b7 `2) . m2) * ((b7 `2) . m1) ) ) );

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;

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) ) ) )
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) ) ) )
proof end;

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

theorem :: INDEX_1:8
for C being Category
for x being set holds
( x is coIndexing of C iff x is Indexing of (C opp) ) by Lm2;

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
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
proof end;

definition
let C be Category;
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
ex b1 being Functor of C,T st
for f being Morphism of C holds b1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)]
proof end;
uniqueness
for b1, b2 being Functor of C,T st ( for f being Morphism of C holds b1 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) & ( for f being Morphism of C holds b2 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] ) holds
b1 = b2
proof end;
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 b4 being Functor of C,T holds
( b4 = I -functor (C,T) iff for f being Morphism of C holds b4 . f = [[((I `1) . (dom f)),((I `1) . (cod f))],((I `2) . f)] );

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)) )
proof end;

theorem :: INDEX_1:12
for C being Category
for I being Indexing of C
for T being TargetCat of I holds Obj (I -functor (C,T)) = I `1 by Lm3;

theorem :: INDEX_1:13
for C being Category
for I being Indexing of C
for T being TargetCat of I
for x being Object of C holds (I -functor (C,T)) . x = (I `1) . x by Lm3;

definition
let C be Category;
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 b1, b2 being strict TargetCat of I st ( for T being TargetCat of I holds b1 = Image (I -functor (C,T)) ) & ( for T being TargetCat of I holds b2 = Image (I -functor (C,T)) ) holds
b1 = b2
proof end;
existence
ex b1 being strict TargetCat of I st
for T being TargetCat of I holds b1 = Image (I -functor (C,T))
proof end;
end;

:: deftheorem Def12 defines rng INDEX_1:def 12 :
for C being Category
for I being Indexing of C
for b3 being strict TargetCat of I holds
( b3 = rng I iff for T being TargetCat of I holds b3 = Image (I -functor (C,T)) );

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 )
proof end;

definition
let C be Category;
let I be Indexing of C;
let m be Morphism of C;
func I . m -> Functor of (I `1) . (dom m),(I `1) . (cod m) equals :: INDEX_1:def 13
(I `2) . m;
coherence
(I `2) . m is Functor of (I `1) . (dom m),(I `1) . (cod m)
proof end;
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;

definition
let C be Category;
let I be coIndexing of C;
let m be Morphism of C;
func I . m -> Functor of (I `1) . (cod m),(I `1) . (dom m) equals :: INDEX_1:def 14
(I `2) . m;
coherence
(I `2) . m is Functor of (I `1) . (cod m),(I `1) . (dom m)
proof end;
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;

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
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 ;
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 ;
thus ([( 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;

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
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 ;
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 ;
thus ([( 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;

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 )
proof end;

registration
let C be Category;
let D be Categorial Category;
let F be Functor of C,D;
cluster Obj F -> Category-yielding ;
coherence
Obj F is Category-yielding
proof end;
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
proof end;

definition
let C be Category;
let D be Categorial Category;
let F be Functor of C,D;
func F -indexing_of C -> Indexing of C equals :: INDEX_1:def 15
[(Obj F),(pr2 F)];
coherence
[(Obj F),(pr2 F)] is Indexing of C by Th16;
end;

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

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

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

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 ;
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
ex b1 being Indexing of C st
for F9 being Functor of C,E st F9 = F holds
b1 = ((I -functor (E,(rng I))) * F9) -indexing_of C
proof end;
uniqueness
for b1, b2 being Indexing of C st ( for F9 being Functor of C,E st F9 = F holds
b1 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) & ( for F9 being Functor of C,E st F9 = F holds
b2 = ((I -functor (E,(rng I))) * F9) -indexing_of C ) holds
b1 = b2
proof end;
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 b6 being Indexing of C holds
( b6 = I * F iff for F9 being Functor of C,E st F9 = F holds
b6 = ((I -functor (E,(rng I))) * F9) -indexing_of C );

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
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
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
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
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)
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;
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
ex b1 being Indexing of C st
for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b1 = (G * (I -functor (C,T))) -indexing_of C
proof end;
uniqueness
for b1, b2 being Indexing of C st ( for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b1 = (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
b2 = (G * (I -functor (C,T))) -indexing_of C ) holds
b1 = b2
proof end;
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 b6 being Indexing of C holds
( b6 = F * I iff for T being TargetCat of I
for G being Functor of T,E st T = D & G = F holds
b6 = (G * (I -functor (C,T))) -indexing_of C );

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
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
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
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
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)
proof end;

definition
let C, D be Category;
let I1 be Indexing of C;
let I2 be Indexing of D;
func I2 * I1 -> Indexing of C equals :: INDEX_1:def 18
I2 * (I1 -functor (C,(rng I1)));
correctness
coherence
I2 * (I1 -functor (C,(rng I1))) is Indexing of C;
;
end;

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

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))
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
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)
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)
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)
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)
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)
proof end;

theorem :: INDEX_1:39
for C being Category holds IdMap C = IdMap (C opp) by Lm2;