The Mizar abstract of FUNCTOR0

Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users
The abstract of the Mizar article:: Functors for Alternative Categories
by
Andrzej Trybulec
Received April 24, 1996
MML identifier: FUNCTOR0
[ Mizar article, MML identifier index ]
environ

 vocabulary FUNCT_1, MCART_1, BOOLE, RELAT_1, PBOOLE, SGRAPH1, PRALG_1,
      FUNCOP_1, MSUALG_3, CAT_4, ALTCAT_1, RELAT_2, MSUALG_6, CAT_1, ALTCAT_2,
      FUNCT_3, ENS_1, WELLORD1, FUNCTOR0;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, MCART_1,
      FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCOP_1, FUNCT_3, FUNCT_4, PBOOLE,
      STRUCT_0, PRALG_1, MSUALG_1, MSUALG_3, ALTCAT_1, ALTCAT_2;
 constructors ALTCAT_2, MCART_1;
 clusters RELAT_1, FUNCT_1, ALTCAT_1, ALTCAT_2, MSUALG_1, STRUCT_0, PRALG_1,
      RELSET_1, SUBSET_1, FUNCT_2;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

scheme ValOnPair
  {X()-> non empty set,f()-> Function,
   x1,x2()-> Element of X(), F(set,set)-> set, P[set,set]}:
 f().(x1(),x2()) = F(x1(),x2())
provided
 f() = { [[o,o'],F(o,o')]
         where o is Element of X(), o' is Element of X(): P[o,o'] } and
 P[x1(),x2()];

theorem :: FUNCTOR0:1
 for A being set holds {} is Function of A,{};

canceled;

theorem :: FUNCTOR0:3
 for I being set for M being ManySortedSet of I holds M*id I = M;

definition let f be empty Function;
  cluster ~f -> empty;
 let g be Function;
  cluster [:f,g:] -> empty;
  cluster [:g,f:] -> empty;
end;

theorem :: FUNCTOR0:4
 for A being set, f being Function holds f.:id A = (~f).:id A;

theorem :: FUNCTOR0:5
 for X,Y being set, f being Function of X,Y holds
  f is onto iff [:f,f:] is onto;

definition let f be Function-yielding Function;
 cluster ~f -> Function-yielding;
end;

theorem :: FUNCTOR0:6
 for A,B being set, a being set
   holds ~([:A,B:] --> a) = [:B,A:] --> a;

theorem :: FUNCTOR0:7
 for f,g being Function st f is one-to-one & g is one-to-one holds
  [:f,g:]" = [:f",g":];

theorem :: FUNCTOR0:8
 for f being Function st [:f,f:] is one-to-one holds f is one-to-one;

theorem :: FUNCTOR0:9
 for f being Function st f is one-to-one
  holds ~f is one-to-one;

theorem :: FUNCTOR0:10
 for f,g being Function st ~[:f,g:] is one-to-one
  holds [:g,f:] is one-to-one;

theorem :: FUNCTOR0:11
 for f,g being Function st f is one-to-one & g is one-to-one holds
  ~[:f,g:]" = ~([:g,f:]");

theorem :: FUNCTOR0:12
 for A,B be set, f being Function of A,B st f is onto
  holds id B c= [:f,f:].:id A;

theorem :: FUNCTOR0:13
 for F,G being Function-yielding Function, f be Function
  holds (G**F)*f = (G*f)**(F*f);

definition let A,B,C be set, f be Function of [:A,B:],C;
 redefine func ~f -> Function of [:B,A:],C;
end;

theorem :: FUNCTOR0:14
 for A,B,C being set,
    f being Function of [:A,B:],C st ~f is onto
  holds f is onto;

theorem :: FUNCTOR0:15
 for A be set, B being non empty set, f being Function of A,B
  holds [:f,f:].:id A c= id B;

begin :: Functions bewteen Cartesian products

definition let A,B be set;
 mode bifunction of A,B is Function of [:A,A:],[:B,B:];
 canceled;
end;

definition let A,B be set, f be bifunction of A,B;
 attr f is Covariant means
:: FUNCTOR0:def 2
 ex g being Function of A,B st f = [:g,g:];
 attr f is Contravariant means
:: FUNCTOR0:def 3
 ex g being Function of A,B st f = ~[:g,g:];
end;

