:: Coherent Space
:: by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received December 29, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

:: Coherent Space and Web of Coherent Space
definition
let IT be set ;
attr IT is binary_complete means :Def1: :: COH_SP:def 1
for A being set st A c= IT & ( for a, b being set st a in A & b in A holds
a \/ b in IT ) holds
union A in IT;
end;

:: deftheorem Def1 defines binary_complete COH_SP:def 1 :
for IT being set holds
( IT is binary_complete iff for A being set st A c= IT & ( for a, b being set st a in A & b in A holds
a \/ b in IT ) holds
union A in IT );

registration
cluster non empty subset-closed binary_complete for set ;
existence
ex b1 being set st
( b1 is subset-closed & b1 is binary_complete & not b1 is empty )
proof end;
end;

definition
mode Coherence_Space is non empty subset-closed binary_complete set ;
end;

theorem :: COH_SP:1
for C being Coherence_Space holds {} in C
proof end;

theorem Th2: :: COH_SP:2
for X being set holds bool X is Coherence_Space
proof end;

theorem :: COH_SP:3
{{}} is Coherence_Space by Th2, ZFMISC_1:1;

theorem Th4: :: COH_SP:4
for x being set
for C being Coherence_Space st x in union C holds
{x} in C
proof end;

definition
let C be Coherence_Space;
func Web C -> Tolerance of (union C) means :Def2: :: COH_SP:def 2
for x, y being set holds
( [x,y] in it iff ex X being set st
( X in C & x in X & y in X ) );
existence
ex b1 being Tolerance of (union C) st
for x, y being set holds
( [x,y] in b1 iff ex X being set st
( X in C & x in X & y in X ) )
proof end;
uniqueness
for b1, b2 being Tolerance of (union C) st ( for x, y being set holds
( [x,y] in b1 iff ex X being set st
( X in C & x in X & y in X ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex X being set st
( X in C & x in X & y in X ) ) ) holds
b1 = b2
by TOLER_1:25;
end;

:: deftheorem Def2 defines Web COH_SP:def 2 :
for C being Coherence_Space
for b2 being Tolerance of (union C) holds
( b2 = Web C iff for x, y being set holds
( [x,y] in b2 iff ex X being set st
( X in C & x in X & y in X ) ) );

theorem Th5: :: COH_SP:5
for C being Coherence_Space
for T being Tolerance of (union C) holds
( T = Web C iff for x, y being set holds
( [x,y] in T iff {x,y} in C ) )
proof end;

theorem Th6: :: COH_SP:6
for a being set
for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
{x,y} in C )
proof end;

theorem Th7: :: COH_SP:7
for a being set
for C being Coherence_Space holds
( a in C iff for x, y being set st x in a & y in a holds
[x,y] in Web C )
proof end;

theorem :: COH_SP:8
for a being set
for C being Coherence_Space st ( for x, y being set st x in a & y in a holds
{x,y} in C ) holds
a c= union C
proof end;

theorem :: COH_SP:9
for C, D being Coherence_Space st Web C = Web D holds
C = D
proof end;

theorem :: COH_SP:10
for C being Coherence_Space st union C in C holds
C = bool (union C)
proof end;

theorem :: COH_SP:11
for C being Coherence_Space st C = bool (union C) holds
Web C = Total (union C)
proof end;

