:: Categories without Uniqueness of { \bf cod } and { \bf dom }
::  by Andrzej Trybulec
::
:: Received February 28, 1995
:: Copyright (c) 1995-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 FUNCT_1, SUBSET_1, RELAT_1, FUNCT_2, XBOOLE_0, TARSKI, PBOOLE,
      ZFMISC_1, MCART_1, FUNCOP_1, STRUCT_0, CAT_1, RELAT_2, BINOP_1, CARD_1,
      ALTCAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, DOMAIN_1,
      RELAT_1, CARD_1, ORDINAL1, NUMBERS, RELSET_1, STRUCT_0, FUNCT_1, FUNCT_2,
      BINOP_1, MULTOP_1, FUNCOP_1, PBOOLE;
 constructors PARTFUN1, BINOP_1, MULTOP_1, PBOOLE, REALSET2, RELSET_1,
      XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1,
      STRUCT_0, RELSET_1, ZFMISC_1, CARD_1, XTUPLE_0;
 requirements BOOLE, SUBSET;


begin :: Preliminaries

reserve i,j,k,x for object;

::$CT 4

theorem :: ALTCAT_1:5
  for A,B being set, F being ManySortedSet of [:B,A:], C being Subset of
A, D being Subset of B, x,y being set st x in C & y in D holds F.(y,x) = (F|([:
  D,C:] qua set)).(y,x);

scheme :: ALTCAT_1:sch 1
  MSSLambda2{ A,B() -> set, F(object,object) -> object }:
 ex M being ManySortedSet of [:A(),B():]
 st for i,j being set st i in A() & j in B() holds M.(i,j) = F(i,j);

scheme :: ALTCAT_1:sch 2
  MSSLambda2D{ A,B() -> non empty set, F(object,object) -> object }:
 ex M being
ManySortedSet of [:A(),B():] st for i being Element of A(), j being Element of
  B() holds M.(i,j) = F(i,j);

scheme :: ALTCAT_1:sch 3
  MSSLambda3{ A,B,C() -> set, F(object,object,object) -> object }:
 ex M being ManySortedSet of [:A(),B(),C():] st
 for i,j,k being set st i in A() & j in B() & k in C()
  holds M.(i,j,k) = F(i,j,k);

scheme :: ALTCAT_1:sch 4
  MSSLambda3D{ A,B,C() -> non empty set, F(object,object,object) -> object }:
ex M being
ManySortedSet of [:A(),B(),C():] st for i being Element of A(), j being Element
  of B(), k being Element of C() holds M.(i,j,k) = F(i,j,k);

theorem :: ALTCAT_1:6
  for A,B being set, N,M being ManySortedSet of [:A,B:] st for i,j
  st i in A & j in B holds N.(i,j) = M.(i,j) holds M = N;

theorem :: ALTCAT_1:7
  for A,B being non empty set, N,M being ManySortedSet of [:A,B:]
st for i being Element of A, j being Element of B holds N.(i,j) = M.(i,j) holds
  M = N;

theorem :: ALTCAT_1:8
  for A being set, N,M being ManySortedSet of [:A,A,A:] st for i,j
  ,k st i in A & j in A & k in A holds N.(i,j,k) = M.(i,j,k) holds M = N;

begin :: Alternative Graphs

definition
  struct(1-sorted) AltGraph (# carrier -> set, Arrows -> ManySortedSet of [:
    the carrier, the carrier:] #);
end;

definition
  let G be AltGraph;
  mode Object of G is Element of G;
end;

definition
  let G be AltGraph;
  let o1,o2 be Object of G;

  func <^o1,o2^> -> set equals
:: ALTCAT_1:def 1
  (the Arrows of G).(o1,o2);
end;

definition
  let G be AltGraph;
  let o1,o2 be Object of G;
  mode Morphism of o1,o2 is Element of <^o1,o2^>;
end;

definition
  let G be AltGraph;

  attr G is transitive means
:: ALTCAT_1:def 2

  for o1,o2,o3 being Object of G st <^o1,o2
  ^> <> {} & <^o2,o3^> <> {} holds <^o1,o3^> <> {};
end;

begin :: Binary Compositions

definition
  let I be set;
  let G be ManySortedSet of [:I,I:];
  func {|G|} -> ManySortedSet of [:I,I,I:] means
:: ALTCAT_1:def 3

  for i,j,k being object st i in I & j in I & k in I
   holds it.(i,j,k) = G.(i,k);
  let H be ManySortedSet of [:I,I:];
  func {|G,H|} -> ManySortedSet of [:I,I,I:] means
:: ALTCAT_1:def 4

  for i,j,k being object st i in I & j in I & k in I
   holds it.(i,j,k) = [:H.(j,k),G.(i,j):];
end;

