:: Comma Category
::  by Grzegorz Bancerek and Agata Darmochwa\l
::
:: Received February 20, 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 CAT_1, STRUCT_0, FUNCT_1, XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI,
      MCART_1, RELAT_1, GRAPH_1, PARTFUN1, CAT_2, FUNCOP_1, FUNCT_3, COMMACAT,
      MONOID_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, BINOP_1, FUNCOP_1, STRUCT_0, GRAPH_1, CAT_1, CAT_2, MCART_1,
      DOMAIN_1;
 constructors DOMAIN_1, CAT_2, FUNCOP_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, CAT_1, CAT_2, STRUCT_0, XTUPLE_0;
 requirements SUBSET, BOOLE;


begin

reserve y for set;

reserve C,D,E for Category,
  c,c1,c2 for Object of C,
  d,d1 for Object of D,
  x for set,
  f,f1 for (Morphism of E),
  g,g1 for (Morphism of C),
  h,h1 for (Morphism of D) ,
  F for Functor of C,E,
  G for Functor of D,E;

definition
  let C,D,E;
  let F be Functor of C,E, G be Functor of D,E;
  given c1,d1,f1 such that
 f1 in Hom(F.c1,G.d1);
  func commaObjs(F,G) -> non empty Subset of [:[:the carrier of C, the carrier
  of D:], the carrier' of E:] equals
:: COMMACAT:def 1

  {[[c,d],f] : f in Hom(F.c,G.d)};
end;

reserve o,o1,o2 for Element of commaObjs(F,G);

theorem :: COMMACAT:1
  (ex c,d,f st f in Hom(F.c,G.d)) implies o = [[o`11,o`12],o`2] & o
  `2 in Hom(F.o`11,G.o`12) & dom o`2 = F.o`11 & cod o`2 = G.o`12;

definition
  let C,D,E,F,G;
  given c1,d1,f1 such that
 f1 in Hom(F.c1,G.d1);
  func commaMorphs(F,G) -> non empty Subset of [:[:commaObjs(F,G), commaObjs(F
  ,G):], [:the carrier' of C, the carrier' of D:]:] equals
:: COMMACAT:def 2

  {[[o1,o2], [g,h]] :
    dom g = o1`11 & cod g = o2`11 & dom h = o1`12 & cod h = o2`12 &
   (o2`2)(*)(F.g) = (G.h)(*)(o1`2)};
end;

reserve k,k1,k2,k9 for Element of commaMorphs(F,G);

definition
  let C,D,E,F,G,k;
  redefine func k`11 -> Element of commaObjs(F,G);
  redefine func k`12 -> Element of commaObjs(F,G);
end;

theorem :: COMMACAT:2
  (ex c,d,f st f in Hom(F.c,G.d)) implies k = [[k`11,k`12], [k`21,k
`22]] & dom k`21 = k`11`11 & cod k`21 = k`12`11 & dom k`22 = k`11`12 & cod k`22
  = k`12`12 & (k`12`2)(*)(F.k`21) = (G.k`22)(*)(k`11`2);

definition
  let C,D,E,F,G,k1,k2;
  given c1,d1,f1 such that
 f1 in Hom(F.c1,G.d1);
  assume
 k1`12 = k2`11;
  func k2*k1 -> Element of commaMorphs(F,G) equals
:: COMMACAT:def 3

  [[k1`11,k2`12],[k2`21(*)k1`21,k2`22(*)k1`22]];
end;

definition
  let C,D,E,F,G;
  func commaComp(F,G) -> PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):],
  commaMorphs(F,G) means
:: COMMACAT:def 4

  dom it = { [k1,k2]: k1`11 = k2`12 } & for k,k9
  st [k,k9] in dom it holds it.[k,k9] = k*k9;
end;

definition
  let C,D,E,F,G;
  given c1,d1,f1 such that
 f1 in Hom(F.c1,G.d1);
  func F comma G -> strict Category means
:: COMMACAT:def 5
  the carrier of it = commaObjs(F,G) &
  the carrier' of it = commaMorphs(F,G) & (for k holds (the Source of it).k = k
`11) & (for k holds (the Target of it).k = k`12) &
    the Comp of it = commaComp(F,G);
end;

theorem :: COMMACAT:3
  the carrier of 1Cat(x,y) = {x} & the carrier' of 1Cat(x,y) = {y};

theorem :: COMMACAT:4
  for a,b being Object of 1Cat(x,y) holds Hom(a,b) = {y};

definition
  let C, c;
  func 1Cat c -> strict Subcategory of C equals
:: COMMACAT:def 6
  1Cat(c, id c);
end;

definition
  let C, c;
  func c comma C -> strict Category equals
:: COMMACAT:def 7
  (incl 1Cat c) comma (id C);
  func C comma c -> strict Category equals
:: COMMACAT:def 8
  (id C) comma (incl 1Cat c);
end;