The abstract of the Mizar article:

Category of Functors between Alternative Categories

by

Robert Nieszczerzewski

Received June 12, 1997

MML identifier: FUNCTOR2

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_2, ALTCAT_1, MSUALG_6, FUNCTOR0, CAT_1, FUNCT_1, BOOLE,
      NATTRA_1, PBOOLE, QC_LANG1, FUNCT_2, PRALG_1, CARD_3, RELAT_1, CAT_2,
      TARSKI, FUNCTOR2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCTOR0, MCART_1, DOMAIN_1,
      RELAT_1, STRUCT_0, CARD_3, FUNCT_1, FUNCT_2, BINOP_1, MULTOP_1, FRAENKEL,
      PBOOLE, MSUALG_1, ALTCAT_1;
 constructors FUNCTOR0, DOMAIN_1;
 clusters STRUCT_0, ALTCAT_1, FUNCTOR0, RELSET_1, SUBSET_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

definition let A be transitive with_units (non empty AltCatStr),
               B be with_units (non empty AltCatStr);
 cluster -> feasible id-preserving Functor of A, B;
end;

definition let A be transitive with_units (non empty AltCatStr),
               B be with_units (non empty AltCatStr);
 cluster covariant -> Covariant comp-preserving Functor of A, B;
 cluster Covariant comp-preserving -> covariant Functor of A, B;
 cluster contravariant -> Contravariant comp-reversing Functor of A, B;
 cluster Contravariant comp-reversing -> contravariant Functor of A, B;
end;

canceled;

 theorem :: FUNCTOR2:2
  for A,B being transitive with_units (non empty AltCatStr),
      F being covariant Functor of A,B
  for a being object of A holds F.idm a = idm (F.a);

begin :: Transformations

 definition
  let A,B be transitive with_units (non empty AltCatStr),
      F1,F2 be covariant Functor of A,B;
  pred F1 is_transformable_to F2 means
:: FUNCTOR2:def 1
   for a being object of A holds <^F1.a,F2.a^> <> {};
reflexivity;
 end;

canceled;

 theorem :: FUNCTOR2:4
  for A,B being transitive with_units (non empty AltCatStr),
      F,F1,F2 being covariant Functor of A,B holds
  F is_transformable_to F1 & F1 is_transformable_to F2 implies
  F is_transformable_to F2;

 definition
  let A,B be transitive with_units (non empty AltCatStr),
      F1,F2 be covariant Functor of A,B;
  assume  F1 is_transformable_to F2;
 mode transformation of F1,F2 ->
         ManySortedSet of the carrier of A means
:: FUNCTOR2:def 2
  for a being object of A holds it.a is Morphism of F1.a,F2.a;
 end;

 definition
  let A,B be transitive with_units (non empty AltCatStr);
  let F be covariant Functor of A,B;
 func idt F -> transformation of F,F means
:: FUNCTOR2:def 3
 for a being object of A holds it.a = idm (F.a);
 end;

 definition
  let A,B be transitive with_units (non empty AltCatStr),
      F1,F2 be covariant Functor of A,B;
  assume  F1 is_transformable_to F2;
  let t be transformation of F1,F2;
  let a be object of A;
 func t!a -> Morphism of F1.a, F2.a means
:: FUNCTOR2:def 4
  it = t.a;
 end;

 definition
  let A,B be transitive with_units (non empty AltCatStr),
      F,F1,F2 be covariant Functor of A,B;
  assume that
 F is_transformable_to F1 and
 F1 is_transformable_to F2;
  let t1 be transformation of F,F1;
  let t2 be transformation of F1,F2;
 func t2`*`t1 -> transformation of F,F2 means
:: FUNCTOR2:def 5
 for a being object of A holds it!a = (t2!a) * (t1!a);
 end;

 theorem :: FUNCTOR2:5
  for A,B being transitive with_units (non empty AltCatStr),
      F1,F2 being covariant Functor of A,B holds
  F1 is_transformable_to F2 implies
  for t1,t2 being transformation of F1,F2 st
   for a being object of A holds t1!a = t2!a
  holds t1 = t2;

theorem :: FUNCTOR2:6
 for A,B being transitive with_units (non empty AltCatStr),
     F being covariant Functor of A,B holds
 for a being object of A holds (idt F)!a = idm(F.a);

theorem :: FUNCTOR2:7
 for A,B being transitive with_units (non empty AltCatStr),
     F1,F2 being covariant Functor of A,B holds
 F1 is_transformable_to F2 implies
 for t being transformation of F1,F2 holds (idt F2)`*`t = t & t`*`(idt F1) = t;

