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 #) & F2 * (id B) = FunctorStr(# the ObjectMap of F2,the MorphMap of F2 #) ) by FUNCTOR3:5;
A8: ( G * F2 = G1 * (G2 * F2) & F * G1 = F2 * (F1 * G1) & (G * F2) * F1 = G * F & (F * G1) * G2 = F * G ) by FUNCTOR0:33;
then ( G * F2,G1 * (id B) are_naturally_equivalent & F * G1,F2 * (id B) are_naturally_equivalent ) by A2, A3, FUNCTOR3:35;
then ( G * F,G1 * F1 are_naturally_equivalent & F * G,F2 * G2 are_naturally_equivalent ) by A5, A6, A7, A8, FUNCTOR3:36;
hence ( G * F, id A are_naturally_equivalent & F * G, id C are_naturally_equivalent ) by A1, A4, FUNCTOR3:33; :: thesis: verum