:: The Composition of Functors and Transformations in Alternative
:: Categories
::  by Artur Korni{\l}owicz
::
:: Received January 21, 1998
:: Copyright (c) 1998-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 RELAT_2, BINOP_1, ALTCAT_1, STRUCT_0, XBOOLE_0, FUNCTOR0,
      MSUALG_6, FUNCOP_1, CAT_1, RELAT_1, FUNCT_1, ZFMISC_1, TARSKI, MEMBER_1,
      PBOOLE, NATTRA_1, PZFMISC1, REALSET1, FUNCTOR2, VALUED_1, ALTCAT_3,
      CAT_3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      STRUCT_0, BINOP_1, FUNCOP_1, PBOOLE, MSUALG_3, ALTCAT_1, ALTCAT_2,
      ALTCAT_3, FUNCTOR0, FUNCTOR2;
 constructors MSUALG_3, ALTCAT_3, FUNCTOR2, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1,
      RELAT_1, PBOOLE, STRUCT_0, ALTCAT_1, FUNCTOR0, FUNCTOR2, ALTCAT_4,
      ALTCAT_2;
 requirements SUBSET, BOOLE;


begin  :: Preliminaries

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

registration
  let A be non empty transitive AltCatStr, B be with_units non empty
  AltCatStr;
  cluster strict comp-preserving comp-reversing Covariant Contravariant
    feasible for FunctorStr over A, B;
end;

registration
  let A be with_units transitive non empty AltCatStr, B be with_units non
  empty AltCatStr;
  cluster strict comp-preserving comp-reversing Covariant Contravariant
    feasible id-preserving for FunctorStr over A, B;
end;

registration
  let A be with_units transitive non empty AltCatStr, B be with_units non
  empty AltCatStr;
  cluster strict feasible covariant contravariant for Functor of A, B;
end;

theorem :: FUNCTOR3:1
  for C being category, o1, o2, o3, o4 being Object of C for a being