definition
  let I be set;
  let G be ManySortedSet of [:I,I:];
  mode BinComp of G is ManySortedFunction of {|G,G|},{|G|};
end;

definition
  let I be non empty set;
  let G be ManySortedSet of [:I,I:];
  let o be BinComp of G;
  let i,j,k be Element of I;
  redefine func o.(i,j,k) -> Function of [:G.(j,k),G.(i,j):], G.(i,k);
end;

definition
  let I be non empty set;
  let G be ManySortedSet of [:I,I:];
  let IT be BinComp of G;
  attr IT is associative means
:: ALTCAT_1:def 5

  for i,j,k,l being Element of I for f,g,h
being set st f in G.(i,j) & g in G.(j,k) & h in G.(k,l) holds IT.(i,k,l).(h,IT.
  (i,j,k).(g,f)) = IT.(i,j,l).(IT.(j,k,l).(h,g),f);
  attr IT is with_right_units means
:: ALTCAT_1:def 6

  for i being Element of I ex e being
set st e in G.(i,i) & for j being Element of I, f be set st f in G.(i,j) holds
  IT.(i,i,j).(f,e) = f;
  attr IT is with_left_units means
:: ALTCAT_1:def 7

  for j being Element of I ex e being
set st e in G.(j,j) & for i being Element of I, f be set st f in G.(i,j) holds
  IT.(i,j,j).(e,f) = f;
end;

begin :: Alternative categories

definition
  struct(AltGraph) AltCatStr (# carrier -> set, Arrows -> ManySortedSet of [:
    the carrier, the carrier:], Comp -> BinComp of the Arrows #);
end;

registration
  cluster strict non empty for AltCatStr;
end;

definition
  let C be non empty AltCatStr;
  let o1,o2,o3 be Object of C such that
 <^o1,o2^> <> {} & <^o2,o3^> <> {};
  let f be Morphism of o1,o2, g be Morphism of o2,o3;
  func g*f -> Morphism of o1,o3 equals
:: ALTCAT_1:def 8

  (the Comp of C).(o1,o2,o3).(g,f
  );
end;

definition
  let IT be Function;
  attr IT is compositional means
:: ALTCAT_1:def 9

  x in dom IT implies ex f,g being Function st x = [g,f] & IT.x = g*f;
end;

registration
  let A,B be functional set;
  cluster compositional for ManySortedFunction of [:A,B:];
end;

::$CT 2

theorem :: ALTCAT_1:11
  for A,B being functional set for F being compositional
ManySortedSet of [:A,B:], g,f being Function st g in A & f in B holds F.(g,f) =
  g*f;

definition
  let A,B be functional set;
  func FuncComp(A,B) -> compositional ManySortedFunction of [:B,A:] means
:: ALTCAT_1:def 10
 not contradiction;
end;

theorem :: ALTCAT_1:12
  for A,B,C being set holds rng FuncComp(Funcs(A,B),Funcs(B,C)) c= Funcs(A,C);

theorem :: ALTCAT_1:13
  for o be set holds FuncComp({id o},{id o}) = (id o,id o) :-> id o;

theorem :: ALTCAT_1:14
  for A,B being functional set, A1 being Subset of A, B1 being
  Subset of B holds FuncComp(A1,B1) = FuncComp(A,B)|([:B1,A1:] qua set);

:: Kategorie przeksztalcen, Semadeni Wiweger, 1.2.2, str.15

definition
  let C be non empty AltCatStr;
  attr C is quasi-functional means
:: ALTCAT_1:def 11

  for a1,a2 being Object of C holds <^a1,a2^> c= Funcs(a1,a2);
  attr C is semi-functional means
:: ALTCAT_1:def 12

  for a1,a2,a3 being Object of C st <^
a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} for f being Morphism of a1,a2
, g being Morphism of a2,a3, f9,g9 being Function st f = f9 & g = g9 holds g*f
  =g9*f9;
  attr C is pseudo-functional means
:: ALTCAT_1:def 13

  for o1,o2,o3 being Object of C
holds (the Comp of C).(o1,o2,o3) = FuncComp(Funcs(o1,o2),Funcs(o2,o3))|([:<^o2,
  o3^>,<^o1,o2^>:] qua set);
end;

registration
  let X be non empty set, A be ManySortedSet of [:X,X:], C be BinComp of A;
  cluster AltCatStr(#X,A,C#) -> non empty;
end;

registration
  cluster strict pseudo-functional for non empty AltCatStr;
end;

theorem :: ALTCAT_1:15
  for C being non empty AltCatStr, a1,a2,a3 being Object of C holds (the
  Comp of C).(a1,a2,a3) is Function of [:<^a2,a3^>,<^a1,a2^>:],<^a1,a3^>;

theorem :: ALTCAT_1:16
  for C being pseudo-functional non empty AltCatStr for a1,a2,a3
being Object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} for f
being Morphism of a1,a2, g being Morphism of a2,a3, f9,g9 being Function st f =
  f9 & g = g9 holds g*f =g9*f9;