theorem :: FUNCTOR0:16
 for A be set, B be non empty set,
     b being Element of B, f being bifunction of A,B
      st f = [:A,A:] --> [b,b]
  holds f is Covariant Contravariant;

definition let A,B be set;
 cluster Covariant Contravariant bifunction of A,B;
end;

theorem :: FUNCTOR0:17
   for A,B being non empty set
 for f being Covariant Contravariant bifunction of A,B
  ex b being Element of B st f = [:A,A:] --> [b,b];


begin :: Unary transformatiom

definition let I1,I2 be set, f be Function of I1,I2;
 let A be ManySortedSet of I1, B be ManySortedSet of I2;
 mode MSUnTrans of f,A,B -> ManySortedSet of I1 means
:: FUNCTOR0:def 4
 ex I2' being non empty set, B' being ManySortedSet of I2',
        f' being Function of I1,I2' st f = f' & B = B' &
            it is ManySortedFunction of A,B'*f' if I2 <> {}
       otherwise it = [0]I1;
end;

definition let I1 be set, I2 be non empty set, f be Function of I1,I2;
 let A be ManySortedSet of I1, B be ManySortedSet of I2;
 redefine mode MSUnTrans of f,A,B means
:: FUNCTOR0:def 5
 it is ManySortedFunction of A,B*f;
end;

definition let I1,I2 be set; let f be Function of I1,I2;
 let A be ManySortedSet of I1, B be ManySortedSet of I2;
 cluster -> Function-yielding MSUnTrans of f,A,B;
end;

theorem :: FUNCTOR0:18
 for I1 being set, I2,I3 being non empty set,
     f being Function of I1,I2, g being Function of I2,I3,
     B being ManySortedSet of I2, C being ManySortedSet of I3,
     G being MSUnTrans of g,B,C
holds G*f is MSUnTrans of g*f,B*f,C;

definition let I1 be set, I2 be non empty set,
     f be Function of I1,I2,
     A be ManySortedSet of [:I1,I1:], B be ManySortedSet of [:I2,I2:],
     F be MSUnTrans of [:f,f:],A,B;
 redefine func ~F -> MSUnTrans of [:f,f:],~A,~B;
end;