definition
let X be set ;
let E be Tolerance of X;
func CohSp E -> Coherence_Space means :Def3: :: COH_SP:def 3
for a being set holds
( a in it iff for x, y being set st x in a & y in a holds
[x,y] in E );
existence
ex b1 being Coherence_Space st
for a being set holds
( a in b1 iff for x, y being set st x in a & y in a holds
[x,y] in E )
proof end;
uniqueness
for b1, b2 being Coherence_Space st ( for a being set holds
( a in b1 iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) & ( for a being set holds
( a in b2 iff for x, y being set st x in a & y in a holds
[x,y] in E ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines CohSp COH_SP:def 3 :
for X being set
for E being Tolerance of X
for b3 being Coherence_Space holds
( b3 = CohSp E iff for a being set holds
( a in b3 iff for x, y being set st x in a & y in a holds
[x,y] in E ) );

theorem :: COH_SP:12
for X being set
for E being Tolerance of X holds Web (CohSp E) = E
proof end;

theorem :: COH_SP:13
for C being Coherence_Space holds CohSp (Web C) = C
proof end;

theorem Th14: :: COH_SP:14
for X, a being set
for E being Tolerance of X holds
( a in CohSp E iff a is TolSet of E )
proof end;

theorem :: COH_SP:15
for X being set
for E being Tolerance of X holds CohSp E = TolSets E
proof end;

begin

definition
let X be set ;
func CSp X -> set equals :: COH_SP:def 4
{ x where x is Subset-Family of X : x is Coherence_Space } ;
coherence
{ x where x is Subset-Family of X : x is Coherence_Space } is set
;
end;

:: deftheorem defines CSp COH_SP:def 4 :
for X being set holds CSp X = { x where x is Subset-Family of X : x is Coherence_Space } ;

registration
let X be set ;
cluster CSp X -> non empty ;
coherence
not CSp X is empty
proof end;
end;

registration
let X be set ;
cluster -> non empty subset-closed binary_complete for Element of CSp X;
coherence
for b1 being Element of CSp X holds
( b1 is subset-closed & b1 is binary_complete & not b1 is empty )
proof end;
end;

theorem Th16: :: COH_SP:16
for X, x, y being set
for C being Element of CSp X st {x,y} in C holds
( x in union C & y in union C )
proof end;

definition
let X be set ;
func FuncsC X -> set equals :: COH_SP:def 5
union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ;
coherence
union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } is set
;
end;

:: deftheorem defines FuncsC COH_SP:def 5 :
for X being set holds FuncsC X = union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ;

registration
let X be set ;
cluster FuncsC X -> functional non empty ;
coherence
( not FuncsC X is empty & FuncsC X is functional )
proof end;
end;

theorem Th17: :: COH_SP:17
for x, X being set holds
( x in FuncsC X iff ex C1, C2 being Element of CSp X st
( ( union C2 = {} implies union C1 = {} ) & x is Function of (union C1),(union C2) ) )
proof end;

definition
let X be set ;
func MapsC X -> set equals :: COH_SP:def 6
{ [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) )
}
;
coherence
{ [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) )
}
is set
;
end;

:: deftheorem defines MapsC COH_SP:def 6 :
for X being set holds MapsC X = { [[C,CC],f] where C, CC is Element of CSp X, f is Element of FuncsC X : ( ( union CC = {} implies union C = {} ) & f is Function of (union C),(union CC) & ( for x, y being set st {x,y} in C holds
{(f . x),(f . y)} in CC ) )
}
;

registration
let X be set ;
cluster MapsC X -> non empty ;
coherence
not MapsC X is empty
proof end;
end;

theorem Th18: :: COH_SP:18
for X being set
for l being Element of MapsC X ex g being Element of FuncsC X ex C1, C2 being Element of CSp X st
( l = [[C1,C2],g] & ( union C2 = {} implies union C1 = {} ) & g is Function of (union C1),(union C2) & ( for x, y being set st {x,y} in C1 holds
{(g . x),(g . y)} in C2 ) )
proof end;

theorem Th19: :: COH_SP:19
for X being set
for C1, C2 being Element of CSp X
for f being Function of (union C1),(union C2) st ( union C2 = {} implies union C1 = {} ) & ( for x, y being set st {x,y} in C1 holds
{(f . x),(f . y)} in C2 ) holds
[[C1,C2],f] in MapsC X
proof end;