theorem :: FUNCTOR2:8
  for A,B being category,
      F,F1,F2,F3 being covariant Functor of A,B holds
 F is_transformable_to F1 & F1 is_transformable_to F2 &
 F2 is_transformable_to F3 implies
 for t1 being transformation of F,F1, t2 being transformation of F1,F2,
     t3 being transformation of F2,F3
  holds t3`*`t2`*`t1 = t3`*`(t2`*`t1);

begin :: Natural transformations

definition
 let A,B be transitive with_units (non empty AltCatStr),
     F1,F2 be covariant Functor of A,B;
 pred F1 is_naturally_transformable_to F2 means
:: FUNCTOR2:def 6
 F1 is_transformable_to F2 &
 ex t being transformation of F1,F2 st
  for a,b being object of A st <^a,b^> <> {}
   for f being Morphism of a,b holds
    t!b*F1.f = F2.f*(t!a);
end;

theorem :: FUNCTOR2:9
 for A,B be transitive with_units (non empty AltCatStr),
  F be covariant Functor of A,B holds
 F is_naturally_transformable_to F;

theorem :: FUNCTOR2:10
 for A,B be category,
     F,F1,F2 be covariant Functor of A,B holds
 F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2
  implies F is_naturally_transformable_to F2;

definition
 let A,B be transitive with_units (non empty AltCatStr),
     F1,F2 be covariant Functor of A,B;
 assume F1 is_naturally_transformable_to F2;
 mode natural_transformation of F1,F2 -> transformation of F1,F2 means
:: FUNCTOR2:def 7
 for a,b being object of A st <^a,b^> <> {}
   for f being Morphism of a,b holds it!b*F1.f = F2.f*(it!a);
end;

definition
 let A,B be transitive with_units (non empty AltCatStr),
     F be covariant Functor of A,B;
 redefine func idt F -> natural_transformation of F,F;
end;

definition
 let A,B be category,
     F,F1,F2 be covariant Functor of A,B such that
 F is_naturally_transformable_to F1 and
 F1 is_naturally_transformable_to F2;
 let t1 be natural_transformation of F,F1;
 let t2 be natural_transformation of F1,F2;
 func t2`*`t1 -> natural_transformation of F,F2 means
:: FUNCTOR2:def 8
 it = t2`*`t1;
end;

theorem :: FUNCTOR2:11
   for A,B be transitive with_units (non empty AltCatStr),
     F1,F2 be covariant Functor of A,B holds
 F1 is_naturally_transformable_to F2 implies
 for t being natural_transformation of F1,F2 holds
   (idt F2)`*`t = t & t`*`(idt F1) = t;

theorem :: FUNCTOR2:12
   for A,B be transitive with_units (non empty AltCatStr),
     F,F1,F2 be covariant Functor of A,B holds
 F is_naturally_transformable_to F1 &
 F1 is_naturally_transformable_to F2 implies
 for t1 being natural_transformation of F,F1
 for t2 being natural_transformation of F1,F2
  for a being object of A
 holds (t2`*`t1)!a = (t2!a)*(t1!a);

theorem :: FUNCTOR2:13
   for A,B be category,
     F,F1,F2,F3 be covariant Functor of A,B
 for t be natural_transformation of F,F1,
     t1 be natural_transformation of F1,F2 holds
 F is_naturally_transformable_to F1 &
 F1 is_naturally_transformable_to F2 &
 F2 is_naturally_transformable_to F3 implies
 for t3 being natural_transformation of F2,F3 holds t3`*`t1`*`t = t3`*`(t1`*`t)
;

begin :: Category of Functors

definition
 let I be set;
 let A,B be ManySortedSet of I;
 func Funcs(A,B) -> set means
:: FUNCTOR2:def 9

 for x be set holds x in it iff x is ManySortedFunction of A,B
   if for i being set st i in I holds B.i = {} implies A.i = {}
   otherwise it = {};
 end;

definition
 let A,B be transitive with_units (non empty AltCatStr);
 func Funct(A,B) -> set means
:: FUNCTOR2:def 10

 for x being set holds x in it iff x is covariant strict Functor of A,B;
end;


definition let A,B be category;
 func Functors(A,B) -> strict non empty transitive AltCatStr means
:: FUNCTOR2:def 11
   the carrier of it = Funct(A,B) &
 (for F,G being strict covariant Functor of A,B, x being set holds
  x in (the Arrows of it).(F,G) iff
   F is_naturally_transformable_to G & x is natural_transformation of F,G) &
 for F,G,H being strict covariant Functor of A,B st
   F is_naturally_transformable_to G & G is_naturally_transformable_to H
  for t1 being natural_transformation of F,G,
      t2 being natural_transformation of G,H
  ex f being Function st f = (the Comp of it).(F,G,H) & f.(t2,t1) = t2`*`t1;
 end;