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

ex F being strict 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) ) )

provided

A1: for a being Object of F₁() holds F₃(a) is Object of F₂() and
A2: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b holds F₄(a,b,f) in the Arrows of F₂() . (F₃(b),F₃(a)) and
A3: for a, b, c being Object of F₁() st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of F₂() st a9 = F₃(a) & b9 = F₃(b) & c9 = F₃(c) holds
for f9 being Morphism of b9,a9
for g9 being Morphism of c9,b9 st f9 = F₄(a,b,f) & g9 = F₄(b,c,g) holds
F₄(a,c,(g * f)) = f9 * g9 and
A4: for a being Object of F₁()
for a9 being Object of F₂() st a9 = F₃(a) holds
F₄(a,a,(idm a)) = idm a9