:: Kategorie EnsCat(A), Semadeni Wiweger 1.2.3, str. 15
:: ale bez parametryzacji

definition
  let A be non empty set;
  func EnsCat A -> strict pseudo-functional non empty AltCatStr means
:: ALTCAT_1:def 14


  the carrier of it = A & for a1,a2 being Object of it holds <^a1,a2^> = Funcs(
  a1,a2);
end;

definition
  let C be non empty AltCatStr;
  attr C is associative means
:: ALTCAT_1:def 15

  the Comp of C is associative;
  attr C is with_units means
:: ALTCAT_1:def 16

  the Comp of C is with_left_units with_right_units;
end;

registration
  cluster transitive associative with_units strict for non empty AltCatStr;
end;

theorem :: ALTCAT_1:17
  for C being transitive non empty AltCatStr, a1,a2,a3 being Object of C
holds dom((the Comp of C).(a1,a2,a3)) = [:<^a2,a3^>,<^a1,a2^>:] & rng((the Comp
  of C).(a1,a2,a3)) c= <^a1,a3^>;

theorem :: ALTCAT_1:18
  for C being with_units non empty AltCatStr for o being Object
  of C holds <^o,o^> <> {};

registration
  let A be non empty set;
  cluster EnsCat A -> transitive associative with_units;
end;

registration
  cluster quasi-functional semi-functional transitive -> pseudo-functional for

    non empty AltCatStr;
  cluster with_units pseudo-functional transitive -> quasi-functional
    semi-functional for non empty AltCatStr;
end;

:: Definicja kategorii, Semadeni Wiweger 1.3.1, str. 16-17

definition
  mode category is transitive associative with_units non empty AltCatStr;
end;

begin

definition
  let C be with_units non empty AltCatStr;
  let o be Object of C;
  func idm o -> Morphism of o,o means
:: ALTCAT_1:def 17

  for o9 being Object of C st <^o,
  o9^> <> {} for a being Morphism of o,o9 holds a*it = a;
end;

theorem :: ALTCAT_1:19
  for C being with_units non empty AltCatStr for o being Object
  of C holds idm o in <^o,o^>;

theorem :: ALTCAT_1:20
  for C being with_units non empty AltCatStr for o1,o2 being Object of
  C st <^o1,o2^> <> {} for a being Morphism of o1,o2 holds (idm o2)*a = a;

theorem :: ALTCAT_1:21
  for C being associative transitive non empty AltCatStr for o1,o2,o3,
o4 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} for
a being Morphism of o1,o2, b being Morphism of o2,o3, c being Morphism of o3,o4
  holds c*(b*a) = (c*b)*a;

begin

:: kategoria dyskretna, Semadeni Wiweger, 1.3.1, str.18

definition
  let C be AltCatStr;
  attr C is quasi-discrete means
:: ALTCAT_1:def 18

  for i,j being Object of C st <^i,j^> <> {} holds i = j;

:: to sa po prostu zbiory monoidow
  attr C is pseudo-discrete means
:: ALTCAT_1:def 19

  for i being Object of C holds <^i,i ^> is trivial;
end;

theorem :: ALTCAT_1:22
  for C being with_units non empty AltCatStr holds C is
  pseudo-discrete iff for o being Object of C holds <^o,o^> = { idm o };

registration
  cluster 1-element -> quasi-discrete for AltCatStr;
end;

theorem :: ALTCAT_1:23
  EnsCat {0} is pseudo-discrete 1-element;

registration
  cluster pseudo-discrete trivial strict for category;
end;

registration
  cluster quasi-discrete pseudo-discrete trivial strict for category;
end;

definition
  mode discrete_category is quasi-discrete pseudo-discrete category;
end;

definition
  let A be non empty set;
  func DiscrCat A -> quasi-discrete strict non empty AltCatStr means
:: ALTCAT_1:def 20

  the carrier of it = A & for i being Object of it holds <^i,i^> = { id i };
end;

registration
  cluster quasi-discrete -> transitive for AltCatStr;
end;

theorem :: ALTCAT_1:24
  for A being non empty set, o1,o2,o3 being Object of DiscrCat A
  st o1 <> o2 or o2 <> o3 holds (the Comp of DiscrCat A).(o1,o2,o3) = {};

theorem :: ALTCAT_1:25
  for A being non empty set, o being Object of DiscrCat A holds (
  the Comp of DiscrCat A).(o,o,o) = (id o,id o) :-> id o;

registration
  let A be non empty set;
  cluster DiscrCat A -> pseudo-functional pseudo-discrete with_units
    associative;
end;