:: Coherent Space
::  by Jaros{\l}aw Kotowicz and Konrad Raczkowski
::
:: Received December 29, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies TARSKI, XBOOLE_0, CLASSES1, ZFMISC_1, EQREL_1, TOLER_1, SETFAM_1,
      SUBSET_1, FUNCT_2, FUNCT_1, RELAT_1, MCART_1, GRAPH_1, ENS_1, PARTFUN1,
      CAT_1, COH_SP, STRUCT_0, MONOID_0, RELAT_2, BINOP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, SETFAM_1,
      RELAT_1, RELSET_1, MCART_1, FUNCT_1, PARTFUN1, CLASSES1, FUNCT_2,
      BINOP_1, EQREL_1, TOLER_1, STRUCT_0, GRAPH_1, CAT_1;
 constructors BINOP_1, EQREL_1, CLASSES1, TOLER_1, CAT_1, RELSET_1, XTUPLE_0,
      XFAMILY;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      EQREL_1, CAT_2, CAT_1, XTUPLE_0;
 requirements SUBSET, BOOLE;


begin

reserve x,y,z,a,b,c,X,A for set;

:: Coherent Space and Web of Coherent Space

definition
  let IT be set;

  attr IT is binary_complete means
:: COH_SP:def 1

  for A st A c= IT & (for a,b st a in
  A & b in A holds a \/ b in IT) holds union A in IT;
end;

registration
  cluster subset-closed binary_complete non empty for set;
end;

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

reserve C,D for Coherence_Space;

theorem :: COH_SP:1
  {} in C;

theorem :: COH_SP:2
  bool X is Coherence_Space;

theorem :: COH_SP:3
  {{}} is Coherence_Space;

theorem :: COH_SP:4
  x in union C implies {x} in C;

definition
  let C be Coherence_Space;
  func Web(C) -> Tolerance of union C means
:: COH_SP:def 2

  for x,y being object holds [x,y] in it
    iff ex X st X in C & x in X & y in X;
end;

reserve T for Tolerance of union C;

theorem :: COH_SP:5
  T = Web(C) iff for x,y being object holds [x,y] in T iff {x,y} in C;

theorem :: COH_SP:6
  a in C iff for x,y st x in a & y in a holds {x,y} in C;

theorem :: COH_SP:7
  a in C iff for x,y st x in a & y in a holds [x,y] in Web(C);

theorem :: COH_SP:8
  (for x,y st x in a & y in a holds {x,y} in C) implies a c= union C;

theorem :: COH_SP:9
  Web(C) = Web(D) implies C = D;

theorem :: COH_SP:10
  union C in C implies C = bool union C;

theorem :: COH_SP:11
  C = bool union C implies Web(C) = Total union C;

definition
  let X be set;
  let E be Tolerance of X;
  func CohSp(E) -> Coherence_Space means
:: COH_SP:def 3

  for a holds a in it iff for x, y st x in a & y in a holds [x,y] in E;
end;

reserve E for Tolerance of X;

theorem :: COH_SP:12
  Web(CohSp(E)) = E;

theorem :: COH_SP:13
  CohSp(Web(C)) = C;

theorem :: COH_SP:14
  a in CohSp(E) iff a is TolSet of E;

theorem :: COH_SP:15
  CohSp(E) = TolSets E;

begin :: Category of Coherence Spaces

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

registration
  let X;
  cluster CSp(X) -> non empty;
end;

registration
  let X be set;
  cluster -> subset-closed binary_complete non empty for Element of CSp(X);
end;

reserve C,C1,C2 for Element of CSp(X);

theorem :: COH_SP:16
  {x,y} in C implies x in union C & y in union C;

definition
  let X;

  func FuncsC(X) -> set equals
:: COH_SP:def 5
  union the set of all  Funcs(union x,union y) where x is
  Element of CSp(X), y is Element of CSp(X);
end;

registration
  let X;
  cluster FuncsC(X) -> non empty functional;
