let A, B, C, D be category; ( 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
; ( 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
; YELLOW18:def 2 B,D are_equivalent
take dF = ((dualizing-func (C,D)) * F) * (dualizing-func (B,A)); YELLOW18:def 2 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)); ( 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; 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; verum