registration
let X be set ;
let l be Element of MapsC X;
cluster l `2 -> Relation-like Function-like ;
coherence
( l `2 is Function-like & l `2 is Relation-like )
proof end;
end;

definition
let X be set ;
let l be Element of MapsC X;
func dom l -> Element of CSp X equals :: COH_SP:def 7
(l `1) `1 ;
coherence
(l `1) `1 is Element of CSp X
proof end;
func cod l -> Element of CSp X equals :: COH_SP:def 8
(l `1) `2 ;
coherence
(l `1) `2 is Element of CSp X
proof end;
end;

:: deftheorem defines dom COH_SP:def 7 :
for X being set
for l being Element of MapsC X holds dom l = (l `1) `1 ;

:: deftheorem defines cod COH_SP:def 8 :
for X being set
for l being Element of MapsC X holds cod l = (l `1) `2 ;

theorem Th20: :: COH_SP:20
for X being set
for l being Element of MapsC X holds l = [[(dom l),(cod l)],(l `2)]
proof end;

Lm1: for X being set
for l, l1 being Element of MapsC X st l `2 = l1 `2 & dom l = dom l1 & cod l = cod l1 holds
l = l1

proof end;

definition
let X be set ;
let C be Element of CSp X;
func id$ C -> Element of MapsC X equals :: COH_SP:def 9
[[C,C],(id (union C))];
coherence
[[C,C],(id (union C))] is Element of MapsC X
proof end;
end;

:: deftheorem defines id$ COH_SP:def 9 :
for X being set
for C being Element of CSp X holds id$ C = [[C,C],(id (union C))];

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

proof end;

