FUNCTOR3

:: The Composition of Functors and Transformations in Alternative
:: Categories
::  by Artur Korni{\l}owicz
::
:: Received January 21, 1998
:: Copyright (c) 1998-2026 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;
 definitions FUNCTOR0, FUNCTOR2, PBOOLE;
 equalities FUNCTOR0, BINOP_1;
 expansions FUNCTOR2, PBOOLE;
 theorems ALTCAT_1, ALTCAT_3, ALTCAT_4, FUNCTOR0, FUNCTOR2, ZFMISC_1, MSUALG_3,
      PBOOLE, FUNCT_1, FUNCT_2, RELAT_1, XBOOLE_0, PARTFUN1;
 schemes PBOOLE;

begin  :: Preliminaries

registration
  cluster transitive associative with_units strict for non empty AltCatStr;
  existence
  proof
    set A = the transitive associative with_units strict non empty AltCatStr;
    take A;
    thus thesis;
  end;
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;
  existence
  proof
    set o = the Object of B;
    take A --> idm o;
    thus thesis;
  end;
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;
  existence
  proof
    set o = the Object of B;
    take A --> idm o;
    thus thesis;
  end;
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;
  existence
  proof
    set o = the Object of B;
    set I = A --> idm o;
    reconsider I as Functor of A, B by FUNCTOR0:def 25;
    take I;
    thus I is strict feasible;
    thus I is covariant;
    thus thesis;
  end;
end;

theorem
  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
proof
  let C be category, o1, o2, o3, o4 be Object of C, a be Morphism of o1, o2, b
  be Morphism of o2, o3, c be Morphism of o1, o4, d be Morphism of o4, o3 such
  that
