let A, B be non empty transitive with_units AltCatStr ; :: thesis: ( ex F being Functor of A,B st
( F is bijective & F is covariant ) implies ex F being Functor of B,A st
( F is bijective & F is covariant ) )
given F being Functor of A,B such that A1: ( F is bijective & F is covariant ) ; :: thesis: ex F being Functor of B,A st
( F is bijective & F is covariant )
consider G being Functor of B,A such that
G = F " and
A2: ( G is bijective & G is covariant ) by A1, Th48;
take G ; :: thesis: ( G is bijective & G is covariant )
thus ( G is bijective & G is covariant ) by A2; :: thesis: verum