theorem Th21: :: COH_SP:21
for X being set
for l being Element of MapsC X holds
( ( union (cod l) <> {} or union (dom l) = {} ) & l `2 is Function of (union (dom l)),(union (cod l)) & ( for x, y being set st {x,y} in dom l holds
{((l `2) . x),((l `2) . y)} in cod l ) )
proof end;

definition
let X be set ;
let l1, l2 be Element of MapsC X;
assume A1: cod l1 = dom l2 ;
func l2 * l1 -> Element of MapsC X equals :Def10: :: COH_SP:def 10
[[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];
coherence
[[(dom l1),(cod l2)],((l2 `2) * (l1 `2))] is Element of MapsC X
proof end;
end;

:: deftheorem Def10 defines * COH_SP:def 10 :
for X being set
for l1, l2 being Element of MapsC X st cod l1 = dom l2 holds
l2 * l1 = [[(dom l1),(cod l2)],((l2 `2) * (l1 `2))];

theorem Th22: :: COH_SP:22
for X being set
for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
( (l2 * l1) `2 = (l2 `2) * (l1 `2) & dom (l2 * l1) = dom l1 & cod (l2 * l1) = cod l2 )
proof end;

theorem Th23: :: COH_SP:23
for X being set
for l2, l1, l3 being Element of MapsC X st dom l2 = cod l1 & dom l3 = cod l2 holds
l3 * (l2 * l1) = (l3 * l2) * l1
proof end;

theorem Th24: :: COH_SP:24
for X being set
for C being Element of CSp X holds
( (id$ C) `2 = id (union C) & dom (id$ C) = C & cod (id$ C) = C )
proof end;

theorem Th25: :: COH_SP:25
for X being set
for l being Element of MapsC X holds
( l * (id$ (dom l)) = l & (id$ (cod l)) * l = l )
proof end;

definition
let X be set ;
func CDom X -> Function of (MapsC X),(CSp X) means :Def11: :: COH_SP:def 11
for l being Element of MapsC X holds it . l = dom l;
existence
ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = dom l
proof end;
uniqueness
for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = dom l ) & ( for l being Element of MapsC X holds b2 . l = dom l ) holds
b1 = b2
proof end;
func CCod X -> Function of (MapsC X),(CSp X) means :Def12: :: COH_SP:def 12
for l being Element of MapsC X holds it . l = cod l;
existence
ex b1 being Function of (MapsC X),(CSp X) st
for l being Element of MapsC X holds b1 . l = cod l
proof end;
uniqueness
for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = cod l ) & ( for l being Element of MapsC X holds b2 . l = cod l ) holds
b1 = b2
proof end;
func CComp X -> PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) means :Def13: :: COH_SP:def 13
( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom it iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
it . [l2,l1] = l2 * l1 ) );
existence
ex b1 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st
( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) st ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b1 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) & ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines CDom COH_SP:def 11 :
for X being set
for b2 being Function of (MapsC X),(CSp X) holds
( b2 = CDom X iff for l being Element of MapsC X holds b2 . l = dom l );

:: deftheorem Def12 defines CCod COH_SP:def 12 :
for X being set
for b2 being Function of (MapsC X),(CSp X) holds
( b2 = CCod X iff for l being Element of MapsC X holds b2 . l = cod l );

:: deftheorem Def13 defines CComp COH_SP:def 13 :
for X being set
for b2 being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) holds
( b2 = CComp X iff ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) ) );

theorem :: COH_SP:26
canceled;

definition
canceled;
let X be set ;
func CohCat X -> non empty non void strict CatStr equals :: COH_SP:def 15
CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);
coherence
CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #) is non empty non void strict CatStr
;
end;

:: deftheorem COH_SP:def 14 :
canceled;

:: deftheorem defines CohCat COH_SP:def 15 :
for X being set holds CohCat X = CatStr(# (CSp X),(MapsC X),(CDom X),(CCod X),(CComp X) #);

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

LmX: for X being set
for a being Element of (CohCat X)
for aa being Element of CSp X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
for b being Element of (CohCat X) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

proof end;

registration
let X be set ;
cluster CohCat X -> non empty non void strict with_identities ;
coherence
CohCat X is with_identities
proof end;
end;

begin

definition
let X be set ;
func Toler X -> set means :Def16: :: COH_SP:def 16
for x being set holds
( x in it iff x is Tolerance of X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Tolerance of X )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Tolerance of X ) ) & ( for x being set holds
( x in b2 iff x is Tolerance of X ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def16 defines Toler COH_SP:def 16 :
for X, b2 being set holds
( b2 = Toler X iff for x being set holds
( x in b2 iff x is Tolerance of X ) );

registration
let X be set ;
cluster Toler X -> non empty ;
coherence
not Toler X is empty
proof end;
end;

definition
let X be set ;
func Toler_on_subsets X -> set equals :: COH_SP:def 17
union { (Toler Y) where Y is Subset of X : verum } ;
coherence
union { (Toler Y) where Y is Subset of X : verum } is set
;
end;

:: deftheorem defines Toler_on_subsets COH_SP:def 17 :
for X being set holds Toler_on_subsets X = union { (Toler Y) where Y is Subset of X : verum } ;

registration
let X be set ;
cluster Toler_on_subsets X -> non empty ;
coherence
not Toler_on_subsets X is empty
proof end;
end;

theorem :: COH_SP:27
for x, X being set holds
( x in Toler_on_subsets X iff ex A being set st
( A c= X & x is Tolerance of A ) )
proof end;

theorem :: COH_SP:28
for a being set holds Total a in Toler a by Def16;

theorem Th29: :: COH_SP:29
for X being set holds {} in Toler_on_subsets X
proof end;

theorem Th30: :: COH_SP:30
for a, X being set st a c= X holds
Total a in Toler_on_subsets X
proof end;

theorem Th31: :: COH_SP:31
for a, X being set st a c= X holds
id a in Toler_on_subsets X
proof end;

theorem :: COH_SP:32
for X being set holds Total X in Toler_on_subsets X by Th30;

theorem :: COH_SP:33
for X being set holds id X in Toler_on_subsets X by Th31;

definition
let X be set ;
func TOL X -> set equals :: COH_SP:def 18
{ [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ;
coherence
{ [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } is set
;
end;

:: deftheorem defines TOL COH_SP:def 18 :
for X being set holds TOL X = { [t,Y] where t is Element of Toler_on_subsets X, Y is Subset of X : t is Tolerance of Y } ;

registration
let X be set ;
cluster TOL X -> non empty ;
coherence
not TOL X is empty
proof end;
end;

theorem :: COH_SP:34
for X being set holds [{},{}] in TOL X
proof end;

theorem Th35: :: COH_SP:35
for a, X being set st a c= X holds
[(id a),a] in TOL X
proof end;

theorem Th36: :: COH_SP:36
for a, X being set st a c= X holds
[(Total a),a] in TOL X
proof end;

theorem :: COH_SP:37
for X being set holds [(id X),X] in TOL X by Th35;

theorem :: COH_SP:38
for X being set holds [(Total X),X] in TOL X by Th36;

definition
let X be set ;
let T be Element of TOL X;
:: original: `2
redefine func T `2 -> Subset of X;
coherence
T `2 is Subset of X
proof end;
:: original: `1
redefine func T `1 -> Tolerance of (T `2);
coherence
T `1 is Tolerance of (T `2)
proof end;
end;

definition
let X be set ;
func FuncsT X -> set equals :: COH_SP:def 19
union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;
coherence
union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } is set
;
end;

:: deftheorem defines FuncsT COH_SP:def 19 :
for X being set holds FuncsT X = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;

registration
let X be set ;
cluster FuncsT X -> functional non empty ;
coherence
( not FuncsT X is empty & FuncsT X is functional )
proof end;
end;

theorem Th39: :: COH_SP:39
for x, X being set holds
( x in FuncsT X iff ex T1, T2 being Element of TOL X st
( ( T2 `2 = {} implies T1 `2 = {} ) & x is Function of (T1 `2),(T2 `2) ) )
proof end;

definition
let X be set ;
func MapsT X -> set equals :: COH_SP:def 20
{ [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )
}
;
coherence
{ [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )
}
is set
;
end;

:: deftheorem defines MapsT COH_SP:def 20 :
for X being set holds MapsT X = { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) )
}
;

registration
let X be set ;
cluster MapsT X -> non empty ;
coherence
not MapsT X is empty
proof end;
end;

theorem Th40: :: COH_SP:40
for X being set
for m being Element of MapsT X ex f being Element of FuncsT X ex T1, T2 being Element of TOL X st
( m = [[T1,T2],f] & ( T2 `2 = {} implies T1 `2 = {} ) & f is Function of (T1 `2),(T2 `2) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) )
proof end;

theorem Th41: :: COH_SP:41
for X being set
for T1, T2 being Element of TOL X
for f being Function of (T1 `2),(T2 `2) st ( T2 `2 = {} implies T1 `2 = {} ) & ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) holds
[[T1,T2],f] in MapsT X
proof end;

registration
let X be set ;
let m be Element of MapsT X;
cluster m `2 -> Relation-like Function-like ;
coherence
( m `2 is Function-like & m `2 is Relation-like )
proof end;
end;

definition
let X be set ;
let m be Element of MapsT X;
func dom m -> Element of TOL X equals :: COH_SP:def 21
(m `1) `1 ;
coherence
(m `1) `1 is Element of TOL X
proof end;
func cod m -> Element of TOL X equals :: COH_SP:def 22
(m `1) `2 ;
coherence
(m `1) `2 is Element of TOL X
proof end;
end;

:: deftheorem defines dom COH_SP:def 21 :
for X being set
for m being Element of MapsT X holds dom m = (m `1) `1 ;

:: deftheorem defines cod COH_SP:def 22 :
for X being set
for m being Element of MapsT X holds cod m = (m `1) `2 ;

theorem Th42: :: COH_SP:42
for X being set
for m being Element of MapsT X holds m = [[(dom m),(cod m)],(m `2)]
proof end;

Lm3: for X being set
for m, m1 being Element of MapsT X st m `2 = m1 `2 & dom m = dom m1 & cod m = cod m1 holds
m = m1

proof end;

definition
let X be set ;
let T be Element of TOL X;
func id$ T -> Element of MapsT X equals :: COH_SP:def 23
[[T,T],(id (T `2))];
coherence
[[T,T],(id (T `2))] is Element of MapsT X
proof end;
end;

:: deftheorem defines id$ COH_SP:def 23 :
for X being set
for T being Element of TOL X holds id$ T = [[T,T],(id (T `2))];

theorem Th43: :: COH_SP:43
for X being set
for m being Element of MapsT X holds
( ( (cod m) `2 <> {} or (dom m) `2 = {} ) & m `2 is Function of ((dom m) `2),((cod m) `2) & ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )
proof end;

definition
let X be set ;
let m1, m2 be Element of MapsT X;
assume A1: cod m1 = dom m2 ;
func m2 * m1 -> Element of MapsT X equals :Def24: :: COH_SP:def 24
[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];
coherence
[[(dom m1),(cod m2)],((m2 `2) * (m1 `2))] is Element of MapsT X
proof end;
end;

:: deftheorem Def24 defines * COH_SP:def 24 :
for X being set
for m1, m2 being Element of MapsT X st cod m1 = dom m2 holds
m2 * m1 = [[(dom m1),(cod m2)],((m2 `2) * (m1 `2))];

theorem Th44: :: COH_SP:44
for X being set
for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
( (m2 * m1) `2 = (m2 `2) * (m1 `2) & dom (m2 * m1) = dom m1 & cod (m2 * m1) = cod m2 )
proof end;

theorem Th45: :: COH_SP:45
for X being set
for m2, m1, m3 being Element of MapsT X st dom m2 = cod m1 & dom m3 = cod m2 holds
m3 * (m2 * m1) = (m3 * m2) * m1
proof end;

theorem Th46: :: COH_SP:46
for X being set
for T being Element of TOL X holds
( (id$ T) `2 = id (T `2) & dom (id$ T) = T & cod (id$ T) = T )
proof end;

theorem Th47: :: COH_SP:47
for X being set
for m being Element of MapsT X holds
( m * (id$ (dom m)) = m & (id$ (cod m)) * m = m )
proof end;

definition
let X be set ;
func fDom X -> Function of (MapsT X),(TOL X) means :Def25: :: COH_SP:def 25
for m being Element of MapsT X holds it . m = dom m;
existence
ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = dom m
proof end;
uniqueness
for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = dom m ) & ( for m being Element of MapsT X holds b2 . m = dom m ) holds
b1 = b2
proof end;
func fCod X -> Function of (MapsT X),(TOL X) means :Def26: :: COH_SP:def 26
for m being Element of MapsT X holds it . m = cod m;
existence
ex b1 being Function of (MapsT X),(TOL X) st
for m being Element of MapsT X holds b1 . m = cod m
proof end;
uniqueness
for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = cod m ) & ( for m being Element of MapsT X holds b2 . m = cod m ) holds
b1 = b2
proof end;
func fComp X -> PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) means :Def27: :: COH_SP:def 27
( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom it iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
it . [m2,m1] = m2 * m1 ) );
existence
ex b1 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st
( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) )
proof end;
uniqueness
for b1, b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) st ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b1 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) & ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines fDom COH_SP:def 25 :
for X being set
for b2 being Function of (MapsT X),(TOL X) holds
( b2 = fDom X iff for m being Element of MapsT X holds b2 . m = dom m );

:: deftheorem Def26 defines fCod COH_SP:def 26 :
for X being set
for b2 being Function of (MapsT X),(TOL X) holds
( b2 = fCod X iff for m being Element of MapsT X holds b2 . m = cod m );

:: deftheorem Def27 defines fComp COH_SP:def 27 :
for X being set
for b2 being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) holds
( b2 = fComp X iff ( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) ) );

definition
canceled;
let X be set ;
func TolCat X -> non empty non void strict CatStr equals :: COH_SP:def 29
CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);
coherence
CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #) is non empty non void strict CatStr
;
end;

:: deftheorem COH_SP:def 28 :
canceled;

:: deftheorem defines TolCat COH_SP:def 29 :
for X being set holds TolCat X = CatStr(# (TOL X),(MapsT X),(fDom X),(fCod X),(fComp X) #);

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

LmX: for X being set
for a being Element of (TolCat X)
for aa being Element of TOL X st a = aa holds
for i being Morphism of a,a st i = id$ aa holds
for b being Element of (TolCat X) holds
( ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) i = g ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )

proof end;

registration
let X be set ;
cluster TolCat X -> non empty non void strict with_identities ;
coherence
TolCat X is with_identities
proof end;
end;