Morphism of o1, o2, b being Morphism of o2, o3 for c being Morphism of o1, o4,
d being Morphism of o4, o3 st b*a = d*c & a*(a") = idm o2 & d"*d = idm o4 & <^
o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^>
  <> {} holds c*(a") = d"*b;

theorem :: FUNCTOR3:2
  for A being non empty transitive AltCatStr for B, C being with_units
non empty AltCatStr for F being feasible Covariant FunctorStr over A, B for G
being FunctorStr over B, C, o, o1 being Object of A holds Morph-Map(G*F,o,o1) =
  Morph-Map(G,F.o,F.o1)*Morph-Map(F,o,o1);

theorem :: FUNCTOR3:3
  for A being non empty transitive AltCatStr for B, C being with_units
  non empty AltCatStr for F being feasible Contravariant FunctorStr over A, B
for G being FunctorStr over B, C, o, o1 being Object of A holds Morph-Map(G*F,o
  ,o1) = Morph-Map(G,F.o1,F.o)*Morph-Map(F,o,o1);

theorem :: FUNCTOR3:4
  for A being non empty transitive AltCatStr for B being with_units non
  empty AltCatStr for F being feasible FunctorStr over A, B holds (id B) * F =
  the FunctorStr of F;

theorem :: FUNCTOR3:5
  for A being with_units transitive non empty AltCatStr for B being
  with_units non empty AltCatStr for F being feasible FunctorStr over A, B
  holds F * (id A) = the FunctorStr of F;

reserve A for non empty AltCatStr,
  B, C for non empty reflexive AltCatStr,
  F for feasible Covariant FunctorStr over A, B,
  G for feasible Covariant FunctorStr over B, C,
  M for feasible Contravariant FunctorStr over A, B,
  N for feasible Contravariant FunctorStr over B, C,
  o1, o2 for Object of A,
  m for Morphism of o1, o2;

theorem :: FUNCTOR3:6
  <^o1,o2^> <> {} implies (G*F).m = G.(F.m);

theorem :: FUNCTOR3:7
  <^o1,o2^> <> {} implies (N*M).m = N.(M.m);

theorem :: FUNCTOR3:8
  <^o1,o2^> <> {} implies (N*F).m = N.(F.m);

theorem :: FUNCTOR3:9
  <^o1,o2^> <> {} implies (G*M).m = G.(M.m);

registration
  let A be non empty transitive AltCatStr, B be transitive with_units non
  empty AltCatStr, C be with_units non empty AltCatStr, F be feasible
  Covariant comp-preserving FunctorStr over A, B, G be feasible Covariant
  comp-preserving FunctorStr over B, C;
  cluster G*F -> comp-preserving;
end;

registration
  let A be non empty transitive AltCatStr, B be transitive with_units non
  empty AltCatStr, C be with_units non empty AltCatStr, F be feasible
Contravariant comp-reversing FunctorStr over A, B, G be feasible Contravariant
  comp-reversing FunctorStr over B, C;
  cluster G*F -> comp-preserving;
end;

registration
  let A be non empty transitive AltCatStr, B be transitive with_units non
  empty AltCatStr, C be with_units non empty AltCatStr, F be feasible
  Covariant comp-preserving FunctorStr over A, B, G be feasible Contravariant
  comp-reversing FunctorStr over B, C;
  cluster G*F -> comp-reversing;
end;

registration
  let A be non empty transitive AltCatStr, B be transitive with_units non
  empty AltCatStr, C be with_units non empty AltCatStr, F be feasible
  Contravariant comp-reversing FunctorStr over A, B, G be feasible Covariant
  comp-preserving FunctorStr over B, C;
  cluster G*F -> comp-reversing;
end;

definition
  let A, B be transitive with_units non empty AltCatStr, C be with_units
non empty AltCatStr, F be covariant Functor of A, B, G be covariant Functor of
  B, C;
  redefine func G*F -> strict covariant Functor of A, C;
end;

definition
  let A, B be transitive with_units non empty AltCatStr, C be with_units
  non empty AltCatStr, F be contravariant Functor of A, B, G be contravariant
  Functor of B, C;
  redefine func G*F -> strict covariant Functor of A, C;
end;

definition
  let A, B be transitive with_units non empty AltCatStr, C be with_units
  non empty AltCatStr, F be covariant Functor of A, B, G be contravariant
  Functor of B, C;
  redefine func G*F -> strict contravariant Functor of A, C;
end;

definition
  let A, B be transitive with_units non empty AltCatStr, C be with_units
  non empty AltCatStr, F be contravariant Functor of A, B, G be covariant
  Functor of B, C;
  redefine func G*F -> strict contravariant Functor of A, C;
end;

reserve A, B, C, D for transitive with_units non empty AltCatStr,
  F1, F2, F3 for covariant Functor of A, B,
  G1, G2, G3 for covariant Functor of B, C,
  H1, H2 for covariant Functor of C, D,
  p for transformation of F1, F2,
  p1 for transformation of F2, F3,
  q for transformation of G1, G2,
  q1 for transformation of G2, G3,
  r for transformation of H1, H2;

theorem :: FUNCTOR3:10
  F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1
  *F1 is_transformable_to G2*F2;

begin  :: The composition of functors with transformations

definition
  let A, B, C be transitive with_units non empty AltCatStr, F1, F2 be
  covariant Functor of A, B, t be transformation of F1, F2, G be covariant
  Functor of B, C such that
 F1 is_transformable_to F2;
  func G*t -> transformation of G*F1,G*F2 means
:: FUNCTOR3:def 1

  for o being Object of A holds it.o = G.(t!o);
end;

theorem :: FUNCTOR3:11
  for o being Object of A st F1 is_transformable_to F2 holds (G1*p
  )!o = G1.(p!o);

definition
  let A, B, C be transitive with_units non empty AltCatStr, G1, G2 be
covariant Functor of B, C, F be covariant Functor of A, B, s be transformation
  of G1, G2 such that
 G1 is_transformable_to G2;
  func s*F -> transformation of G1*F,G2*F means
:: FUNCTOR3:def 2

  for o being Object of A holds it.o = s!(F.o);
end;

theorem :: FUNCTOR3:12
  for o being Object of A st G1 is_transformable_to G2 holds (q*F1
  )!o = q!(F1.o);

theorem :: FUNCTOR3:13
  F1 is_transformable_to F2 & F2 is_transformable_to F3 implies G1
  *(p1`*`p) = (G1*p1)`*`(G1*p);

theorem :: FUNCTOR3:14
  G1 is_transformable_to G2 & G2 is_transformable_to G3 implies (
  q1`*`q)*F1 = (q1*F1)`*`(q*F1);

theorem :: FUNCTOR3:15
  H1 is_transformable_to H2 implies r*G1*F1 = r*(G1*F1);

theorem :: FUNCTOR3:16
  G1 is_transformable_to G2 implies H1*q*F1 = H1*(q*F1);

theorem :: FUNCTOR3:17
  F1 is_transformable_to F2 implies H1*G1*p = H1*(G1*p);

theorem :: FUNCTOR3:18
  (idt G1)*F1 = idt (G1*F1);

theorem :: FUNCTOR3:19
  G1 * idt F1 = idt (G1*F1);

theorem :: FUNCTOR3:20
  F1 is_transformable_to F2 implies (id B) * p = p;

theorem :: FUNCTOR3:21
  G1 is_transformable_to G2 implies q * id B = q;

begin  :: The composition of transformations

definition
  let A, B, C be transitive with_units non empty AltCatStr, F1, F2 be
  covariant Functor of A, B, G1, G2 be covariant Functor of B, C, t be
  transformation of F1, F2, s be transformation of G1, G2;
  func s (#) t -> transformation of G1*F1, G2*F2 equals
:: FUNCTOR3:def 3
  (s*F2) `*` (G1*t);
end;

theorem :: FUNCTOR3:22
  for q being natural_transformation of G1, G2 st F1
is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds q (#) p = (
  G2*p) `*` (q*F1);

theorem :: FUNCTOR3:23
  F1 is_transformable_to F2 implies (idt id B)(#)p = p;

theorem :: FUNCTOR3:24
  G1 is_transformable_to G2 implies q(#)(idt id B) = q;

theorem :: FUNCTOR3:25
  F1 is_transformable_to F2 implies G1*p = (idt G1) (#) p;

theorem :: FUNCTOR3:26
  G1 is_transformable_to G2 implies q*F1 = q (#) idt F1;

reserve A, B, C, D for category,
  F1, F2, F3 for covariant Functor of A, B,
  G1, G2, G3 for covariant Functor of B, C;

theorem :: FUNCTOR3:27
  for H1, H2 being covariant Functor of C, D for t being transformation
  of F1, F2, s being transformation of G1, G2 for u being transformation of H1,
  H2 st F1 is_transformable_to F2 & G1 is_transformable_to G2 & H1
  is_transformable_to H2 holds u(#)s(#)t = u(#)(s(#)t);

reserve t for natural_transformation of F1, F2,
  s for natural_transformation of G1, G2,
  s1 for natural_transformation of G2, G3;

theorem :: FUNCTOR3:28
  F1 is_naturally_transformable_to F2 implies G1*t is
  natural_transformation of G1*F1, G1*F2;

theorem :: FUNCTOR3:29
  G1 is_naturally_transformable_to G2 implies s*F1 is
  natural_transformation of G1*F1, G2*F1;

theorem :: FUNCTOR3:30
  F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to
  G2 implies G1*F1 is_naturally_transformable_to G2*F2 & s(#)t is
  natural_transformation of G1*F1, G2*F2;

theorem :: FUNCTOR3:31
  for t being transformation of F1, F2, t1 being transformation of F2,
F3 st F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3
  & G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3
  holds (s1`*`s)(#)(t1`*`t) = (s1(#)t1)`*`(s(#)t);

begin  :: Natural equivalences

theorem :: FUNCTOR3:32
  F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1
  & (for a being Object of A holds t!a is iso) implies F2
is_naturally_transformable_to F1 & ex f being natural_transformation of F2, F1
  st for a being Object of A holds f.a = (t!a)" & f!a is iso;

definition
  let A, B be category, F1, F2 be covariant Functor of A, B;
  pred F1, F2 are_naturally_equivalent means
:: FUNCTOR3:def 4

  F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 & ex t being
  natural_transformation of F1, F2 st for a being Object of A holds t!a is iso;
  reflexivity;
  symmetry;
end;

definition
  let A, B be category, F1, F2 be covariant Functor of A, B such that
 F1, F2 are_naturally_equivalent;
  mode natural_equivalence of F1, F2 -> natural_transformation of F1, F2 means
:: FUNCTOR3:def 5

    for a being Object of A holds it!a is iso;
end;

reserve e for natural_equivalence of F1, F2,
  e1 for natural_equivalence of F2, F3,
  f for natural_equivalence of G1, G2;

theorem :: FUNCTOR3:33
  F1, F2 are_naturally_equivalent & F2, F3
  are_naturally_equivalent implies F1, F3 are_naturally_equivalent;

theorem :: FUNCTOR3:34
  F1, F2 are_naturally_equivalent & F2, F3
  are_naturally_equivalent implies e1 `*` e is natural_equivalence of F1, F3;

theorem :: FUNCTOR3:35
  F1, F2 are_naturally_equivalent implies G1*F1, G1*F2
  are_naturally_equivalent & G1*e is natural_equivalence of G1*F1, G1*F2;

theorem :: FUNCTOR3:36
  G1, G2 are_naturally_equivalent implies G1*F1, G2*F1
  are_naturally_equivalent & f*F1 is natural_equivalence of G1*F1, G2*F1;

theorem :: FUNCTOR3:37
  F1, F2 are_naturally_equivalent & G1, G2 are_naturally_equivalent
implies G1*F1, G2*F2 are_naturally_equivalent & f (#) e is natural_equivalence
  of G1*F1, G2*F2;

definition
  let A, B be category, F1, F2 be covariant Functor of A, B, e be
  natural_equivalence of F1, F2 such that
 F1, F2 are_naturally_equivalent;
  func e" -> natural_equivalence of F2, F1 means
:: FUNCTOR3:def 6

  for a being Object of A holds it.a = (e!a)";
end;

theorem :: FUNCTOR3:38
  for o being Object of A st F1, F2 are_naturally_equivalent holds
  e"!o = (e!o)";

theorem :: FUNCTOR3:39
  F1, F2 are_naturally_equivalent implies e `*` e" = idt F2;

theorem :: FUNCTOR3:40
  F1, F2 are_naturally_equivalent implies e" `*` e = idt F1;

definition
  let A, B be category, F be covariant Functor of A, B;
  redefine func idt F -> natural_equivalence of F, F;
end;

theorem :: FUNCTOR3:41
  F1, F2 are_naturally_equivalent implies (e")" = e;

theorem :: FUNCTOR3:42
  for k being natural_equivalence of F1, F3 st k = e1 `*` e & F1, F2
are_naturally_equivalent & F2, F3 are_naturally_equivalent holds k" = e" `*` e1
  ";

theorem :: FUNCTOR3:43
  (idt F1)" = idt F1;