theorem :: FUNCTOR0:19
 for I1,I2 being non empty set,
     A being ManySortedSet of I1, B being ManySortedSet of I2,
     o being Element of I2 st B.o <> {}
 for m being Element of B.o, f being Function of I1,I2 st f = I1 --> o
  holds
   { [o',A.o' --> m] where o' is Element of I1: not contradiction }
      is MSUnTrans of f,A,B;

theorem :: FUNCTOR0:20
 for I1 being set, I2,I3 being non empty set,
     f being Function of I1,I2, g being Function of I2,I3,
     A being ManySortedSet of I1, B being ManySortedSet of I2,
     C being ManySortedSet of I3, F being MSUnTrans of f,A,B,
     G being MSUnTrans of g*f,B*f,C
   st for ii being set st ii in I1 & (B*f).ii = {}
       holds A.ii = {} or (C*(g*f)).ii = {}
  holds G**(F qua Function-yielding Function) is MSUnTrans of g*f,A,C;

begin :: Functors

definition let C1,C2 be 1-sorted;
 struct BimapStr over C1,C2
    (#ObjectMap -> bifunction of the carrier of C1, the carrier of C2 #);
end;

definition let C1,C2 be non empty AltGraph;
 let F be BimapStr over C1,C2; let o be object of C1;
 func F.o -> object of C2 equals
:: FUNCTOR0:def 6
  ((the ObjectMap of F).(o,o))`1;
end;

definition let A,B be 1-sorted, F be BimapStr over A,B;
 attr F is one-to-one means
:: FUNCTOR0:def 7
 the ObjectMap of F is one-to-one;
 attr F is onto means
:: FUNCTOR0:def 8
 the ObjectMap of F is onto;
 attr F is reflexive means
:: FUNCTOR0:def 9

 (the ObjectMap of F).:id the carrier of A c= id the carrier of B;
 attr F is coreflexive means
:: FUNCTOR0:def 10

 id the carrier of B c= (the ObjectMap of F).:id the carrier of A;
end;

definition let A,B be non empty AltGraph, F be BimapStr over A,B;
 redefine attr F is reflexive means
:: FUNCTOR0:def 11
 for o being object of A holds (the ObjectMap of F).(o,o) = [F.o,F.o];
end;

theorem :: FUNCTOR0:21
 for A,B being reflexive non empty AltGraph,
     F being BimapStr over A,B st F is coreflexive
 for o being object of B
  ex o' being object of A st F.o' = o;

definition let C1, C2 be non empty AltGraph;
 let F be BimapStr over C1,C2;
 attr F is feasible means
:: FUNCTOR0:def 12
 for o1,o2 being object of C1 st <^o1,o2^> <> {} holds
       (the Arrows of C2).((the ObjectMap of F).(o1,o2)) <> {};
end;

definition let C1,C2 be AltGraph;
 struct(BimapStr over C1,C2) FunctorStr over C1,C2
    (#ObjectMap -> bifunction of the carrier of C1,the carrier of C2,
     MorphMap ->
       MSUnTrans of the ObjectMap, the Arrows of C1, the Arrows of C2 #);
end;

definition let C1,C2 be 1-sorted;
 let IT be BimapStr over C1,C2;
 attr IT is Covariant means
:: FUNCTOR0:def 13
 the ObjectMap of IT is Covariant;
 attr IT is Contravariant means
:: FUNCTOR0:def 14
 the ObjectMap of IT is Contravariant;
end;

definition let C1,C2 be AltGraph;
 cluster Covariant FunctorStr over C1,C2;
 cluster Contravariant FunctorStr over C1,C2;
end;

definition let C1,C2 be AltGraph;
 let F be FunctorStr over C1,C2; let o1,o2 be object of C1;
 func Morph-Map(F,o1,o2) equals
:: FUNCTOR0:def 15

  (the MorphMap of F).(o1,o2);
end;

definition let C1,C2 be AltGraph;
 let F be FunctorStr over C1,C2; let o1,o2 be object of C1;
 cluster Morph-Map(F,o1,o2) -> Relation-like Function-like;
end;

definition let C1,C2 be non empty AltGraph;
 let F be Covariant FunctorStr over C1,C2; let o1,o2 be object of C1;
 redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o1,F.o2^>;
end;

definition let C1,C2 be non empty AltGraph;
 let F be Covariant FunctorStr over C1,C2; let o1,o2 be object of C1 such that
 <^o1,o2^> <> {} & <^F.o1,F.o2^> <> {};
 let m be Morphism of o1,o2;
 func F.m -> Morphism of F.o1, F.o2 equals
:: FUNCTOR0:def 16
  Morph-Map(F,o1,o2).m;
end;

definition let C1,C2 be non empty AltGraph;
 let F be Contravariant FunctorStr over C1,C2; let o1,o2 be object of C1;
 redefine func Morph-Map(F,o1,o2) -> Function of <^o1,o2^>, <^F.o2,F.o1^>;
end;

definition let C1,C2 be non empty AltGraph;
 let F be Contravariant FunctorStr over C1,C2;
 let o1,o2 be object of C1 such that
 <^o1,o2^> <> {} & <^F.o2,F.o1^> <> {};
 let m be Morphism of o1,o2;
 func F.m -> Morphism of F.o2, F.o1 equals
:: FUNCTOR0:def 17
  Morph-Map(F,o1,o2).m;
end;

definition
 let C1,C2 be non empty AltGraph;
 let o be object of C2 such that
 <^o,o^> <> {};
 let m be Morphism of o,o;
 func C1 --> m -> strict FunctorStr over C1,C2 means
:: FUNCTOR0:def 18

  the ObjectMap of it = [:the carrier of C1,the carrier of C1:] --> [o,o] &
  the MorphMap of it =
   { [[o1,o2],<^o1,o2^> --> m] where o1 is object of C1, o2 is object of C1:
      not contradiction };
end;

theorem :: FUNCTOR0:22
 for C1,C2 being non empty AltGraph, o2 being object of C2 st <^o2,o2^> <> {}
 for m be Morphism of o2,o2, o1 being object of C1
  holds (C1 --> m).o1 = o2;

definition
 let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
 let o be object of C2, m be Morphism of o,o;
 cluster C1 --> m -> Covariant Contravariant feasible;
end;

definition
 let C1 be non empty AltGraph, C2 be non empty reflexive AltGraph;
 cluster feasible Covariant Contravariant FunctorStr over C1,C2;
end;

theorem :: FUNCTOR0:23
 for C1, C2 being non empty AltGraph,
     F being Covariant FunctorStr over C1,C2,
     o1,o2 being object of C1
 holds (the ObjectMap of F).(o1,o2) = [F.o1,F.o2];

definition let C1, C2 be non empty AltGraph;
 let F be Covariant FunctorStr over C1,C2;
 redefine attr F is feasible means
:: FUNCTOR0:def 19

 for o1,o2 being object of C1 st <^o1,o2^> <> {} holds <^F.o1,F.o2^> <> {};
end;

theorem :: FUNCTOR0:24
 for C1, C2 being non empty AltGraph,
     F being Contravariant FunctorStr over C1,C2,
     o1,o2 being object of C1
 holds (the ObjectMap of F).(o1,o2) = [F.o2,F.o1];

definition let C1, C2 be non empty AltGraph;
 let F be Contravariant FunctorStr over C1,C2;
 redefine attr F is feasible means
:: FUNCTOR0:def 20

 for o1,o2 being object of C1 st <^o1,o2^> <> {} holds <^F.o2,F.o1^> <> {};
end;

definition let C1,C2 be AltGraph;
 let F be FunctorStr over C1,C2;
 cluster the MorphMap of F -> Function-yielding;
end;

definition
 cluster non empty reflexive AltCatStr;
end;

:: Wlasnosci funktorow, Semadeni-Wiweger str. 32

definition let C1,C2 be with_units (non empty AltCatStr);
 let F be FunctorStr over C1,C2;
 attr F is id-preserving means
:: FUNCTOR0:def 21
  for o being object of C1
   holds Morph-Map(F,o,o).idm o = idm F.o;
end;

theorem :: FUNCTOR0:25
 for C1,C2 being non empty AltGraph, o2 being object of C2 st <^o2,o2^> <> {}
 for m be Morphism of o2,o2, o,o' being object of C1, f being Morphism of o,o'
   st <^o,o'^> <> {}
  holds Morph-Map(C1 --> m,o,o').f = m;

definition
 cluster with_units -> reflexive (non empty AltCatStr);
end;

definition let C1,C2 be with_units (non empty AltCatStr);
 let o2 be object of C2;
 cluster C1 --> idm o2 -> id-preserving;
end;

definition let C1 be non empty AltGraph;
 let C2 be non empty reflexive AltGraph;
 let o2 be object of C2; let m be Morphism of o2,o2;
 cluster C1 --> m -> reflexive;
end;

definition let C1 be non empty AltGraph;
 let C2 be non empty reflexive AltGraph;
 cluster feasible reflexive FunctorStr over C1,C2;
end;

definition let C1,C2 be with_units (non empty AltCatStr);
 cluster id-preserving feasible reflexive strict FunctorStr over C1,C2;
end;

definition let C1,C2 be non empty AltCatStr;
 let F be FunctorStr over C1,C2;
 attr F is comp-preserving means
:: FUNCTOR0:def 22
  for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
  for f being Morphism of o1,o2, g being Morphism of o2,o3
   ex f' being Morphism of F.o1,F.o2, g' being Morphism of F.o2,F.o3 st
      f' = Morph-Map(F,o1,o2).f & g' = Morph-Map(F,o2,o3).g &
      Morph-Map(F,o1,o3).(g*f) = g'*f';
end;

definition let C1,C2 be non empty AltCatStr;
 let F be FunctorStr over C1,C2;
 attr F is comp-reversing means
:: FUNCTOR0:def 23
 for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
     for f being Morphism of o1,o2, g being Morphism of o2,o3
   ex f' being Morphism of F.o2,F.o1, g' being Morphism of F.o3,F.o2 st
      f' = Morph-Map(F,o1,o2).f & g' = Morph-Map(F,o2,o3).g &
      Morph-Map(F,o1,o3).(g*f) = f'*g';
end;

definition let C1 be non empty transitive AltCatStr;
 let C2 be non empty reflexive AltCatStr;
 let F be Covariant feasible FunctorStr over C1,C2;
 redefine attr F is comp-preserving means
:: FUNCTOR0:def 24
    for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
  for f being Morphism of o1,o2, g being Morphism of o2,o3
     holds F.(g*f) = (F.g)*(F.f);
end;

definition let C1 be non empty transitive AltCatStr;
 let C2 be non empty reflexive AltCatStr;
 let F be Contravariant feasible FunctorStr over C1,C2;
 redefine attr F is comp-reversing means
:: FUNCTOR0:def 25
    for o1,o2,o3 being object of C1 st <^o1,o2^> <> {} & <^o2,o3^> <> {}
  for f being Morphism of o1,o2, g being Morphism of o2,o3
     holds F.(g*f) = (F.f)*(F.g);
end;

theorem :: FUNCTOR0:26
 for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
     o2 being object of C2, m be Morphism of o2,o2,
     F being Covariant feasible FunctorStr over C1,C2 st F = C1 --> m
 for o,o' being object of C1, f being Morphism of o,o'
   st <^o,o'^> <> {}
  holds F.f = m;

theorem :: FUNCTOR0:27
 for C1 being non empty AltGraph, C2 being non empty reflexive AltGraph,
     o2 being object of C2, m be Morphism of o2,o2,
     o,o' being object of C1, f being Morphism of o,o'
   st <^o,o'^> <> {}
  holds (C1 --> m).f = m;

definition
 let C1 be non empty transitive AltCatStr,
     C2 be with_units (non empty AltCatStr);
 let o be object of C2;
 cluster C1 --> idm o -> comp-preserving comp-reversing;
end;

definition
 let C1 be transitive with_units (non empty AltCatStr),
     C2 be with_units (non empty AltCatStr);
 mode Functor of C1,C2 -> FunctorStr over C1,C2 means
:: FUNCTOR0:def 26
  it is feasible id-preserving &
  (it is Covariant comp-preserving or it is Contravariant comp-reversing);
end;

definition
 let C1 be transitive with_units (non empty AltCatStr),
     C2 be with_units (non empty AltCatStr),
     F be Functor of C1,C2;
 attr F is covariant means
:: FUNCTOR0:def 27
   F is Covariant comp-preserving;
 attr F is contravariant means
:: FUNCTOR0:def 28
   F is Contravariant comp-reversing;
end;

definition let A be AltCatStr, B be SubCatStr of A;
 func incl B -> strict FunctorStr over B,A means
:: FUNCTOR0:def 29
 the ObjectMap of it = id [:the carrier of B, the carrier of B:] &
  the MorphMap of it = id the Arrows of B;
end;

definition let A be AltGraph;
 func id A -> strict FunctorStr over A,A means
:: FUNCTOR0:def 30
 the ObjectMap of it = id [:the carrier of A, the carrier of A:] &
  the MorphMap of it = id the Arrows of A;
end;

definition let A be AltCatStr, B be SubCatStr of A;
 cluster incl B -> Covariant;
end;

theorem :: FUNCTOR0:28
 for A being non empty AltCatStr, B being non empty SubCatStr of A,
     o being object of B
   holds (incl B).o = o;

theorem :: FUNCTOR0:29
 for A being non empty AltCatStr, B being non empty SubCatStr of A,
     o1,o2 being object of B
   holds <^o1,o2^> c= <^(incl B).o1,(incl B).o2^>;

definition let A be non empty AltCatStr, B be non empty SubCatStr of A;
 cluster incl B -> feasible;
end;

definition let A,B be AltGraph, F be FunctorStr over A,B;
 attr F is faithful means
:: FUNCTOR0:def 31
 the MorphMap of F is "1-1";
end;

definition let A,B be AltGraph, F be FunctorStr over A,B;
 attr F is full means
:: FUNCTOR0:def 32
 ex B' being ManySortedSet of [:the carrier of A, the carrier of A:],
        f being ManySortedFunction of (the Arrows of A),B' st
       B' = (the Arrows of B)*the ObjectMap of F & f = the MorphMap of F
          & f is "onto";
end;

definition
 let A be AltGraph, B be non empty AltGraph, F be FunctorStr over A,B;
 redefine attr F is full means
:: FUNCTOR0:def 33
 ex f being ManySortedFunction of (the Arrows of A),
                                      (the Arrows of B)*the ObjectMap of F st
       f = the MorphMap of F & f is "onto";
end;

definition let A,B be AltGraph, F be FunctorStr over A,B;
 attr F is injective means
:: FUNCTOR0:def 34
 F is one-to-one faithful;
 attr F is surjective means
:: FUNCTOR0:def 35
 F is full onto;
end;

definition let A,B be AltGraph, F be FunctorStr over A,B;
 attr F is bijective means
:: FUNCTOR0:def 36
 F is injective surjective;
end;

definition let A,B be transitive with_units (non empty AltCatStr);
 cluster strict covariant contravariant feasible Functor of A,B;
end;

theorem :: FUNCTOR0:30
 for A being non empty AltGraph, o being object of A
  holds (id A).o = o;

theorem :: FUNCTOR0:31
 for A being non empty AltGraph, o1,o2 being object of A st <^o1,o2^> <> {}
 for m being Morphism of o1,o2
  holds Morph-Map(id A,o1,o2).m = m;

definition let A be non empty AltGraph;
 cluster id A -> feasible Covariant;
end;

definition let A be non empty AltGraph;
 cluster Covariant feasible FunctorStr over A,A;
end;

theorem :: FUNCTOR0:32
 for A being non empty AltGraph, o1,o2 being object of A st <^o1,o2^> <> {}
 for F being Covariant feasible FunctorStr over A,A st F = id A
 for m being Morphism of o1,o2
  holds F.m = m;

definition let A be transitive with_units (non empty AltCatStr);
 cluster id A -> id-preserving comp-preserving;
end;

definition let A be transitive with_units (non empty AltCatStr);
 redefine func id A -> strict covariant Functor of A,A;
end;

definition let A be AltGraph;
 cluster id A -> bijective;
end;

begin :: The composition of functors

definition
 let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
 let F be feasible FunctorStr over C1,C2, G be FunctorStr over C2,C3;
 func G*F -> strict FunctorStr over C1,C3 means
:: FUNCTOR0:def 37
 the ObjectMap of it = (the ObjectMap of G)*the ObjectMap of F &
  the MorphMap of it =
   ((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
 let F be Covariant feasible FunctorStr over C1,C2,
     G be Covariant FunctorStr over C2,C3;
 cluster G*F -> Covariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
 let F be Contravariant feasible FunctorStr over C1,C2,
     G be Covariant FunctorStr over C2,C3;
 cluster G*F -> Contravariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
 let F be Covariant feasible FunctorStr over C1,C2,
     G be Contravariant FunctorStr over C2,C3;
 cluster G*F -> Contravariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
 let F be Contravariant feasible FunctorStr over C1,C2,
     G be Contravariant FunctorStr over C2,C3;
 cluster G*F -> Covariant;
end;

definition let C1 be non empty AltGraph, C2,C3 be non empty reflexive AltGraph;
 let F be feasible FunctorStr over C1,C2,
     G be feasible FunctorStr over C2,C3;
 cluster G*F -> feasible;
end;

theorem :: FUNCTOR0:33
   for C1 being non empty AltGraph,
     C2,C3,C4 being non empty reflexive AltGraph,
     F being feasible FunctorStr over C1,C2,
     G being feasible FunctorStr over C2,C3,
     H being FunctorStr over C3,C4
 holds H*G*F = H*(G*F);

theorem :: FUNCTOR0:34
 for C1 being non empty AltCatStr, C2,C3 being non empty reflexive AltCatStr,
     F be feasible reflexive FunctorStr over C1,C2, G be FunctorStr over C2,C3,
     o be object of C1
 holds (G*F).o = G.(F.o);

theorem :: FUNCTOR0:35
 for C1 being non empty AltGraph,
     C2,C3 being non empty reflexive AltGraph,
     F be feasible reflexive FunctorStr over C1,C2,
     G be FunctorStr over C2,C3,
     o be object of C1
 holds Morph-Map(G*F,o,o) = Morph-Map(G,F.o,F.o)*Morph-Map(F,o,o);

definition let C1,C2,C3 be with_units (non empty AltCatStr);
 let F be id-preserving feasible reflexive FunctorStr over C1,C2;
 let G be id-preserving FunctorStr over C2,C3;
  cluster G*F -> id-preserving;
end;

definition let A,C be non empty reflexive AltCatStr;
 let B be non empty SubCatStr of A;
 let F be FunctorStr over A,C;
 func F|B -> FunctorStr over B,C equals
:: FUNCTOR0:def 38
    F*incl B;
end;

begin :: The inverse functor

definition let A,B be non empty AltGraph, F be FunctorStr over A,B;
 assume
 F is bijective;
 func F" -> strict FunctorStr over B,A means
:: FUNCTOR0:def 39
 the ObjectMap of it = (the ObjectMap of F)" &
   ex f being ManySortedFunction of (the Arrows of A),
                                    (the Arrows of B)*the ObjectMap of F st
       f = the MorphMap of F & the MorphMap of it = f""*(the ObjectMap of F)";
end;

theorem :: FUNCTOR0:36
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible FunctorStr over A,B st F is bijective
 holds F" is bijective feasible;

theorem :: FUNCTOR0:37
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible reflexive FunctorStr over A,B st
       F is bijective coreflexive
 holds F" is reflexive;

theorem :: FUNCTOR0:38
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible reflexive id-preserving FunctorStr over A,B
          st F is bijective coreflexive
 holds F" is id-preserving;

theorem :: FUNCTOR0:39
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible FunctorStr over A,B st F is bijective Covariant
  holds F" is Covariant;

theorem :: FUNCTOR0:40
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible FunctorStr over A,B st F is bijective Contravariant
  holds F" is Contravariant;

theorem :: FUNCTOR0:41
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible reflexive FunctorStr over A,B
          st F is bijective coreflexive Covariant
 for o1,o2 being object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {}
  holds Morph-Map(F,F".o1,F".o2).(Morph-Map(F",o1,o2).m) = m;

theorem :: FUNCTOR0:42
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible reflexive FunctorStr over A,B
          st F is bijective coreflexive Contravariant
 for o1,o2 being object of B, m being Morphism of o1,o2 st <^o1,o2^> <> {}
  holds Morph-Map(F,F".o2,F".o1).(Morph-Map(F",o1,o2).m) = m;

theorem :: FUNCTOR0:43
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible reflexive FunctorStr over A,B st
        F is bijective comp-preserving Covariant coreflexive
 holds F" is comp-preserving;

theorem :: FUNCTOR0:44
 for A,B being transitive with_units (non empty AltCatStr),
     F being feasible reflexive FunctorStr over A,B st
        F is bijective comp-reversing Contravariant coreflexive
 holds F" is comp-reversing;

definition let C1 be 1-sorted, C2 be non empty 1-sorted;
 cluster Covariant -> reflexive BimapStr over C1,C2;
end;

definition let C1 be 1-sorted, C2 be non empty 1-sorted;
 cluster Contravariant -> reflexive BimapStr over C1,C2;
end;

theorem :: FUNCTOR0:45
 for C1,C2 being 1-sorted, M being BimapStr over C1,C2
  st M is Covariant onto holds M is coreflexive;

theorem :: FUNCTOR0:46
 for C1,C2 being 1-sorted, M being BimapStr over C1,C2
  st M is Contravariant onto holds M is coreflexive;

definition
 let C1 be transitive with_units (non empty AltCatStr),
     C2 be with_units (non empty AltCatStr);
 cluster covariant -> reflexive Functor of C1,C2;
end;

definition
 let C1 be transitive with_units (non empty AltCatStr),
     C2 be with_units (non empty AltCatStr);
 cluster contravariant -> reflexive Functor of C1,C2;
end;

theorem :: FUNCTOR0:47
 for C1 being transitive with_units (non empty AltCatStr),
     C2 being with_units (non empty AltCatStr),
     F being Functor of C1,C2 st F is covariant onto
  holds F is coreflexive;

theorem :: FUNCTOR0:48
 for C1 being transitive with_units (non empty AltCatStr),
     C2 being with_units (non empty AltCatStr),
     F being Functor of C1,C2 st F is contravariant onto
  holds F is coreflexive;

theorem :: FUNCTOR0:49
 for A,B being transitive with_units (non empty AltCatStr),
     F being covariant Functor of A,B st F is bijective
  ex G being Functor of B,A st G = F" & G is bijective covariant;

theorem :: FUNCTOR0:50
 for A,B being transitive with_units (non empty AltCatStr),
     F being contravariant Functor of A,B st F is bijective
  ex G being Functor of B,A st G = F" & G is bijective contravariant;

definition let A,B be transitive with_units (non empty AltCatStr);
 pred A,B are_isomorphic means
:: FUNCTOR0:def 40
   ex F being Functor of A,B st F is bijective covariant;
 reflexivity;
 symmetry;
 pred A,B are_anti-isomorphic means
:: FUNCTOR0:def 41
   ex F being Functor of A,B st F is bijective contravariant;
 symmetry;
end;
The abstract of the Mizar article:

Functors for Alternative Categories