end;

reserve g for Element of FuncsC(X);

theorem :: COH_SP:17
  x in FuncsC(X) iff ex C1,C2 st (union C2 = {} implies union C1 =
  {}) & x is Function of union C1,union C2;

definition
  let X;
  func MapsC(X) -> set equals
:: COH_SP:def 6
  { [[C,CC],f] where C is Element of CSp(X), 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 st {x,y} in C holds {f.x,f.y}
  in CC};
end;

registration
  let X;
  cluster MapsC(X) -> non empty;
end;

reserve l,l1,l2,l3 for Element of MapsC(X);

theorem :: COH_SP:18
  ex g,C1,C2 st l = [[C1,C2],g] & (union C2 = {} implies union C1
= {}) & g is Function of union C1,union C2 & for x,y st {x,y} in C1 holds {g.x,
  g.y} in C2;

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

registration
  let X be set, l be Element of MapsC(X);
  cluster l`2 -> Function-like Relation-like for set;
end;

definition
  let X,l;
  func dom l -> Element of CSp(X) equals
:: COH_SP:def 7
  l`1`1;
  func cod l -> Element of CSp(X) equals
:: COH_SP:def 8
  l`1`2;
end;

theorem :: COH_SP:20
  l = [[dom l,cod l],l`2];

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

theorem :: COH_SP:21
  (union cod l <> {} or union dom l = {}) & l`2 is Function of
union dom l,union cod l &
for x,y st {x,y} in dom l holds {(l`2).x,(l`2).y} in cod
  l;

definition
  let X,l1,l2;
  assume
 cod l1 = dom l2;
  func l2*l1 -> Element of MapsC(X) equals
:: COH_SP:def 10

  [[dom l1,cod l2],l2`2*l1`2];
end;

theorem :: COH_SP:22
  dom l2 = cod l1 implies (l2*l1)`2 = l2`2*l1`2 & dom(l2*l1) = dom
  l1 & cod(l2*l1) = cod l2;

theorem :: COH_SP:23
  dom l2 = cod l1 & dom l3 = cod l2 implies l3*(l2*l1) = (l3*l2)* l1;

theorem :: COH_SP:24
  (id$ C)`2 = id union C & dom id$ C = C & cod id$ C = C;

theorem :: COH_SP:25
  l*(id$ dom l) = l & (id$ cod l)*l = l;

definition
  let X;
  func CDom X -> Function of MapsC(X),CSp(X) means
:: COH_SP:def 11

  for l holds it.l = dom l;
  func CCod X -> Function of MapsC(X),CSp(X) means
:: COH_SP:def 12

  for l holds it.l = cod l;
  func CComp X -> PartFunc of [:MapsC(X),MapsC(X):],MapsC(X) means
:: COH_SP:def 13

  (for l2,l1 holds [l2,l1] in dom it iff dom l2 = cod l1) &
   for l2,l1 st dom l2 = cod l1 holds it.[l2,l1] = l2*l1;
end;

::$CT

definition
::$CD
  let X;
  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 #);
end;

registration let X;
 cluster CohCat X -> Category-like transitive associative reflexive;
end;

registration let X;
 cluster CohCat X -> with_identities;
end;

begin :: Category of Tolerances

definition
  let X be set;
  func Toler(X) -> set means
:: COH_SP:def 16

  x in it iff x is Tolerance of X;
end;

registration
  let X be set;
  cluster Toler(X) -> non empty;
end;

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

registration
  let X be set;
  cluster Toler_on_subsets(X) -> non empty;
end;

theorem :: COH_SP:27
  x in Toler_on_subsets(X) iff ex A st A c= X & x is Tolerance of A;

theorem :: COH_SP:28
  Total a in Toler(a);

theorem :: COH_SP:29
  {} in Toler_on_subsets(X);

theorem :: COH_SP:30
  a c= X implies Total a in Toler_on_subsets(X);

theorem :: COH_SP:31
  a c= X implies id a in Toler_on_subsets(X);

theorem :: COH_SP:32
  Total X in Toler_on_subsets(X);

theorem :: COH_SP:33
  id X in Toler_on_subsets(X);

definition
  let X;
  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};
end;

registration
  let X;
  cluster TOL(X) -> non empty;
end;

reserve T,T1,T2 for Element of TOL(X);

theorem :: COH_SP:34
  [{},{}] in TOL(X);

theorem :: COH_SP:35
  a c= X implies [id a,a] in TOL(X);

theorem :: COH_SP:36
  a c= X implies [Total a,a] in TOL(X);

theorem :: COH_SP:37
  [id X,X] in TOL(X);

theorem :: COH_SP:38
  [Total X,X] in TOL(X);

definition
  let X,T;
  redefine func T`2 -> Subset of X;
  redefine func T`1 -> Tolerance of T`2;
end;

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

registration
  let X;
  cluster FuncsT(X) -> non empty functional;
end;

reserve f for Element of FuncsT(X);

theorem :: COH_SP:39
  x in FuncsT(X) iff ex T1,T2 st (T2`2 = {} implies T1`2 = {}) & x
  is Function of T1`2,T2`2;

definition
  let X;
  func MapsT(X) -> set equals
:: COH_SP:def 20
  { [[T,TT],f] where T is Element of TOL(X), 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 st [x,y] in T`1 holds [f.x,f.y] in TT`1};
end;

registration
  let X;
  cluster MapsT(X) -> non empty;
end;

reserve m,m1,m2,m3 for Element of MapsT(X);

theorem :: COH_SP:40
  ex f,T1,T2 st m = [[T1,T2],f] & (T2`2 = {} implies T1`2 = {}) &
  f is Function of T1`2,T2`2 & for x,y st [x,y] in T1`1 holds [f.x,f.y] in T2`1
;

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

registration
  let X be set,m be Element of MapsT(X);
  cluster m`2 -> Function-like Relation-like for set;
end;

definition
  let X,m;

  func dom m -> Element of TOL(X) equals
:: COH_SP:def 21
  m`1`1;
  func cod m -> Element of TOL(X) equals
:: COH_SP:def 22
  m`1`2;
end;

theorem :: COH_SP:42
  m = [[dom m,cod m],m`2];

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

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

