The abstract of the Mizar article:

Examples of Category Structures

by

Adam Grabowski

Received June 11, 1996

MML identifier: MSINST_1

[ Mizar article, MML identifier index ]

environ

 vocabulary AMI_1, MSUALG_1, ALTCAT_1, MSALIMIT, FUNCT_1, CAT_1, PBOOLE,
      MCART_1, PUA2MSS1, PRALG_1, BOOLE, RELAT_1, RELAT_2, BINOP_1, MSUALG_6,
      TDGROUP, FUNCT_2, PARTFUN1, CARD_3, TARSKI, FUNCOP_1, ZF_REFLE, NATTRA_1,
      QC_LANG1, MSUALG_3, FUNCT_6, FINSEQ_4, ALG_1, MSINST_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, MCART_1, RELAT_1,
      FUNCT_1, STRUCT_0, FUNCT_2, MCART_2, RELSET_1, PARTFUN1, FINSEQ_2,
      CARD_3, BINOP_1, MULTOP_1, FUNCT_6, PBOOLE, PRALG_1, MSUALG_1, MSUALG_3,
      EXTENS_1, ALTCAT_1, PRALG_2, AUTALG_1, PUA2MSS1, MSUALG_6, MSALIMIT;
 constructors AUTALG_1, CLOSURE1, EXTENS_1, MCART_2, MSALIMIT, ALTCAT_1,
      PUA2MSS1, MSUALG_6;
 clusters ALTCAT_1, FUNCT_1, MSALIMIT, MSUALG_1, MSUALG_6, PRALG_1, RELSET_1,
      STRUCT_0, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin  :: Category of Many Sorted Signatures

 reserve A for non empty set,
         S for non void non empty ManySortedSign;
 reserve x for set;

definition let A;
  func MSSCat A -> strict non empty AltCatStr means
:: MSINST_1:def 1
   the carrier of it = MSS_set A &
   ( for i, j be Element of MSS_set A holds
   (the Arrows of it).(i,j) = MSS_morph (i,j) ) &
    for i,j,k be object of it st
     i in MSS_set A & j in MSS_set A & k in MSS_set A
     for f1,f2,g1,g2 be Function st
      [f1,f2] in (the Arrows of it).(i,j) &
      [g1,g2] in (the Arrows of it).(j,k) holds
       (the Comp of it).(i,j,k).([g1,g2],[f1,f2]) = [g1*f1,g2*f2];
end;

definition let A;
  cluster MSSCat A -> transitive associative with_units;
end;

theorem :: MSINST_1:1
   for C be category st C = MSSCat A
  for o be object of C holds o is non empty non void ManySortedSign;

definition let S;
  cluster strict feasible MSAlgebra over S;
end;

definition let S, A;
  func MSAlg_set (S,A) means
:: MSINST_1:def 2
   x in it iff ex M be strict feasible MSAlgebra over S st x = M &
     for C be Component of the Sorts of M holds C c= A;
end;

definition let S, A;
  cluster MSAlg_set (S,A) -> non empty;
end;

begin :: Category of Many Sorted Algebras

 reserve o for OperSymbol of S;

theorem :: MSINST_1:2
 for x be MSAlgebra over S st x in MSAlg_set (S,A) holds
  the Sorts of x in Funcs (the carrier of S, bool A) &
  the Charact of x in Funcs (the OperSymbols of S,PFuncs(PFuncs (NAT ,A),A));

theorem :: MSINST_1:3
 for U1,U2 be MSAlgebra over S
   st the Sorts of U1 is_transformable_to the Sorts of U2 &
      Args (o,U1) <> {} holds Args (o,U2) <> {};

theorem :: MSINST_1:4
for U1,U2,U3 be feasible MSAlgebra over S,
    F be ManySortedFunction of U1,U2,
    G be ManySortedFunction of U2,U3,
  x be Element of Args(o,U1) st Args (o,U1) <> {} &
    the Sorts of U1 is_transformable_to the Sorts of U2
  & the Sorts of U2 is_transformable_to the Sorts of U3
  ex GF be ManySortedFunction of U1,U3 st
   GF = G ** F & GF#x = G#(F#x);

theorem :: MSINST_1:5
for U1,U2,U3 be feasible MSAlgebra over S,
 F be ManySortedFunction of U1,U2,
 G be ManySortedFunction of U2,U3 st
  the Sorts of U1 is_transformable_to the Sorts of U2
  & the Sorts of U2 is_transformable_to the Sorts of U3
  & F is_homomorphism U1,U2 & G is_homomorphism U2,U3
  ex GF be ManySortedFunction of U1,U3 st
   GF = G ** F & GF is_homomorphism U1,U3;

definition let S, A; let i,j be set;
  assume  i in MSAlg_set (S,A) & j in MSAlg_set (S,A);
  func MSAlg_morph (S,A,i,j) means
:: MSINST_1:def 3
    x in it iff (ex M,N be strict feasible MSAlgebra over S,
     f be ManySortedFunction of M,N
     st M = i & N = j & f = x &
    the Sorts of M is_transformable_to the Sorts of N & f is_homomorphism M,N);
end;

definition let S, A;
  func MSAlgCat (S,A) -> strict non empty AltCatStr means
:: MSINST_1:def 4
   the carrier of it = MSAlg_set (S,A) &
 ( for i, j be Element of MSAlg_set (S,A) holds
 (the Arrows of it).(i,j) = MSAlg_morph (S,A,i,j) ) &
   ( for i,j,k be object of it, f,g be Function-yielding Function st
     f in (the Arrows of it).(i,j) &
     g in (the Arrows of it).(j,k) holds
   (the Comp of it).(i,j,k).(g,f) = ( g ** f ) );
end;

definition let S, A;
  cluster MSAlgCat (S,A) -> transitive associative with_units;
end;

theorem :: MSINST_1:6
    for C be category st C = MSAlgCat (S,A)
   for o be object of C holds
   o is strict feasible MSAlgebra over S;