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, Th14;
A8: ((dualizing-func (A,B)) * (G * F)) * (dualizing-func (B,A)) = (((dualizing-func (A,B)) * G) * F) * (dualizing-func (B,A)) by FUNCTOR0:32
.= ((dualizing-func (A,B)) * G) * (F * (dualizing-func (B,A))) by FUNCTOR0:32
.= ((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:32
.= (dG * (dualizing-func (C,D))) * (F * (dualizing-func (B,A))) by A7, FUNCTOR0:32
.= dG * ((dualizing-func (C,D)) * (F * (dualizing-func (B,A)))) by FUNCTOR0:32
.= dG * dF by FUNCTOR0:32 ;
((dualizing-func (A,B)) * (id A)) * (dualizing-func (B,A)) = id B by A1, A6, Th14;
hence dG * dF, id B are_naturally_equivalent by A1, A3, A8, Th24; :: 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, Th14;
A12: ((dualizing-func (C,D)) * (F * G)) * (dualizing-func (D,C)) = (((dualizing-func (C,D)) * F) * G) * (dualizing-func (D,C)) by FUNCTOR0:32
.= ((dualizing-func (C,D)) * F) * (G * (dualizing-func (D,C))) by FUNCTOR0:32
.= ((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:32
.= (dF * (dualizing-func (A,B))) * (G * (dualizing-func (D,C))) by A11, FUNCTOR0:32
.= dF * ((dualizing-func (A,B)) * (G * (dualizing-func (D,C)))) by FUNCTOR0:32
.= dF * dG by FUNCTOR0:32 ;
((dualizing-func (C,D)) * (id C)) * (dualizing-func (D,C)) = id D by A2, A10, Th14;
hence dF * dG, id D are_naturally_equivalent by A2, A4, A12, Th24; :: thesis: verum