scheme :: YELLOW18:sch 13
CatAntiIsomorphism{ F₁() -> category, F₂() -> category, F₃( object ) -> object , F₄( object , object , object ) -> object } :

F₁(),F₂() are_anti-isomorphic

provided

A1: ex F being contravariant Functor of F₁(),F₂() st
( ( for a being Object of F₁() holds F . a = F₃(a) ) & ( for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = F₄(a,b,f) ) ) and
A2: for a, b being Object of F₁() st F₃(a) = F₃(b) holds
a = b and
A3: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f, g being Morphism of a,b st F₄(a,b,f) = F₄(a,b,g) holds
f = g and
A4: for a, b being Object of F₂() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being Object of F₁() ex g being Morphism of c,d st
( b = F₃(c) & a = F₃(d) & <^c,d^> <> {} & f = F₄(c,d,g) )