A1: b*a = d*c and
A2: a*(a") = idm o2 and
A3: d"*d = idm o4 and
A4: <^o1,o2^> <> {} and
A5: <^o2,o1^> <> {} and
A6: <^o2,o3^> <> {} and
A7: <^o3,o4^> <> {} and
A8: <^o4,o3^> <> {};
A9: <^o2,o4^> <> {} by A6,A7,ALTCAT_1:def 2;
  <^o1,o3^> <> {} by A4,A6,ALTCAT_1:def 2;
  then
A10: <^o1,o4^> <> {} by A7,ALTCAT_1:def 2;
  b = b*idm o2 by A6,ALTCAT_1:def 17
    .= b*a*(a") by A2,A4,A5,A6,ALTCAT_1:21;
  hence d"*b = d"*(d*(c*(a"))) by A1,A5,A8,A10,ALTCAT_1:21
    .= (d"*d)*(c*(a")) by A7,A8,A9,ALTCAT_1:21
    .= c*(a") by A3,A9,ALTCAT_1:20;
end;

theorem
  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)
proof
  let A be non empty transitive AltCatStr, B, C be with_units non empty
AltCatStr, F be feasible Covariant FunctorStr over A, B, G be FunctorStr over
  B, C, o, o1 be Object of A;
  dom(the MorphMap of G) = [:the carrier of B,the carrier of B:] & rng(the
  ObjectMap of F) c= [:the carrier of B,the carrier of B:] by PARTFUN1:def 2;
  then
  dom((the MorphMap of G)*the ObjectMap of F) = dom(the ObjectMap of F) by
RELAT_1:27
    .= [:the carrier of A,the carrier of A:] by FUNCT_2:def 1;
  then
A1: [o,o1] in dom((the MorphMap of G)*the ObjectMap of F) by ZFMISC_1:87;
  then
A2: ((the MorphMap of G)*the ObjectMap of F).[o,o1] = (the MorphMap of G).((
  the ObjectMap of F).(o,o1)) by FUNCT_1:12
    .= Morph-Map(G,F.o,F.o1) by FUNCTOR0:22;
  dom(the MorphMap of F) = [:the carrier of A,the carrier of A:] by
PARTFUN1:def 2;
  then [o,o1] in dom(the MorphMap of F) by ZFMISC_1:87;
  then [o,o1] in dom((the MorphMap of G)*the ObjectMap of F) /\ dom(the
  MorphMap of F) by A1,XBOOLE_0:def 4;
  then
A3: [o,o1] in dom(((the MorphMap of G)*the ObjectMap of F)**the MorphMap of
  F) by PBOOLE:def 19;
  thus Morph-Map(G*F,o,o1) = (((the MorphMap of G)*the ObjectMap of F)**the
  MorphMap of F).(o,o1) by FUNCTOR0:def 36
    .= Morph-Map(G,F.o,F.o1)*Morph-Map(F,o,o1) by A3,A2,PBOOLE:def 19;
end;

theorem
  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)
proof
  let A be non empty transitive AltCatStr, B, C be with_units non empty
  AltCatStr, F be feasible Contravariant FunctorStr over A, B, G be FunctorStr
  over B, C, o, o1 be Object of A;
  dom(the MorphMap of G) = [:the carrier of B,the carrier of B:] & rng(the
  ObjectMap of F) c= [:the carrier of B,the carrier of B:] by PARTFUN1:def 2;
  then
  dom((the MorphMap of G)*the ObjectMap of F) = dom(the ObjectMap of F) by
RELAT_1:27
    .= [:the carrier of A,the carrier of A:] by FUNCT_2:def 1;
  then
A1: [o,o1] in dom((the MorphMap of G)*the ObjectMap of F) by ZFMISC_1:87;
  then
A2: ((the MorphMap of G)*the ObjectMap of F).[o,o1] = (the MorphMap of G).((
  the ObjectMap of F).(o,o1)) by FUNCT_1:12
    .= Morph-Map(G,F.o1,F.o) by FUNCTOR0:23;
  dom(the MorphMap of F) = [:the carrier of A,the carrier of A:] by
PARTFUN1:def 2;
  then [o,o1] in dom(the MorphMap of F) by ZFMISC_1:87;
  then [o,o1] in dom((the MorphMap of G)*the ObjectMap of F) /\ dom(the
  MorphMap of F) by A1,XBOOLE_0:def 4;
  then
A3: [o,o1] in dom(((the MorphMap of G)*the ObjectMap of F)**the MorphMap of
  F) by PBOOLE:def 19;
  thus Morph-Map(G*F,o,o1) = (((the MorphMap of G)*the ObjectMap of F)**the
  MorphMap of F).(o,o1) by FUNCTOR0:def 36
    .= Morph-Map(G,F.o1,F.o)*Morph-Map(F,o,o1) by A3,A2,PBOOLE:def 19;
end;

Lm1: for I1 being set, I2 being non empty set, f being Function of I1,I2 for A
being ManySortedSet of I1, B being ManySortedSet of I2 for M being
ManySortedFunction of A,B*f holds ((id B)*f)**M = M
proof
  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;
  let M be ManySortedFunction of A,B*f;
A1: now
    let i be object;
    assume
A2: i in I1;
    hence
A3: (B*f).i = B.(f.i) by FUNCT_2:15;
    ((id B)*f).i = (id B).(f.i) & f.i in I2 by A2,FUNCT_2:5,15;
    hence ((id B)*f).i = id ((B*f).i) by A3,MSUALG_3:def 1;
  end;
  now
A4: (id B)*f is ManySortedFunction of B*f, B*f
    proof
      let i be object;
      assume i in I1;
      then ((id B)*f).i = id ((B*f).i) by A1;
      hence thesis;
    end;
    let i be object;
    assume
A5: i in I1;
    then
A6: M.i is Function of A.i, (B*f).i by PBOOLE:def 15;
    ((id B)*f).i = (id B).(f.i) & f.i in I2 by A5,FUNCT_2:5,15;
    then
A7: ((id B)*f).i = id (B.(f.i)) by MSUALG_3:def 1;
    (B*f).i = B.(f.i) by A1,A5;
    hence (((id B)*f)**M).i = (id ((B*f).i))*(M.i) by A5,A4,A7,MSUALG_3:2
      .= M.i by A6,FUNCT_2:17;
  end;
  hence thesis;
end;

theorem
  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
proof
  let A be non empty transitive AltCatStr, B be with_units non empty
  AltCatStr, F be feasible FunctorStr over A, B;
A1: the ObjectMap of ((id B) * F) = (the ObjectMap of (id B))*the ObjectMap
  of F by FUNCTOR0:def 36
    .= (id [:the carrier of B, the carrier of B:])*the ObjectMap of F by
FUNCTOR0:def 29
    .= the ObjectMap of F by FUNCT_2:17;
A2: the MorphMap of F is ManySortedFunction of the Arrows of A, (the Arrows
  of B)*the ObjectMap of F by FUNCTOR0:def 4;
  the MorphMap of ((id B) * F) = ((the MorphMap of id B)*the ObjectMap of
  F)**the MorphMap of F by FUNCTOR0:def 36
    .= ((id the Arrows of B)*the ObjectMap of F)**the MorphMap of F by
FUNCTOR0:def 29
    .= the MorphMap of F by A2,Lm1;
  hence thesis by A1;
end;

theorem
  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
proof
  let A be with_units transitive non empty AltCatStr, B be with_units non
  empty AltCatStr, F be feasible FunctorStr over A, B;
A1: the ObjectMap of (F*(id A)) = (the ObjectMap of F)*the ObjectMap of id A
  by FUNCTOR0:def 36
    .= (the ObjectMap of F)*id [:the carrier of A, the carrier of A:] by
FUNCTOR0:def 29
    .= the ObjectMap of F by FUNCT_2:17;
A2: the MorphMap of F is ManySortedFunction of the Arrows of A, (the Arrows
  of B)*the ObjectMap of F by FUNCTOR0:def 4;
  the MorphMap of (F*id A) = ((the MorphMap of F)*the ObjectMap of id A)**
  the MorphMap of id A by FUNCTOR0:def 36
    .= ((the MorphMap of F)*id [:the carrier of A, the carrier of A:]) **the
  MorphMap of id A by FUNCTOR0:def 29
    .= (the MorphMap of F)**the MorphMap of id A by FUNCTOR0:2
    .= (the MorphMap of F)**id the Arrows of A by FUNCTOR0:def 29
    .= the MorphMap of F by A2,MSUALG_3:3;
  hence thesis by A1;
end;

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 Th6:
  <^o1,o2^> <> {} implies (G*F).m = G.(F.m)
proof
  set I = the carrier of A;
  reconsider s = (the MorphMap of F).(o1,o2) as Function;
  reconsider r = (((the MorphMap of G)*the ObjectMap of F)** the MorphMap of F
  ).(o1,o2) as Function;
  reconsider t = ((the MorphMap of G)*the ObjectMap of F).(o1,o2) as Function;
A1: dom (((the MorphMap of G)*the ObjectMap of F)**the MorphMap of F) = (dom
((the MorphMap of G)*the ObjectMap of F)) /\ (dom(the MorphMap of F)) by
PBOOLE:def 19
    .= [:I,I:] /\ (dom(the MorphMap of F)) by PARTFUN1:def 2
    .= [:I,I:] /\ [:I,I:] by PARTFUN1:def 2
    .= [:I,I:];
A2: dom the ObjectMap of F = [:I,I:] by FUNCT_2:def 1;
A3: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
  assume
A4: <^o1,o2^> <> {};
  then
A5: <^F.o1,F.o2^> <> {} by FUNCTOR0:def 18;
  then
A6: dom Morph-Map(F,o1,o2) = <^o1,o2^> by FUNCT_2:def 1;
A7: <^G.(F.o1),G.(F.o2)^> <> {} by A5,FUNCTOR0:def 18;
  (G*F).o1 = G.(F.o1) & (G*F).o2 = G.(F.o2) by FUNCTOR0:33;
  hence (G*F).m = Morph-Map(G*F,o1,o2).m by A4,A7,FUNCTOR0:def 15
    .= r.m by FUNCTOR0:def 36
    .= (t * s).m by A1,A3,PBOOLE:def 19
    .= t.(Morph-Map(F,o1,o2).m) by A4,A6,FUNCT_1:13
    .= t.(F.m) by A4,A5,FUNCTOR0:def 15
    .= ((the MorphMap of G).((the ObjectMap of F).(o1,o2))).(F.m) by A2,A3,
FUNCT_1:13
    .= Morph-Map(G,F.o1,F.o2).(F.m) by FUNCTOR0:22
    .= G.(F.m) by A5,A7,FUNCTOR0:def 15;
end;

theorem Th7:
  <^o1,o2^> <> {} implies (N*M).m = N.(M.m)
proof
  set I = the carrier of A;
  reconsider s = (the MorphMap of M).(o1,o2) as Function;
  reconsider r = (((the MorphMap of N)*the ObjectMap of M)** the MorphMap of M
  ).(o1,o2) as Function;
  reconsider t = ((the MorphMap of N)*the ObjectMap of M).(o1,o2) as Function;
A1: dom (((the MorphMap of N)*the ObjectMap of M)**the MorphMap of M) = (dom
((the MorphMap of N)*the ObjectMap of M)) /\ (dom(the MorphMap of M)) by
PBOOLE:def 19
    .= [:I,I:] /\ (dom(the MorphMap of M)) by PARTFUN1:def 2
    .= [:I,I:] /\ [:I,I:] by PARTFUN1:def 2
    .= [:I,I:];
A2: dom the ObjectMap of M = [:I,I:] by FUNCT_2:def 1;
A3: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
  assume
A4: <^o1,o2^> <> {};
  then
A5: <^M.o2,M.o1^> <> {} by FUNCTOR0:def 19;
  then
A6: dom Morph-Map(M,o1,o2) = <^o1,o2^> by FUNCT_2:def 1;
A7: <^N.(M.o1),N.(M.o2)^> <> {} by A5,FUNCTOR0:def 19;
  (N*M).o1 = N.(M.o1) & (N*M).o2 = N.(M.o2) by FUNCTOR0:33;
  hence (N*M).m = Morph-Map(N*M,o1,o2).m by A4,A7,FUNCTOR0:def 15
    .= r.m by FUNCTOR0:def 36
    .= (t * s).m by A1,A3,PBOOLE:def 19
    .= t.(Morph-Map(M,o1,o2).m) by A4,A6,FUNCT_1:13
    .= t.(M.m) by A4,A5,FUNCTOR0:def 16
    .= ((the MorphMap of N).((the ObjectMap of M).(o1,o2))).(M.m) by A2,A3,
FUNCT_1:13
    .= Morph-Map(N,M.o2,M.o1).(M.m) by FUNCTOR0:23
    .= N.(M.m) by A5,A7,FUNCTOR0:def 16;
end;

theorem Th8:
  <^o1,o2^> <> {} implies (N*F).m = N.(F.m)
proof
  set I = the carrier of A;
  reconsider s = (the MorphMap of F).(o1,o2) as Function;
  reconsider r = (((the MorphMap of N)*the ObjectMap of F)** the MorphMap of F
  ).(o1,o2) as Function;
  reconsider t = ((the MorphMap of N)*the ObjectMap of F).(o1,o2) as Function;
A1: dom (((the MorphMap of N)*the ObjectMap of F)**the MorphMap of F) = (dom
((the MorphMap of N)*the ObjectMap of F)) /\ (dom(the MorphMap of F)) by
PBOOLE:def 19
    .= [:I,I:] /\ (dom(the MorphMap of F)) by PARTFUN1:def 2
    .= [:I,I:] /\ [:I,I:] by PARTFUN1:def 2
    .= [:I,I:];
A2: dom the ObjectMap of F = [:I,I:] by FUNCT_2:def 1;
A3: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
  assume
A4: <^o1,o2^> <> {};
  then
A5: <^F.o1,F.o2^> <> {} by FUNCTOR0:def 18;
  then
A6: dom Morph-Map(F,o1,o2) = <^o1,o2^> by FUNCT_2:def 1;
A7: <^N.(F.o2),N.(F.o1)^> <> {} by A5,FUNCTOR0:def 19;
  (N*F).o1 = N.(F.o1) & (N*F).o2 = N.(F.o2) by FUNCTOR0:33;
  hence (N*F).m = Morph-Map(N*F,o1,o2).m by A4,A7,FUNCTOR0:def 16
    .= r.m by FUNCTOR0:def 36
    .= (t * s).m by A1,A3,PBOOLE:def 19
    .= t.(Morph-Map(F,o1,o2).m) by A4,A6,FUNCT_1:13
    .= t.(F.m) by A4,A5,FUNCTOR0:def 15
    .= ((the MorphMap of N).((the ObjectMap of F).(o1,o2))).(F.m) by A2,A3,
FUNCT_1:13
    .= Morph-Map(N,F.o1,F.o2).(F.m) by FUNCTOR0:22
    .= N.(F.m) by A5,A7,FUNCTOR0:def 16;
end;

theorem Th9:
  <^o1,o2^> <> {} implies (G*M).m = G.(M.m)
proof
  set I = the carrier of A;
  reconsider s = (the MorphMap of M).(o1,o2) as Function;
  reconsider r = (((the MorphMap of G)*the ObjectMap of M)** the MorphMap of M
  ).(o1,o2) as Function;
  reconsider t = ((the MorphMap of G)*the ObjectMap of M).(o1,o2) as Function;
A1: dom (((the MorphMap of G)*the ObjectMap of M)**the MorphMap of M) = (dom
((the MorphMap of G)*the ObjectMap of M)) /\ (dom(the MorphMap of M)) by
PBOOLE:def 19
    .= [:I,I:] /\ (dom(the MorphMap of M)) by PARTFUN1:def 2
    .= [:I,I:] /\ [:I,I:] by PARTFUN1:def 2
    .= [:I,I:];
A2: dom the ObjectMap of M = [:I,I:] by FUNCT_2:def 1;
A3: [o1,o2] in [:I,I:] by ZFMISC_1:def 2;
  assume
A4: <^o1,o2^> <> {};
  then
A5: <^M.o2,M.o1^> <> {} by FUNCTOR0:def 19;
  then
A6: dom Morph-Map(M,o1,o2) = <^o1,o2^> by FUNCT_2:def 1;
A7: <^G.(M.o2),G.(M.o1)^> <> {} by A5,FUNCTOR0:def 18;
  (G*M).o1 = G.(M.o1) & (G*M).o2 = G.(M.o2) by FUNCTOR0:33;
  hence (G*M).m = Morph-Map(G*M,o1,o2).m by A4,A7,FUNCTOR0:def 16
    .= r.m by FUNCTOR0:def 36
    .= (t * s).m by A1,A3,PBOOLE:def 19
    .= t.(Morph-Map(M,o1,o2).m) by A4,A6,FUNCT_1:13
    .= t.(M.m) by A4,A5,FUNCTOR0:def 16
    .= ((the MorphMap of G).((the ObjectMap of M).(o1,o2))).(M.m) by A2,A3,
FUNCT_1:13
    .= Morph-Map(G,M.o2,M.o1).(M.m) by FUNCTOR0:23
    .= G.(M.m) by A5,A7,FUNCTOR0:def 15;
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 Covariant
  comp-preserving FunctorStr over B, C;
  cluster G*F -> comp-preserving;
  coherence
  proof
    let o1, o2, o3 be Object of A such that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
A3: <^F.o1,F.o2^> <> {} & <^F.o2,F.o3^> <> {} by A1,A2,FUNCTOR0:def 18;
    let f be Morphism of o1, o2, g be Morphism of o2, o3;
A4: (G*F).o1 = G.(F.o1) & (G*F).o3 = G.(F.o3) by FUNCTOR0:33;
A5: (G*F).o2 = G.(F.o2) by FUNCTOR0:33;
    then reconsider GFg = (G*F).g as Morphism of G.(F.o2), G.(F.o3) by
FUNCTOR0:33;
    <^o1,o3^> <> {} by A1,A2,ALTCAT_1:def 2;
    hence (G*F).(g*f) = G.(F.(g*f)) by Th6
      .= G.((F.g)*(F.f)) by A1,A2,FUNCTOR0:def 23
      .= (G.(F.g))*(G.(F.f)) by A3,FUNCTOR0:def 23
      .= GFg*(G.(F.f)) by A2,Th6
      .= ((G*F).g)*((G*F).f) by A1,A5,A4,Th6;
  end;
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;
  coherence
  proof
    let o1, o2, o3 be Object of A such that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
A3: <^F.o2,F.o1^> <> {} & <^F.o3,F.o2^> <> {} by A1,A2,FUNCTOR0:def 19;
    let f be Morphism of o1, o2, g be Morphism of o2, o3;
A4: (G*F).o1 = G.(F.o1) & (G*F).o3 = G.(F.o3) by FUNCTOR0:33;
A5: (G*F).o2 = G.(F.o2) by FUNCTOR0:33;
    then reconsider GFg = (G*F).g as Morphism of G.(F.o2), G.(F.o3) by
FUNCTOR0:33;
    <^o1,o3^> <> {} by A1,A2,ALTCAT_1:def 2;
    hence (G*F).(g*f) = G.(F.(g*f)) by Th7
      .= G.((F.f)*(F.g)) by A1,A2,FUNCTOR0:def 24
      .= (G.(F.g))*(G.(F.f)) by A3,FUNCTOR0:def 24
      .= GFg*(G.(F.f)) by A2,Th7
      .= ((G*F).g)*((G*F).f) by A1,A5,A4,Th7;
  end;
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;
  coherence
  proof
    let o1, o2, o3 be Object of A such that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
A3: <^F.o1,F.o2^> <> {} & <^F.o2,F.o3^> <> {} by A1,A2,FUNCTOR0:def 18;
    let f be Morphism of o1, o2, g be Morphism of o2, o3;
A4: (G*F).o2 = G.(F.o2) & (G*F).o3 = G.(F.o3) by FUNCTOR0:33;
A5: (G*F).o1 = G.(F.o1) by FUNCTOR0:33;
    then reconsider GFf = (G*F).f as Morphism of G.(F.o2), G.(F.o1) by
FUNCTOR0:33;
    <^o1,o3^> <> {} by A1,A2,ALTCAT_1:def 2;
    hence (G*F).(g*f) = G.(F.(g*f)) by Th8
      .= G.((F.g)*(F.f)) by A1,A2,FUNCTOR0:def 23
      .= (G.(F.f))*(G.(F.g)) by A3,FUNCTOR0:def 24
      .= GFf*(G.(F.g)) by A1,Th8
      .= ((G*F).f)*((G*F).g) by A2,A5,A4,Th8;
  end;
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;
  coherence
  proof
    let o1, o2, o3 be Object of A such that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {};
A3: <^F.o2,F.o1^> <> {} & <^F.o3,F.o2^> <> {} by A1,A2,FUNCTOR0:def 19;
    let f be Morphism of o1, o2, g be Morphism of o2, o3;
A4: (G*F).o2 = G.(F.o2) & (G*F).o3 = G.(F.o3) by FUNCTOR0:33;
A5: (G*F).o1 = G.(F.o1) by FUNCTOR0:33;
    then reconsider GFf = (G*F).f as Morphism of G.(F.o2), G.(F.o1) by
FUNCTOR0:33;
    <^o1,o3^> <> {} by A1,A2,ALTCAT_1:def 2;
    hence (G*F).(g*f) = G.(F.(g*f)) by Th9
      .= G.((F.f)*(F.g)) by A1,A2,FUNCTOR0:def 24
      .= (G.(F.f))*(G.(F.g)) by A3,FUNCTOR0:def 23
      .= GFf*(G.(F.g)) by A1,Th9
      .= ((G*F).f)*((G*F).g) by A2,A5,A4,Th9;
  end;
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;  :: redefines * (FUNCTOR0, definition)
  coherence by FUNCTOR0:def 25;
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;  :: redefines * (FUNCTOR0, definition)
  coherence by FUNCTOR0:def 25;
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;  :: redefines * (FUNCTOR0, definition)
  coherence by FUNCTOR0:def 25;
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;  :: redefines * (FUNCTOR0, definition)
  coherence by FUNCTOR0:def 25;
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 Th10:
  F1 is_transformable_to F2 & G1 is_transformable_to G2 implies G1
  *F1 is_transformable_to G2*F2
proof
  assume
A1: for a being Object of A holds <^F1.a,F2.a^> <> {};
  assume
A2: for a being Object of B holds <^G1.a,G2.a^> <> {};
  let a be Object of A;
  <^F1.a,F2.a^> <> {} by A1;
  then
A3: <^G1.(F1.a),G1.(F2.a)^> <> {} by FUNCTOR0:def 18;
A4: (G1*F1).a = G1.(F1.a) & (G2*F2).a = G2.(F2.a) by FUNCTOR0:33;
  <^G1.(F2.a),G2.(F2.a)^> <> {} by A2;
  hence thesis by A4,A3,ALTCAT_1:def 2;
end;

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
A1: F1 is_transformable_to F2;
  func G*t -> transformation of G*F1,G*F2 means
  :Def1:
  for o being Object of A holds it.o = G.(t!o);
  existence
  proof
    defpred P[object,object] means
    ex o being Object of A st $1 = o & $2 = G.(t!o);
    set I = the carrier of A;
A2: for i being object st i in I ex j being object st P[i,j]
    proof
      let i be object;
      assume i in I;
      then reconsider o = i as Object of A;
      take G.(t!o);
      thus thesis;
    end;
    consider IT being ManySortedSet of I such that
A3: for o being object st o in I holds P[o,IT.o] from PBOOLE:sch 3(A2);
    IT is transformation of G*F1,G*F2
    proof
      thus G*F1 is_transformable_to G*F2 by A1,Th10;
      let o be Object of A;
      ( P[o,IT.o])& G.(F1.o) = (G*F1).o by A3,FUNCTOR0:33;
      hence thesis by FUNCTOR0:33;
    end;
    then reconsider IT as transformation of G*F1,G*F2;
    take IT;
    let o be Object of A;
    P[o,IT.o] by A3;
    hence thesis;
  end;
  uniqueness
  proof
    let X, Y be transformation of G*F1,G*F2 such that
A4: for o being Object of A holds X.o = G.(t!o) and
A5: for o being Object of A holds Y.o = G.(t!o);
A6: G*F1 is_transformable_to G*F2 by A1,Th10;
    now
      let o be Object of A;
      thus X!o = X.o by A6,FUNCTOR2:def 4
        .= G.(t!o) by A4
        .= Y.o by A5
        .= Y!o by A6,FUNCTOR2:def 4;
    end;
    hence thesis by A1,Th10,FUNCTOR2:3;
  end;
end;

theorem Th11:
  for o being Object of A st F1 is_transformable_to F2 holds (G1*p
  )!o = G1.(p!o)
proof
  let o be Object of A;
  assume
A1: F1 is_transformable_to F2;
  then G1*F1 is_transformable_to G1*F2 by Th10;
  hence (G1*p)!o = (G1*p).o by FUNCTOR2:def 4
    .= G1.(p!o) by A1,Def1;
end;

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
A1: G1 is_transformable_to G2;
  func s*F -> transformation of G1*F,G2*F means
  :Def2:
  for o being Object of A holds it.o = s!(F.o);
  existence
  proof
    defpred P[object,object] means
ex o being Object of A st $1 = o & $2 = s!(F.o);
    set I = the carrier of A;
A2: for i being object st i in I ex j being object st P[i,j]
    proof
      let i be object;
      assume i in I;
      then reconsider o = i as Object of A;
      take s!(F.o);
      thus thesis;
    end;
    consider IT being ManySortedSet of I such that
A3: for o being object st o in I holds P[o,IT.o] from PBOOLE:sch 3(A2);
    IT is transformation of G1*F,G2*F
    proof
      thus G1*F is_transformable_to G2*F by A1,Th10;
      let o be Object of A;
      ( P[o,IT.o])& G1.(F.o) = (G1*F).o by A3,FUNCTOR0:33;
      hence thesis by FUNCTOR0:33;
    end;
    then reconsider IT as transformation of G1*F,G2*F;
    take IT;
    let o be Object of A;
    P[o,IT.o] by A3;
    hence thesis;
  end;
  uniqueness
  proof
    let X, Y be transformation of G1*F,G2*F such that
A4: for o being Object of A holds X.o = s!(F.o) and
A5: for o being Object of A holds Y.o = s!(F.o);
A6: G1*F is_transformable_to G2*F by A1,Th10;
    now
      let o be Object of A;
      thus X!o = X.o by A6,FUNCTOR2:def 4
        .= s!(F.o) by A4
        .= Y.o by A5
        .= Y!o by A6,FUNCTOR2:def 4;
    end;
    hence thesis by A1,Th10,FUNCTOR2:3;
  end;
end;

theorem Th12:
  for o being Object of A st G1 is_transformable_to G2 holds (q*F1
  )!o = q!(F1.o)
proof
  let o be Object of A;
  assume
A1: G1 is_transformable_to G2;
  then G1*F1 is_transformable_to G2*F1 by Th10;
  hence (q*F1)!o = (q*F1).o by FUNCTOR2:def 4
    .= q!(F1.o) by A1,Def2;
end;

theorem Th13:
  F1 is_transformable_to F2 & F2 is_transformable_to F3 implies G1
  *(p1`*`p) = (G1*p1)`*`(G1*p)
proof
  assume that
A1: F1 is_transformable_to F2 and
A2: F2 is_transformable_to F3;
A3: G1*F1 is_transformable_to G1*F2 & G1*F2 is_transformable_to G1*F3 by A1,A2
,Th10;
A4: now
    let a be Object of A;
A5: G1.(F2.a) = (G1*F2).a & G1.(F3.a) = (G1*F3).a by FUNCTOR0:33;
A6: G1.(F1.a) = (G1*F1).a by FUNCTOR0:33;
    then reconsider G1ta = (G1*p)!a as Morphism of G1.(F1.a), G1.(F2.a) by
FUNCTOR0:33;
A7: <^F1.a,F2.a^> <> {} & <^F2.a,F3.a^> <> {} by A1,A2;
    thus (G1*(p1`*`p))!a = G1.((p1`*`p)!a) by A1,A2,Th11,FUNCTOR2:2
      .= G1.((p1!a)*(p!a)) by A1,A2,FUNCTOR2:def 5
      .= G1.(p1!a)*G1.(p!a) by A7,FUNCTOR0:def 23
      .= G1.(p1!a)*G1ta by A1,Th11
      .= ((G1*p1)!a)*((G1*p)!a) by A2,A6,A5,Th11
      .= ((G1*p1)`*`(G1*p))!a by A3,FUNCTOR2:def 5;
  end;
  F1 is_transformable_to F3 by A1,A2,FUNCTOR2:2;
  hence thesis by A4,Th10,FUNCTOR2:3;
end;

theorem Th14:
  G1 is_transformable_to G2 & G2 is_transformable_to G3 implies (
  q1`*`q)*F1 = (q1*F1)`*`(q*F1)
proof
  assume that
A1: G1 is_transformable_to G2 and
A2: G2 is_transformable_to G3;
A3: G1*F1 is_transformable_to G2*F1 & G2*F1 is_transformable_to G3*F1 by A1,A2
,Th10;
A4: now
    let a be Object of A;
A5: G1.(F1.a) = (G1*F1).a & G3.(F1.a) = (G3*F1).a by FUNCTOR0:33;
A6: G2.(F1.a) = (G2*F1).a by FUNCTOR0:33;
    then reconsider s1F1a = (q1*F1)!a as Morphism of G2.(F1.a), G3.(F1.a) by
FUNCTOR0:33;
    thus ((q1`*`q)*F1)!a = (q1`*`q)!(F1.a) by A1,A2,Th12,FUNCTOR2:2
      .= (q1!(F1.a))*(q!(F1.a)) by A1,A2,FUNCTOR2:def 5
      .= s1F1a*(q!(F1.a)) by A2,Th12
      .= ((q1*F1)!a)*((q*F1)!a) by A1,A6,A5,Th12
      .= ((q1*F1)`*`(q*F1))!a by A3,FUNCTOR2:def 5;
  end;
  G1 is_transformable_to G3 by A1,A2,FUNCTOR2:2;
  hence thesis by A4,Th10,FUNCTOR2:3;
end;

theorem Th15:
  H1 is_transformable_to H2 implies r*G1*F1 = r*(G1*F1)
proof
A1: H2*G1*F1 = H2*(G1*F1) by FUNCTOR0:32;
  then reconsider m = r*(G1*F1) as transformation of H1*G1*F1, H2*G1*F1 by
FUNCTOR0:32;
  assume
A2: H1 is_transformable_to H2;
A3: now
    let a be Object of A;
    thus (r*G1*F1)!a = (r*G1)!(F1.a) by A2,Th10,Th12
      .= r!(G1.(F1.a)) by A2,Th12
      .= r!((G1*F1).a) by FUNCTOR0:33
      .= (r*(G1*F1))!a by A2,Th12
      .= m!a by A1,FUNCTOR0:32;
  end;
  H1*G1 is_transformable_to H2*G1 by A2,Th10;
  hence thesis by A3,Th10,FUNCTOR2:3;
end;

theorem Th16:
  G1 is_transformable_to G2 implies H1*q*F1 = H1*(q*F1)
proof
A1: H1*G2*F1 = H1*(G2*F1) by FUNCTOR0:32;
  then reconsider m = H1*(q*F1) as transformation of H1*G1*F1, H1*G2*F1 by
FUNCTOR0:32;
  assume
A2: G1 is_transformable_to G2;
A3: now
    let a be Object of A;
A4: (G1*F1).a = G1.(F1.a) & (G2*F1).a = G2.(F1.a) by FUNCTOR0:33;
    thus (H1*q*F1)!a = (H1*q)!(F1.a) by A2,Th10,Th12
      .= H1.(q!(F1.a)) by A2,Th11
      .= H1.((q*F1)!a) by A2,A4,Th12
      .= (H1*(q*F1))!a by A2,Th10,Th11
      .= m!a by A1,FUNCTOR0:32;
  end;
  H1*G1 is_transformable_to H1*G2 by A2,Th10;
  hence thesis by A3,Th10,FUNCTOR2:3;
end;

theorem Th17:
  F1 is_transformable_to F2 implies H1*G1*p = H1*(G1*p)
proof
A1: H1*G1*F2 = H1*(G1*F2) by FUNCTOR0:32;
  then reconsider m = H1*(G1*p) as transformation of H1*G1*F1, H1*G1*F2 by
FUNCTOR0:32;
  assume
A2: F1 is_transformable_to F2;
  now
    let a be Object of A;
A3: (G1*F1).a = G1.(F1.a) & (G1*F2).a = G1.(F2.a) by FUNCTOR0:33;
A4: <^F1.a,F2.a^> <> {} by A2;
    thus (H1*G1*p)!a = (H1*G1).(p!a) by A2,Th11
      .= H1.(G1.(p!a)) by A4,Th6
      .= H1.((G1*p)!a) by A2,A3,Th11
      .= (H1*(G1*p))!a by A2,Th10,Th11
      .= m!a by A1,FUNCTOR0:32;
  end;
  hence thesis by A2,Th10,FUNCTOR2:3;
end;

theorem Th18:
  (idt G1)*F1 = idt (G1*F1)
proof
  now
    let a be Object of A;
    thus ((idt G1)*F1)!a = (idt G1)!(F1.a) by Th12
      .= idm(G1.(F1.a)) by FUNCTOR2:4
      .= idm((G1*F1).a) by FUNCTOR0:33
      .= (idt (G1*F1))!a by FUNCTOR2:4;
  end;
  hence thesis by FUNCTOR2:3;
end;

theorem Th19:
  G1 * idt F1 = idt (G1*F1)
proof
  now
    let a be Object of A;
    thus (G1*(idt F1))!a = G1.((idt F1)!a) by Th11
      .= G1.(idm (F1.a)) by FUNCTOR2:4
      .= idm (G1.(F1.a)) by FUNCTOR2:1
      .= idm ((G1*F1).a) by FUNCTOR0:33
      .= (idt (G1*F1))!a by FUNCTOR2:4;
  end;
  hence thesis by FUNCTOR2:3;
end;

theorem Th20:
  F1 is_transformable_to F2 implies (id B) * p = p
proof
  assume
A1: F1 is_transformable_to F2;
  now
    let i be object;
    assume i in the carrier of A;
    then reconsider a = i as Object of A;
A2: <^F1.a,F2.a^> <> {} by A1;
    thus ((id B) * p).i = (id B).(p!a) by A1,Def1
      .= p!a by A2,FUNCTOR0:31
      .= p.i by A1,FUNCTOR2:def 4;
  end;
  hence thesis;
end;

theorem Th21:
  G1 is_transformable_to G2 implies q * id B = q
proof
  assume
A1: G1 is_transformable_to G2;
  now
    let i be object;
    assume i in the carrier of B;
    then reconsider a = i as Object of B;
    thus (q * id B).i = q!((id B).a) by A1,Def2
      .= q!a by FUNCTOR0:29
      .= q.i by A1,FUNCTOR2:def 4;
  end;
  hence thesis;
end;

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
  (s*F2) `*` (G1*t);
  coherence;
end;

theorem Th22:
  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)
proof
  let q be natural_transformation of G1, G2;
  assume that
A1: F1 is_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2;
A3: G1*F1 is_transformable_to G1*F2 by A1,Th10;
A4: G2*F1 is_transformable_to G2*F2 by A1,Th10;
A5: G1 is_transformable_to G2 by A2;
  then
A6: G1*F1 is_transformable_to G2*F1 by Th10;
A7: G1*F2 is_transformable_to G2*F2 by A5,Th10;
  now
    let a be Object of A;
A8: G1.(F1.a) = (G1*F1).a by FUNCTOR0:33;
A9: G2.(F2.a) = (G2*F2).a by FUNCTOR0:33;
    then reconsider sF2a = q!F2.a as Morphism of (G1*F2).a, (G2*F2).a by
FUNCTOR0:33;
    reconsider G2ta = G2*p!a as Morphism of G2.(F1.a), G2.(F2.a) by A9,
FUNCTOR0:33;
A10: G1.(F2.a) = (G1*F2).a by FUNCTOR0:33;
A11: <^F1.a,F2.a^> <> {} by A1;
A12: G2.(F1.a) = (G2*F1).a by FUNCTOR0:33;
    thus ((q*F2) `*` (G1*p))!a = ((q*F2)!a) * ((G1*p)!a) by A7,A3,
FUNCTOR2:def 5
      .= sF2a * ((G1*p)!a) by A5,Th12
      .= (q!F2.a) * G1.(p!a) by A1,A8,A10,A9,Th11
      .= G2.(p!a) * (q!F1.a) by A2,A11,FUNCTOR2:def 7
      .= G2ta * (q!F1.a) by A1,Th11
      .= G2*p!a * (q*F1!a) by A5,A8,A12,A9,Th12
      .= ((G2*p) `*` (q*F1))!a by A6,A4,FUNCTOR2:def 5;
  end;
  hence thesis by A1,A5,Th10,FUNCTOR2:3;
end;

theorem
  F1 is_transformable_to F2 implies (idt id B)(#)p = p
proof
  assume
A1: F1 is_transformable_to F2;
  then
A2: (id B)*F1 is_transformable_to (id B)*F2 by Th10;
  thus (idt id B)(#)p = (idt (id B*F2)) `*` (id B*p) by Th18
    .= id B*p by A2,FUNCTOR2:5
    .= p by A1,Th20;
end;

theorem
  G1 is_transformable_to G2 implies q(#)(idt id B) = q
proof
  assume
A1: G1 is_transformable_to G2;
  then
A2: G1*(id B) is_transformable_to G2*(id B) by Th10;
  thus q(#)(idt id B) = (q*(id B))`*`(idt (G1*id B)) by Th19
    .= q*id B by A2,FUNCTOR2:5
    .= q by A1,Th21;
end;

theorem
  F1 is_transformable_to F2 implies G1*p = (idt G1) (#) p
proof
  assume F1 is_transformable_to F2;
  then G1*F1 is_transformable_to G1*F2 by Th10;
  hence G1*p = (idt (G1*F2))`*`(G1*p) by FUNCTOR2:5
    .= (idt G1) (#) p by Th18;
end;

theorem
  G1 is_transformable_to G2 implies q*F1 = q (#) idt F1
proof
  assume G1 is_transformable_to G2;
  then G1*F1 is_transformable_to G2*F1 by Th10;
  hence q*F1 = (q*F1)`*`(idt(G1*F1)) by FUNCTOR2:5
    .= q (#) idt F1 by Th19;
end;

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
  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)
proof
  let H1, H2 be covariant Functor of C, D, t be transformation of F1, F2, s be
  transformation of G1, G2, u be transformation of H1, H2;
  assume that
A1: F1 is_transformable_to F2 and
A2: G1 is_transformable_to G2 and
A3: H1 is_transformable_to H2;
A4: G1*F2 is_transformable_to G2*F2 & G1*F1 is_transformable_to G1*F2 by A1,A2
,Th10;
A5: H1*s*F2 = H1*(s*F2) & H1*G1*t = H1*(G1*t) by A1,A2,Th16,Th17;
A6: H1*G2*F2 = H1*(G2*F2) & H2*G2*F2 = H2*(G2*F2) by FUNCTOR0:32;
A7: H1*G1*F1 is_transformable_to H1*G1*F2 & u*G2*F2 = u*(G2*F2) by A1,A3,Th10
,Th15;
A8: H1*G1*F1 = H1*(G1*F1) & H1*G1*F2 = H1*(G1*F2) by FUNCTOR0:32;
A9: H1*G1 is_transformable_to H1*G2 by A2,Th10;
  then
A10: H1*G1*F2 is_transformable_to H1*G2*F2 by Th10;
A11: H1*G2 is_transformable_to H2*G2 by A3,Th10;
  then
A12: H1*G2*F2 is_transformable_to H2*G2*F2 by Th10;
  thus u(#)s(#)t = ((u*G2)*F2) `*` ((H1*s)*F2) `*` ((H1*G1)*t) by A11,A9,Th14
    .= (u*(G2*F2)) `*` ((H1*(s*F2)) `*` (H1*(G1*t))) by A12,A10,A7,A5,A8,A6,
FUNCTOR2:6
    .= u(#)(s(#)t) by A4,Th13;
end;

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

Lm2: now
  let A, B, C, F1, F2, G1, G2, s, t;
  set k = s(#)t;
  assume
A1: F1 is_naturally_transformable_to F2;
  then
A2: F1 is_transformable_to F2;
  assume
A3: G1 is_naturally_transformable_to G2;
  then
A4: G1 is_transformable_to G2;
A5: now
    let a, b be Object of A such that
A6: <^a,b^> <> {};
A7: <^(G1*F1).a, (G1*F1).b^> <> {} by A6,FUNCTOR0:def 18;
A8: (G2*F2).a = G2.(F2.a) by FUNCTOR0:33;
    then reconsider sF2a = s!(F2.a) as Morphism of (G1*F2).a, (G2*F2).a by
FUNCTOR0:33;
A9: (G2*F2).b = G2.(F2.b) by FUNCTOR0:33;
    then reconsider sF2b = s!(F2.b) as Morphism of (G1*F2).b, (G2*F2).b by
FUNCTOR0:33;
    <^G1.(F2.b),G2.(F2.b)^> <> {} by A4;
    then
A10: <^(G1*F2).b, (G2*F2).b^> <> {} by A9,FUNCTOR0:33;
    let f be Morphism of a,b;
A11: (G1*F1).a = G1.(F1.a) by FUNCTOR0:33;
    then reconsider
    G1tbF1f = G1.(t!b*F1.f) as Morphism of (G1*F1).a, (G1*F2).b by FUNCTOR0:33;
    reconsider G1ta = G1.(t!a) as Morphism of (G1*F1).a, (G1*F2).a by A11,
FUNCTOR0:33;
A12: <^G1.(F1.a),G2.(F1.a)^> <> {} by A4;
A13: (G1*F1).b = G1.(F1.b) by FUNCTOR0:33;
    then reconsider G1tb = G1.(t!b) as Morphism of (G1*F1).b, (G1*F2).b by
FUNCTOR0:33;
A14: <^F1.b,F2.b^> <> {} by A2;
    then <^G1.(F1.b),G1.(F2.b)^> <> {} by FUNCTOR0:def 18;
    then
A15: <^(G1*F1).b, (G1*F2).b^> <> {} by A13,FUNCTOR0:33;
A16: <^F1.a,F1.b^> <> {} by A6,FUNCTOR0:def 18;
    then
A17: <^F1.a,F2.b^> <> {} by A14,ALTCAT_1:def 2;
    reconsider G1F1f = G1.(F1.f) as Morphism of (G1*F1).a, (G1*F1).b by A13,
FUNCTOR0:33;
A18: s!(F2.a) = (s*F2).a by A4,Def2;
A19: G1.(t!b*F1.f) = G1.(t!b)*G1.(F1.f) by A14,A16,FUNCTOR0:def 23
      .= G1tb*G1F1f by A11,A13,FUNCTOR0:33;
    reconsider G2F2f = G2.(F2.f) as Morphism of (G2*F2).a, (G2*F2).b by A8,
FUNCTOR0:33;
A20: s!(F2.b) = (s*F2).b by A4,Def2;
A21: G1*F2 is_transformable_to G2*F2 by A4,Th10;
A22: <^F2.a,F2.b^> <> {} by A6,FUNCTOR0:def 18;
    then
A23: <^G2.(F2.a),G2.(F2.b)^> <> {} by FUNCTOR0:def 18;
A24: <^F1.a,F2.a^> <> {} by A2;
    then
A25: <^G2.(F1.a),G2.(F2.a)^> <> {} by FUNCTOR0:def 18;
A26: G1*F1 is_transformable_to G1*F2 by A2,Th10;
    hence (k!b)*((G1*F1).f) = ((s*F2)!b)*((G1*t)!b)*((G1*F1).f) by A21,
FUNCTOR2:def 5
      .= sF2b*((G1*t)!b)*((G1*F1).f) by A21,A20,FUNCTOR2:def 4
      .= sF2b*G1tb*((G1*F1).f) by A2,Th11
      .= sF2b*G1tb*G1F1f by A6,Th6
      .= sF2b*G1tbF1f by A7,A15,A10,A19,ALTCAT_1:21
      .= s!(F2.b)*G1.(t!b*F1.f) by A11,A9,FUNCTOR0:33
      .= G2.(t!b*F1.f)*(s!(F1.a)) by A3,A17,FUNCTOR2:def 7
      .= G2.(F2.f*(t!a))*(s!(F1.a)) by A1,A6,FUNCTOR2:def 7
      .= G2.(F2.f)*G2.(t!a)*(s!(F1.a)) by A22,A24,FUNCTOR0:def 23
      .= G2.(F2.f)*(G2.(t!a)*(s!(F1.a))) by A12,A25,A23,ALTCAT_1:21
      .= G2.(F2.f)*(s!(F2.a)*G1.(t!a)) by A3,A24,FUNCTOR2:def 7
      .= G2F2f*(sF2a*G1ta) by A11,A8,A9,FUNCTOR0:33
      .= ((G2*F2).f)*(sF2a*G1ta) by A6,Th6
      .= ((G2*F2).f)*(((s*F2)!a)*G1ta) by A21,A18,FUNCTOR2:def 4
      .= ((G2*F2).f)*(((s*F2)!a)*((G1*t)!a)) by A2,Th11
      .= ((G2*F2).f)*(k!a) by A21,A26,FUNCTOR2:def 5;
  end;
  thus G1*F1 is_naturally_transformable_to G2*F2
  by A2,A4,Th10,A5;
  hence s(#)t is natural_transformation of G1*F1, G2*F2 by A5,FUNCTOR2:def 7;
end;

theorem Th28:
  F1 is_naturally_transformable_to F2 implies G1*t is
  natural_transformation of G1*F1, G1*F2
proof
  assume
A1: F1 is_naturally_transformable_to F2;
  then
A2: F1 is_transformable_to F2;
  thus G1*F1 is_naturally_transformable_to G1*F2 by A1,Lm2;
  let a, b be Object of A such that
A3: <^a,b^> <> {};
A4: (G1*F1).b = G1.(F1.b) & <^F1.a,F1.b^> <> {} by A3,FUNCTOR0:33,def 18;
A5: <^F1.b,F2.b^> <> {} by A2;
A6: <^F1.a,F2.a^> <> {} by A2;
  reconsider G1ta = G1.(t!a) as Morphism of G1.(F1.a), (G1*F2).a by FUNCTOR0:33
;
  reconsider G1tb = G1.(t!b) as Morphism of (G1*F1).b, G1.(F2.b) by FUNCTOR0:33
;
  let f be Morphism of a, b;
A7: (G1*F2).a = G1.(F2.a) by FUNCTOR0:33;
A8: <^F2.a,F2.b^> <> {} by A3,FUNCTOR0:def 18;
A9: (G1*F1).a = G1.(F1.a) by FUNCTOR0:33;
  then reconsider G1F1f = G1.(F1.f) as Morphism of (G1*F1).a, (G1*F1).b by
FUNCTOR0:33;
A10: (G1*F2).b = G1.(F2.b) by FUNCTOR0:33;
  hence (G1*t)!b*(G1*F1).f = G1tb*((G1*F1).f) by A2,Th11
    .= G1tb*G1F1f by A3,Th6
    .= G1.(t!b*F1.f) by A9,A4,A5,FUNCTOR0:def 23
    .= G1.(F2.f*(t!a)) by A1,A3,FUNCTOR2:def 7
    .= G1.(F2.f)*G1.(t!a) by A6,A8,FUNCTOR0:def 23
    .= (G1*F2).f*G1ta by A3,A7,A10,Th6
    .= (G1*F2).f*((G1*t)!a) by A2,A9,Th11;
end;

theorem Th29:
  G1 is_naturally_transformable_to G2 implies s*F1 is
  natural_transformation of G1*F1, G2*F1
proof
  assume
A1: G1 is_naturally_transformable_to G2;
  thus G1*F1 is_naturally_transformable_to G2*F1 by A1,Lm2;
  let a, b be Object of A such that
A2: <^a,b^> <> {};
A3: <^F1.a,F1.b^> <> {} by A2,FUNCTOR0:def 18;
  reconsider sF1a = s!F1.a as Morphism of G1.(F1.a), (G2*F1).a by FUNCTOR0:33;
  let f be Morphism of a, b;
A4: (G2*F1).a = G2.(F1.a) by FUNCTOR0:33;
A5: (G2*F1).b = G2.(F1.b) by FUNCTOR0:33;
  then reconsider sF1b = s!(F1.b) as Morphism of (G1*F1).b, (G2*F1).b by
FUNCTOR0:33;
A6: (G1*F1).b = G1.(F1.b) & (G2*F1).b = G2.(F1.b) by FUNCTOR0:33;
A7: (G1*F1).a = G1.(F1.a) by FUNCTOR0:33;
  then reconsider G1F1f = G1.(F1.f) as Morphism of (G1*F1).a, (G1*F1).b by
FUNCTOR0:33;
A8: G1 is_transformable_to G2 by A1;
  hence (s*F1)!b*(G1*F1).f = sF1b*((G1*F1).f) by Th12
    .= sF1b*G1F1f by A2,Th6
    .= G2.(F1.f)*(s!F1.a) by A1,A7,A6,A3,FUNCTOR2:def 7
    .= (G2*F1).f*sF1a by A2,A4,A5,Th6
    .= (G2*F1).f*((s*F1)!a) by A8,A7,Th12;
end;

theorem
  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 by Lm2;

theorem
  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)
proof
  let t be transformation of F1, F2, t1 be transformation of F2, F3 such that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_naturally_transformable_to F3 and
A3: G1 is_naturally_transformable_to G2 and
A4: G2 is_naturally_transformable_to G3;
A5: F1 is_transformable_to F2 by A1;
  then
A6: s(#)t = (G2*t)`*`(s*F1) by A3,Th22;
A7: G2*F1 is_transformable_to G2*F2 by A5,Th10;
A8: G3*F1 is_transformable_to G3*F2 by A5,Th10;
  G1*F1 is_naturally_transformable_to G2*F2 by A1,A3,Lm2;
  then
A9: G1*F1 is_transformable_to G2*F2;
A10: G1 is_transformable_to G2 by A3;
  then
A11: G1*F1 is_transformable_to G2*F1 by Th10;
A12: F2 is_transformable_to F3 by A2;
  then
A13: s1(#)t1 = (G3*t1)`*`(s1*F2) by A4,Th22;
A14: G3*F2 is_transformable_to G3*F3 by A12,Th10;
A15: G2 is_transformable_to G3 by A4;
  then
A16: G2*F1 is_transformable_to G3*F1 by Th10;
  G1 is_transformable_to G3 by A10,A15,FUNCTOR2:2;
  then
A17: G1*F1 is_transformable_to G3*F1 by Th10;
A18: G2*F2 is_transformable_to G3*F2 by A15,Th10;
  F1 is_transformable_to F3 by A5,A12,FUNCTOR2:2;
  hence (s1`*`s)(#)(t1`*`t) = (G3*(t1`*`t))`*`((s1`*`s)*F1) by A3,A4,Th22,
FUNCTOR2:8
    .= (G3*t1)`*`(G3*t)`*`((s1`*`s)*F1) by A5,A12,Th13
    .= (G3*t1)`*`(G3*t)`*`(((s1 qua transformation of G2,G3)`*`s)*F1) by A3,A4,
FUNCTOR2:def 8
    .= (G3*t1)`*`(G3*t)`*`((s1*F1)`*`(s*F1)) by A10,A15,Th14
    .= (G3*t1)`*`((G3*t)`*`((s1*F1)`*`(s*F1))) by A14,A8,A17,FUNCTOR2:6
    .= (G3*t1)`*`((G3*t)`*`(s1*F1)`*`(s*F1)) by A8,A11,A16,FUNCTOR2:6
    .= (G3*t1)`*`((s1(#)t)`*`(s*F1)) by A4,A5,Th22
    .= (G3*t1)`*`((s1*F2)`*`((G2*t)`*`(s*F1))) by A11,A18,A7,FUNCTOR2:6
    .= (s1(#)t1)`*`(s(#)t) by A14,A18,A9,A13,A6,FUNCTOR2:6;
end;

begin  :: Natural equivalences

theorem Th32:
  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
proof
  assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1 and
A3: for a being Object of A holds t!a is iso;
  defpred P[object,object] means
   ex a being Object of A st a = $1 & $2 = (t!a)";
  set I = the carrier of A;
A4: for i being object st i in I ex j being object st P[i,j]
  proof
    let i be object;
    assume i in I;
    then reconsider o = i as Object of A;
    take (t!o)";
    thus thesis;
  end;
  consider f being ManySortedSet of I such that
A5: for i being object st i in I holds P[i,f.i] from PBOOLE:sch 3(A4);
  f is transformation of F2, F1
  proof
    thus F2 is_transformable_to F1 by A2;
    let a be Object of A;
    ex b being Object of A st b = a & f.a = (t!b)" by A5;
    hence thesis;
  end;
  then reconsider f as transformation of F2, F1;
A6: F1 is_transformable_to F2 by A1;
A7: now
    let a, b be Object of A such that
A8: <^a,b^> <> {};
A9: <^F1.a,F1.b^> <> {} by A8,FUNCTOR0:def 18;
    let g be Morphism of a, b;
A10: ex bb being Object of A st bb = b & f.b = (t!bb)" by A5;
A11: t!b is iso by A3;
A12: <^F2.a,F1.a^> <> {} by A2;
A13: <^F1.a,F2.a^> <> {} by A6;
A14: ex aa being Object of A st aa = a & f.a = (t!aa)" by A5;
    then reconsider fa = f.a as Morphism of F2.a, F1.a;
A15: t!a is iso by A3;
A16: <^F1.b,F2.b^> <> {} by A6;
A17: <^F2.b,F1.b^> <> {} by A2;
A18: <^F2.a,F2.b^> <> {} by A8,FUNCTOR0:def 18;
    then
A19: <^F2.a,F1.b^> <> {} by A17,ALTCAT_1:def 2;
    hence f!b*F2.g = f!b*(F2.g)*(idm (F2.a)) by ALTCAT_1:def 17
      .= f!b*(F2.g)*((t!a)*fa) by A14,A15,ALTCAT_3:def 5
      .= f!b*(F2.g)*((t!a)*(f!a)) by A2,FUNCTOR2:def 4
      .= f!b*(F2.g)*(t!a)*(f!a) by A13,A12,A19,ALTCAT_1:21
      .= f!b*((F2.g)*(t!a))*(f!a) by A13,A17,A18,ALTCAT_1:21
      .= f!b*((t!b)*(F1.g))*(f!a) by A1,A8,FUNCTOR2:def 7
      .= f!b*(t!b)*(F1.g)*(f!a) by A17,A16,A9,ALTCAT_1:21
      .= (t!b)"*(t!b)*(F1.g)*(f!a) by A2,A10,FUNCTOR2:def 4
      .= (idm (F1.b))*(F1.g)*(f!a) by A11,ALTCAT_3:def 5
      .= F1.g*(f!a) by A9,ALTCAT_1:20;
  end;
  hence F2 is_naturally_transformable_to F1 by A2;
  F2 is_naturally_transformable_to F1 by A2,A7;
  then reconsider f as natural_transformation of F2, F1 by A7,FUNCTOR2:def 7;
  take f;
  let a be Object of A;
  consider b being Object of A such that
A20: b = a and
A21: f.a = (t!b)" by A5;
  thus f.a = (t!a)" by A20,A21;
A22: <^F1.a,F2.a^> <> {} by A6;
A23: <^F2.a,F1.a^> <> {} by A2;
  f!a = (t!b)" by A2,A21,FUNCTOR2:def 4;
  hence thesis by A3,A20,A22,A23,ALTCAT_4:3;
end;

definition
  let A, B be category, F1, F2 be covariant Functor of A, B;
  pred F1, F2 are_naturally_equivalent means
  :Def4:
  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
  proof
    let F be covariant Functor of A, B;
    thus F is_naturally_transformable_to F & F is_transformable_to F;
    take idt F;
    let a be Object of A;
    (idt F)!a = idm (F.a) by FUNCTOR2:4;
    hence thesis;
  end;
  symmetry
  proof
    let F1, F2 be covariant Functor of A, B such that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1;
    given t being natural_transformation of F1, F2 such that
A3: for a being Object of A holds t!a is iso;
    consider f being natural_transformation of F2, F1 such that
A4: for a being Object of A holds f.a = (t!a)" & f!a is iso by A1,A2,A3,Th32;
    thus F2 is_naturally_transformable_to F1 by A1,A2,A3,Th32;
    thus F1 is_transformable_to F2 by A1;
    take f;
    thus thesis by A4;
  end;
end;

definition
  let A, B be category, F1, F2 be covariant Functor of A, B such that
A1: F1, F2 are_naturally_equivalent;
  mode natural_equivalence of F1, F2 -> natural_transformation of F1, F2 means
    :Def5:
    for a being Object of A holds it!a is iso;
  existence by A1;
end;

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

theorem Th33:
  F1, F2 are_naturally_equivalent & F2, F3
  are_naturally_equivalent implies F1, F3 are_naturally_equivalent
proof
  assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_transformable_to F1;
  given t being natural_transformation of F1, F2 such that
A3: for a being Object of A holds t!a is iso;
  assume that
A4: F2 is_naturally_transformable_to F3 and
A5: F3 is_transformable_to F2;
  given t1 being natural_transformation of F2, F3 such that
A6: for a being Object of A holds t1!a is iso;
  thus F1 is_naturally_transformable_to F3 & F3 is_transformable_to F1 by A1,A2
,A4,A5,FUNCTOR2:2,8;
  take t1 `*` t;
  let a be Object of A;
A7: t1!a is iso by A6;
  F3 is_transformable_to F1 by A2,A5,FUNCTOR2:2;
  then
A8: <^F3.a,F1.a^> <> {};
A9: t!a is iso by A3;
A10: F2 is_transformable_to F3 by A4;
  then
A11: <^F2.a,F3.a^> <> {};
A12: F1 is_transformable_to F2 by A1;
  then
A13: <^F1.a,F2.a^> <> {};
  (t1 `*` t)!a = ((t1 qua transformation of F2, F3) `*` t)!a by A1,A4,
FUNCTOR2:def 8
    .= (t1!a)*(t!a) by A12,A10,FUNCTOR2:def 5;
  hence thesis by A13,A11,A8,A7,A9,ALTCAT_3:7;
end;

theorem Th34:
  F1, F2 are_naturally_equivalent & F2, F3
  are_naturally_equivalent implies e1 `*` e is natural_equivalence of F1, F3
proof
  assume that
A1: F1, F2 are_naturally_equivalent and
A2: F2, F3 are_naturally_equivalent;
  thus
A3: F1, F3 are_naturally_equivalent by A1,A2,Th33;
  let a be Object of A;
A4: F1 is_transformable_to F2 by A1,Def4;
  then
A5: <^F1.a,F2.a^> <> {};
  F3 is_transformable_to F1 by A3;
  then
A6: <^F3.a,F1.a^> <> {};
A7: F2 is_transformable_to F3 by A2,Def4;
  then
A8: <^F2.a,F3.a^> <> {};
  F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to
  F3 by A1,A2;
  then
A9: (e1 `*` e)!a = ((e1 qua transformation of F2, F3) `*` e)!a by
FUNCTOR2:def 8
    .= (e1!a)*(e!a) by A4,A7,FUNCTOR2:def 5;
  e1!a is iso & e!a is iso by A1,A2,Def5;
  hence thesis by A9,A5,A8,A6,ALTCAT_3:7;
end;

theorem Th35:
  F1, F2 are_naturally_equivalent implies G1*F1, G1*F2
  are_naturally_equivalent & G1*e is natural_equivalence of G1*F1, G1*F2
proof
  assume
A1: F1, F2 are_naturally_equivalent;
  then
A2: F2 is_transformable_to F1;
A3: F1 is_naturally_transformable_to F2 by A1;
  then reconsider k = G1*e as natural_transformation of G1*F1, G1*F2 by Th28;
A4: F1 is_transformable_to F2 by A1,Def4;
A5: now
    let a be Object of A;
A6: (G1*F1).a = G1.(F1.a) & (G1*F2).a = G1.(F2.a) by FUNCTOR0:33;
A7: <^F2.a,F1.a^> <> {} by A2;
    k!a = G1.(e!a) & <^F1.a,F2.a^> <> {} by A4,Th11;
    hence k!a is iso by A1,A6,A7,Def5,ALTCAT_4:20;
  end;
  G1*F1, G1*F2 are_naturally_equivalent
  by A3,Lm2,A2,Th10,A5;
  hence thesis by A5,Def5;
end;

theorem Th36:
  G1, G2 are_naturally_equivalent implies G1*F1, G2*F1
  are_naturally_equivalent & f*F1 is natural_equivalence of G1*F1, G2*F1
proof
  assume
A1: G1, G2 are_naturally_equivalent;
  then
 G1 is_naturally_transformable_to G2;
  then reconsider k = f*F1 as natural_transformation of G1*F1, G2*F1 by Th29;
A2: now
    let a be Object of A;
    G1 is_transformable_to G2 by A1,Def4;
    then
A3: k!a = f!(F1.a) by Th12;
    (G1*F1).a = G1.(F1.a) & (G2*F1).a = G2.(F1.a) by FUNCTOR0:33;
    hence k!a is iso by A1,A3,Def5;
  end;
  G1*F1, G2*F1 are_naturally_equivalent
  by Lm2,A1,Th10,A2;
  hence thesis by A2,Def5;
end;

theorem
  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
proof
  assume that
A1: F1, F2 are_naturally_equivalent and
A2: G1, G2 are_naturally_equivalent;
A3: G1*F1, G1*F2 are_naturally_equivalent by A1,Th35;
  G1 is_naturally_transformable_to G2 by A2;
  then reconsider sF2 = f*F2 as natural_transformation of G1*F2, G2*F2 by Th29;
  F1 is_naturally_transformable_to F2 by A1;
  then reconsider G1t = G1*e as natural_transformation of G1*F1, G1*F2 by Th28;
A4: G1*F2, G2*F2 are_naturally_equivalent by A2,Th36;
  f*F2 is natural_equivalence of G1*F2, G2*F2 & G1*e is
  natural_equivalence of G1*F1, G1*F2 by A1,A2,Th35,Th36;
  then sF2`*`G1t is natural_equivalence of G1*F1, G2*F2 by A4,A3,Th34;
  hence thesis by A4,A3,Th33,FUNCTOR2:def 8;
end;

definition
  let A, B be category, F1, F2 be covariant Functor of A, B, e be
  natural_equivalence of F1, F2 such that
A1: F1, F2 are_naturally_equivalent;
  func e" -> natural_equivalence of F2, F1 means
  :Def6:
  for a being Object of A holds it.a = (e!a)";
  existence
  proof
A2: for a being Object of A holds e!a is iso by A1,Def5;
    F1 is_naturally_transformable_to F2 & F2 is_transformable_to F1 by A1;
    then consider f being natural_transformation of F2, F1 such that
A3: for a being Object of A holds f.a = (e!a)" & f!a is iso by A2,Th32;
    f is natural_equivalence of F2, F1
    proof
      thus F2, F1 are_naturally_equivalent by A1;
      let a be Object of A;
      thus thesis by A3;
    end;
    then reconsider f as natural_equivalence of F2, F1;
    take f;
    let a be Object of A;
    thus thesis by A3;
  end;
  uniqueness
  proof
    let P, R be natural_equivalence of F2, F1 such that
A4: for a being Object of A holds P.a = (e!a)" and
A5: for a being Object of A holds R.a = (e!a)";
A6: F2 is_transformable_to F1 by A1;
    now
      let a be Object of A;
      thus P!a = P.a by A6,FUNCTOR2:def 4
        .= (e!a)" by A4
        .= R.a by A5
        .= R!a by A6,FUNCTOR2:def 4;
    end;
    hence P = R by A6,FUNCTOR2:3;
  end;
end;

theorem Th38:
  for o being Object of A st F1, F2 are_naturally_equivalent holds
  e"!o = (e!o)"
proof
  let o be Object of A;
  assume
A1: F1, F2 are_naturally_equivalent;
  then F2 is_transformable_to F1;
  hence e"!o = e".o by FUNCTOR2:def 4
    .= (e!o)" by A1,Def6;
end;

theorem Th39:
  F1, F2 are_naturally_equivalent implies e `*` e" = idt F2
proof
  assume
A1: F1, F2 are_naturally_equivalent;
  then
A2: F1 is_transformable_to F2 & F2 is_transformable_to F1 by Def4;
A3: F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to
  F1 by A1,Def4;
  now
    let a be Object of A;
A4: e!a is iso by A1,Def5;
    thus (e `*` e")!a = ((e qua transformation of F1, F2) `*` e")!a by A3,
FUNCTOR2:def 8
      .= (e!a)*(e"!a) by A2,FUNCTOR2:def 5
      .= (e!a)*((e!a)") by A1,Th38
      .= idm (F2.a) by A4,ALTCAT_3:def 5
      .= (idt F2)!a by FUNCTOR2:4;
  end;
  hence thesis by FUNCTOR2:3;
end;

theorem
  F1, F2 are_naturally_equivalent implies e" `*` e = idt F1
proof
  assume
A1: F1, F2 are_naturally_equivalent;
  then
A2: F1 is_transformable_to F2 & F2 is_transformable_to F1 by Def4;
A3: F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to
  F1 by A1,Def4;
  now
    let a be Object of A;
A4: e!a is iso by A1,Def5;
    thus (e" `*` e)!a = (e" `*` (e qua transformation of F1, F2))!a by A3,
FUNCTOR2:def 8
      .= (e"!a)*(e!a) by A2,FUNCTOR2:def 5
      .= (e!a)"*(e!a) by A1,Th38
      .= idm (F1.a) by A4,ALTCAT_3:def 5
      .= (idt F1)!a by FUNCTOR2:4;
  end;
  hence thesis by FUNCTOR2:3;
end;

definition
  let A, B be category, F be covariant Functor of A, B;
  redefine func idt F -> natural_equivalence of F, F;  :: redefines idt (FUNCTOR2, definition)
  coherence
  proof
    set e = the natural_equivalence of F, F;
    e `*` e" = idt F by Th39;
    hence thesis by Th34;
  end;
end;

theorem
  F1, F2 are_naturally_equivalent implies (e")" = e
proof
  assume
A1: F1, F2 are_naturally_equivalent;
  then
A2: F1 is_transformable_to F2 by Def4;
  now
    let a be Object of A;
A3: <^F1.a,F2.a^> <> {} by A2;
    F2 is_transformable_to F1 by A1;
    then
A4: <^F2.a,F1.a^> <> {};
    e!a is iso by A1,Def5;
    then
A5: e!a is retraction coretraction by ALTCAT_3:5;
    thus (e")"!a = (e"!a)" by A1,Th38
      .= ((e!a)")" by A1,Th38
      .= e!a by A3,A4,A5,ALTCAT_3:3;
  end;
  hence thesis by A2,FUNCTOR2:3;
end;

theorem
  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
  "
proof
  let k be natural_equivalence of F1, F3 such that
A1: k = e1 `*` e and
A2: F1, F2 are_naturally_equivalent and
A3: F2, F3 are_naturally_equivalent;
A4: F3 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to
  F1 by A2,A3,Def4;
A5: F1 is_transformable_to F2 & F2 is_transformable_to F3 by A2,A3,Def4;
A6: F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to
  F3 by A2,A3;
A7: F3 is_transformable_to F2 & F2 is_transformable_to F1 by A2,A3;
  then
A8: F3 is_transformable_to F1 by FUNCTOR2:2;
  now
    let a be Object of A;
A9: <^F1.a,F2.a^> <> {} & <^F2.a,F3.a^> <> {} by A5;
A10: <^F3.a,F1.a^> <> {} by A8;
A11: e!a is iso & e1!a is iso by A2,A3,Def5;
    thus k"!a = ((e1 `*` e)!a)" by A1,A2,A3,Th33,Th38
      .= (((e1 qua transformation of F2, F3)`*` e)!a)" by A6,FUNCTOR2:def 8
      .= ((e1!a)*(e!a))" by A5,FUNCTOR2:def 5
      .= ((e!a)")*((e1!a)") by A11,A9,A10,ALTCAT_3:7
      .= ((e!a)")*(e1"!a) by A3,Th38
      .= (e"!a)*(e1"!a) by A2,Th38
      .= ((e" qua transformation of F2, F1)`*` e1")!a by A7,FUNCTOR2:def 5
      .= (e" `*` e1")!a by A4,FUNCTOR2:def 8;
  end;
  hence thesis by A7,FUNCTOR2:2,3;
end;

theorem
  (idt F1)" = idt F1
proof
  now
    let a be Object of A;
    thus (idt F1)"!a = ((idt F1)!a)" by Th38
      .= (idm(F1.a))" by FUNCTOR2:4
      .= idm(F1.a) by ALTCAT_3:4
      .= (idt F1)!a by FUNCTOR2:4;
  end;
  hence thesis by FUNCTOR2:3;
end;