scheme :: YELLOW18:sch 11
CatIsomorphism{ F1() -> category, F2() -> category, F3( object ) -> object , F4( object , object , object ) -> object } :
F1(),F2() are_isomorphic
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 = F4(a,b,f) ) ) and
A2: for a, b being Object of F1() st F3(a) = F3(b) holds
a = b and
A3: for a, b being Object of F1() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F4(a,b,f) = F4(a,b,g) holds
f = g and
A4: for a, b being Object of F2() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of F1() ex g being Morphism of c,d st
( a = F3(c) & b = F3(d) & <^c,d^> <> {} & f = F4(c,d,g) )