let A, B be category; for F1, F2, F3 being covariant Functor of A,B st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds
F1,F3 are_naturally_equivalent
let F1, F2, F3 be covariant Functor of A,B; ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies F1,F3 are_naturally_equivalent )
assume that
A1:
F1 is_naturally_transformable_to F2
and
A2:
F2 is_transformable_to F1
; FUNCTOR3:def 4 ( for t being natural_transformation of F1,F2 holds
not for a being Object of A holds t ! a is iso or not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )
given t being natural_transformation of F1,F2 such that A3:
for a being Object of A holds t ! a is iso
; ( not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )
assume that
A4:
F2 is_naturally_transformable_to F3
and
A5:
F3 is_transformable_to F2
; FUNCTOR3:def 4 ( for t being natural_transformation of F2,F3 holds
not for a being Object of A holds t ! a is iso or F1,F3 are_naturally_equivalent )
given t1 being natural_transformation of F2,F3 such that A6:
for a being Object of A holds t1 ! a is iso
; F1,F3 are_naturally_equivalent
thus
( F1 is_naturally_transformable_to F3 & F3 is_transformable_to F1 )
by A1, A2, A4, A5, FUNCTOR2:2, FUNCTOR2:8; FUNCTOR3:def 4 ex t being natural_transformation of F1,F3 st
for a being Object of A holds t ! a is iso
take
t1 `*` t
; for a being Object of A holds (t1 `*` t) ! a is iso
let a be Object of A; (t1 `*` t) ! a is iso
A7:
t1 ! a is iso
by A6;
F3 is_transformable_to F1
by A2, A5, FUNCTOR2:2;
then A8:
<^(F3 . a),(F1 . a)^> <> {}
;
A9:
t ! a is iso
by A3;
A10:
F2 is_transformable_to F3
by A4;
then A11:
<^(F2 . a),(F3 . a)^> <> {}
;
A12:
F1 is_transformable_to F2
by A1;
then A13:
<^(F1 . a),(F2 . a)^> <> {}
;
(t1 `*` t) ! a =
(t1 `*` t) ! a
by A1, A4, FUNCTOR2:def 8
.=
(t1 ! a) * (t ! a)
by A12, A10, FUNCTOR2:def 5
;
hence
(t1 `*` t) ! a is iso
by A13, A11, A8, A7, A9, ALTCAT_3:7; verum