definition
  let X,m1,m2;
  assume
 cod m1 = dom m2;
  func m2*m1 -> Element of MapsT(X) equals
:: COH_SP:def 24

  [[dom m1,cod m2],m2`2*m1`2];
end;

theorem :: COH_SP:44
  dom m2 = cod m1 implies (m2*m1)`2 = m2`2*m1`2 & dom(m2*m1) = dom
  m1 & cod(m2*m1) = cod m2;

theorem :: COH_SP:45
  dom m2 = cod m1 & dom m3 = cod m2 implies m3*(m2*m1) = (m3*m2)* m1;

theorem :: COH_SP:46
  (id$ T)`2 = id T`2 & dom id$ T = T & cod id$ T = T;

theorem :: COH_SP:47
  m*(id$ dom m) = m & (id$ cod m)*m = m;

definition
  let X;
  func fDom X -> Function of MapsT(X),TOL(X) means
:: COH_SP:def 25

  for m holds it.m = dom m;
  func fCod X -> Function of MapsT(X),TOL(X) means
:: COH_SP:def 26

  for m holds it.m = cod m;
  func fComp X -> PartFunc of [:MapsT(X),MapsT(X):],MapsT(X) means
:: COH_SP:def 27

  (
for m2,m1 holds [m2,m1] in dom it iff dom m2 = cod m1) & for m2,m1 st dom m2 =
  cod m1 holds it.[m2,m1] = m2*m1;
end;

definition
::$CD
  let X;
  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#);
end;

registration
  let X;
  cluster TolCat(X) -> Category-like transitive associative reflexive;
end;

registration
  let X;
  cluster TolCat(X) -> with_identities;
end;