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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

registration
let X be set ;
let l be Element of MapsC X;
clusterl `2  ->  Relation-like Function-like ;
coherence
 ( l `2 is Function-like & l `2 is Relation-like )
proofend;
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
proofend;
func cod l ->  Element of CSp X equals :: COH_SP:def 8
(l `1) `2 ;
coherence
 (l `1) `2 is Element of CSp X
proofend;
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)]
proofend;

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

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

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

definition
let X be set ;
let l1, l2 be Element of MapsC X;
assume A1: cod l1 = dom l2 ;
funcl2 * 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
proofend;
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) &amp; dom (l2 * l1) = dom l1 &amp; cod (l2 * l1) = cod l2 )
proofend;

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

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

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

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
proofend;
uniqueness
 for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = dom l ) &amp; ( for l being Element of MapsC X holds b2 . l = dom l ) holds
b1 = b2
proofend;
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
proofend;
uniqueness
 for b1, b2 being Function of (MapsC X),(CSp X) st ( for l being Element of MapsC X holds b1 . l = cod l ) &amp; ( for l being Element of MapsC X holds b2 . l = cod l ) holds
b1 = b2
proofend;
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 ) ) &amp; ( 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 ) ) &amp; ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) )
proofend;
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 ) ) &amp; ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b1 . [l2,l1] = l2 * l1 ) &amp; ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b2 iff dom l2 = cod l1 ) ) &amp; ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b2 . [l2,l1] = l2 * l1 ) holds
b1 = b2
proofend;
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 ) ) &amp; ( 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 &amp; CohCat X is transitive &amp; CohCat X is associative &amp; CohCat X is reflexive )
proofend;
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 ) &amp; ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proofend;

registration
let X be set ;
cluster CohCat X ->  non empty non void strict with_identities ;
coherence
 CohCat X is with_identities
proofend;
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 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Tolerance of X ) ) &amp; ( for x being set holds
( x in b2 iff x is Tolerance of X ) ) holds
b1 = b2
proofend;
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
proofend;
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
proofend;
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 &amp; x is Tolerance of A ) )
proofend;

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

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

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

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

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

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

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

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 funcT `2  ->  Subset of X;
coherence
 T `2 is Subset of X
proofend;
:: original:`1
redefine funcT `1  ->  Tolerance of (T `2);
coherence
 T `1 is Tolerance of (T `2)
proofend;
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 &amp; FuncsT X is functional )
proofend;
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 = {} ) &amp; x is Function of (T1 `2),(T2 `2) ) )
proofend;

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 = {} ) &amp; f is Function of (T `2),(TT `2) &amp; ( 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 = {} ) &amp; f is Function of (T `2),(TT `2) &amp; ( 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 = {} ) &amp; f is Function of (T `2),(TT `2) &amp; ( 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
proofend;
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] &amp; ( T2 `2 = {} implies T1 `2 = {} ) &amp; f is Function of (T1 `2),(T2 `2) &amp; ( for x, y being set st [x,y] in T1 `1 holds
[(f . x),(f . y)] in T2 `1 ) )
proofend;

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 = {} ) &amp; ( 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
proofend;

registration
let X be set ;
let m be Element of MapsT X;
clusterm `2  ->  Relation-like Function-like ;
coherence
 ( m `2 is Function-like &amp; m `2 is Relation-like )
proofend;
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
proofend;
func cod m ->  Element of TOL X equals :: COH_SP:def 22
(m `1) `2 ;
coherence
 (m `1) `2 is Element of TOL X
proofend;
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)]
proofend;

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

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
proofend;
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 = {} ) &amp; m `2 is Function of ((dom m) `2),((cod m) `2) &amp; ( for x, y being set st [x,y] in (dom m) `1 holds
[((m `2) . x),((m `2) . y)] in (cod m) `1 ) )
proofend;

definition
let X be set ;
let m1, m2 be Element of MapsT X;
assume A1: cod m1 = dom m2 ;
funcm2 * 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
proofend;
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) &amp; dom (m2 * m1) = dom m1 &amp; cod (m2 * m1) = cod m2 )
proofend;

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

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

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

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
proofend;
uniqueness
 for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = dom m ) &amp; ( for m being Element of MapsT X holds b2 . m = dom m ) holds
b1 = b2
proofend;
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
proofend;
uniqueness
 for b1, b2 being Function of (MapsT X),(TOL X) st ( for m being Element of MapsT X holds b1 . m = cod m ) &amp; ( for m being Element of MapsT X holds b2 . m = cod m ) holds
b1 = b2
proofend;
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 ) ) &amp; ( 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 ) ) &amp; ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) )
proofend;
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 ) ) &amp; ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b1 . [m2,m1] = m2 * m1 ) &amp; ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b2 iff dom m2 = cod m1 ) ) &amp; ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b2 . [m2,m1] = m2 * m1 ) holds
b1 = b2
proofend;
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 ) ) &amp; ( 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 &amp; TolCat X is transitive &amp; TolCat X is associative &amp; TolCat X is reflexive )
proofend;
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 ) &amp; ( Hom (b,a) <> {} implies for f being Morphism of b,a holds i (*) f = f ) )
proofend;

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