scheme :: YELLOW18:sch 10
CoBijectiveSch{ F₁() -> category, F₂() -> category, F₃() -> covariant Functor of F₁(),F₂(), F₄( object ) -> object , F₅( object , object , object ) -> object } :

F₃() is bijective

provided

A1: for a being Object of F₁() holds F₃() . a = F₄(a) and
A2: 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
A3: for a, b being Object of F₁() st F₄(a) = F₄(b) holds
a = b and
A4: 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
A5: 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
( a = F₄(c) & b = F₄(d) & <^c,d^> <> {} & f = F₅(c,d,g) )