let A, B, C, D be category; :: thesis: ( A,B are_opposite & C,D are_opposite & A,C are_equivalent implies B,D are_equivalent )
assume that
A1: A,B are_opposite and
A2: C,D are_opposite ; :: thesis: ( not A,C are_equivalent or B,D are_equivalent )
given F being covariant Functor of A,C, G being covariant Functor of C,A such that A3: G * F, id A are_naturally_equivalent and
A4: F * G, id C are_naturally_equivalent ; :: according to YELLOW18:def 2 :: thesis: B,D are_equivalent
take dF = ((dualizing-func C,D) * F) * (dualizing-func B,A); :: according to YELLOW18:def 2 :: thesis: ex G being covariant Functor of D,B st
( G * dF, id B are_naturally_equivalent & dF * G, id D are_naturally_equivalent )
take dG = ((dualizing-func A,B) * G) * (dualizing-func D,C); :: thesis: ( dG * dF, id B are_naturally_equivalent & dF * dG, id D are_naturally_equivalent )
A5: G * (id C) = FunctorStr(# the ObjectMap of G,the MorphMap of G #) by FUNCTOR3:5;
A6: (dualizing-func A,B) * (id A) = dualizing-func A,B by FUNCTOR3:5;
A7: id C = (dualizing-func D,C) * (dualizing-func C,D) by A2, Th15;
A8: ((dualizing-func A,B) * (G * F)) * (dualizing-func B,A) = (((dualizing-func A,B) * G) * F) * (dualizing-func B,A) by FUNCTOR0:33
.= ((dualizing-func A,B) * G) * (F * (dualizing-func B,A)) by FUNCTOR0:33
.= ((dualizing-func A,B) * (G * (id C))) * (F * (dualizing-func B,A)) by A5, Th3
.= (((dualizing-func A,B) * G) * (id C)) * (F * (dualizing-func B,A)) by FUNCTOR0:33
.= (dG * (dualizing-func C,D)) * (F * (dualizing-func B,A)) by A7, FUNCTOR0:33
.= dG * ((dualizing-func C,D) * (F * (dualizing-func B,A))) by FUNCTOR0:33
.= dG * dF by FUNCTOR0:33 ;
((dualizing-func A,B) * (id A)) * (dualizing-func B,A) = id B by A1, A6, Th15;
hence dG * dF, id B are_naturally_equivalent by A1, A3, A8, Th25; :: thesis: dF * dG, id D are_naturally_equivalent
A9: F * (id A) = FunctorStr(# the ObjectMap of F,the MorphMap of F #) by FUNCTOR3:5;
A10: (dualizing-func C,D) * (id C) = dualizing-func C,D by FUNCTOR3:5;
A11: id A = (dualizing-func B,A) * (dualizing-func A,B) by A1, Th15;
A12: ((dualizing-func C,D) * (F * G)) * (dualizing-func D,C) = (((dualizing-func C,D) * F) * G) * (dualizing-func D,C) by FUNCTOR0:33
.= ((dualizing-func C,D) * F) * (G * (dualizing-func D,C)) by FUNCTOR0:33
.= ((dualizing-func C,D) * (F * (id A))) * (G * (dualizing-func D,C)) by A9, Th3
.= (((dualizing-func C,D) * F) * (id A)) * (G * (dualizing-func D,C)) by FUNCTOR0:33
.= (dF * (dualizing-func A,B)) * (G * (dualizing-func D,C)) by A11, FUNCTOR0:33
.= dF * ((dualizing-func A,B) * (G * (dualizing-func D,C))) by FUNCTOR0:33
.= dF * dG by FUNCTOR0:33 ;
((dualizing-func C,D) * (id C)) * (dualizing-func D,C) = id D by A2, A10, Th15;
hence dF * dG, id D are_naturally_equivalent by A2, A4, A12, Th25; :: thesis: verum