let A, B, C be category; :: thesis: ( A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent )
given F1 being covariant Functor of A,B, G1 being covariant Functor of B,A such that A1: G1 * F1, id A are_naturally_equivalent and
A2: F1 * G1, id B are_naturally_equivalent ; :: according to YELLOW18:def 2 :: thesis: ( not B,C are_equivalent or A,C are_equivalent )
given F2 being covariant Functor of B,C, G2 being covariant Functor of C,B such that A3: G2 * F2, id B are_naturally_equivalent and
A4: F2 * G2, id C are_naturally_equivalent ; :: according to YELLOW18:def 2 :: thesis: A,C are_equivalent
take F = F2 * F1; :: according to YELLOW18:def 2 :: thesis: ex G being covariant Functor of C,A st
( G * F, id A are_naturally_equivalent & F * G, id C are_naturally_equivalent )
take G = G1 * G2; :: thesis: ( G * F, id A are_naturally_equivalent & F * G, id C are_naturally_equivalent )
FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) = FunctorStr(# the ObjectMap of F1, the MorphMap of F1 #) ;
then A5: FunctorStr(# the ObjectMap of G1, the MorphMap of G1 #) * F1 = G1 * F1 by Th3;
FunctorStr(# the ObjectMap of G2, the MorphMap of G2 #) = FunctorStr(# the ObjectMap of G2, the MorphMap of G2 #) ;
then A6: FunctorStr(# the ObjectMap of F2, the MorphMap of F2 #) * G2 = F2 * G2 by Th3;
A7: G1 * (id B) = FunctorStr(# the ObjectMap of G1, the MorphMap of G1 #) by FUNCTOR3:5;
A8: F2 * (id B) = FunctorStr(# the ObjectMap of F2, the MorphMap of F2 #) by FUNCTOR3:5;
A9: G * F2 = G1 * (G2 * F2) by FUNCTOR0:32;
A10: F * G1 = F2 * (F1 * G1) by FUNCTOR0:32;
A11: (G * F2) * F1 = G * F by FUNCTOR0:32;
A12: (F * G1) * G2 = F * G by FUNCTOR0:32;
A13: G * F2,G1 * (id B) are_naturally_equivalent by A3, A9, FUNCTOR3:35;
A14: F * G1,F2 * (id B) are_naturally_equivalent by A2, A10, FUNCTOR3:35;
A15: G * F,G1 * F1 are_naturally_equivalent by A5, A7, A11, A13, FUNCTOR3:36;
F * G,F2 * G2 are_naturally_equivalent by A6, A8, A12, A14, FUNCTOR3:36;
hence ( G * F, id A are_naturally_equivalent & F * G, id C are_naturally_equivalent ) by A1, A4, A15, FUNCTOR3:33; :: thesis: verum