scheme :: YELLOW18:sch 22
ConcreteCatEquivalence{ F1() -> semi-functional para-functional category, F2() -> semi-functional para-functional category, F3( object ) -> object , F4( object ) -> object , F5( object , object , object ) -> Function, F6( object , object , object ) -> Function, F7( object ) -> Function, F8( object ) -> Function } :
F1(),F2() are_equivalent
provided
A1: ex F being covariant Functor of F1(),F2() st
( ( for a being Object of F1() holds F . a = F3(a) ) & ( for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F5(a,b,f) ) ) and
A2: ex G being covariant Functor of F2(),F1() st
( ( for a being Object of F2() holds G . a = F4(a) ) & ( for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = F6(a,b,f) ) ) and
A3: for a, b being Object of F1() st a = F4(F3(b)) holds
( F7(b) in <^a,b^> & F7(b) " in <^b,a^> & F7(b) is one-to-one ) and
A4: for a, b being Object of F2() st b = F3(F4(a)) holds
( F8(a) in <^a,b^> & F8(a) " in <^b,a^> & F8(a) is one-to-one ) and
A5: for a, b being Object of F1() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F7(b) * F6(F3(a),F3(b),F5(a,b,f)) = f * F7(a) and
A6: for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F5(F4(a),F4(b),F6(a,b,f)) * F8(a) = F8(b) * f