:: Opposite Categories and Contravariant Functors
:: by Czes\l aw Byli\'nski
::
:: Received February 13, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
let X, Y, Z be non empty set ;
let f be PartFunc of [:X,Y:],Z;
:: original:~
redefine func ~ f ->  PartFunc of [:Y,X:],Z;
coherence
 ~ f is PartFunc of [:Y,X:],Z by FUNCT_4:48;
end;

:: Opposite Category
definition
let C be Category;
funcC opp  ->  non empty non void strict CatStr  equals :: OPPCAT_1:def 1
 CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);
coherence
 CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #) is non empty non void strict CatStr ;
end;

:: deftheorem  defines opp OPPCAT_1:def_1_:_
 for C being Category holds C opp = CatStr(# the carrier of C, the carrier' of C, the Target of C, the Source of C,(~ the Comp of C) #);

definition
let C be Category;
let c be Object of C;
funcc opp  ->  Object of (C opp) equals :: OPPCAT_1:def 2
c;
coherence
 c is Object of (C opp) ;
end;

:: deftheorem  defines opp OPPCAT_1:def_2_:_
 for C being Category
for c being Object of C holds c opp = c;

registration
let C be Category;
clusterC opp  ->  non empty non void strict Category-like transitive associative reflexive with_identities ;
coherence
 ( C opp is Category-like & C opp is transitive & C opp is associative & C opp is reflexive & C opp is with_identities )
proofend;
end;

definition
let C be Category;
let c be Object of (C opp);
func opp c ->  Object of C equals :: OPPCAT_1:def 3
c opp ;
coherence
 c opp is Object of C ;
end;

:: deftheorem  defines opp OPPCAT_1:def_3_:_
 for C being Category
for c being Object of (C opp) holds opp c = c opp ;

theorem :: OPPCAT_1:1
canceled;

theorem :: OPPCAT_1:2
for C being Category
for c being Object of C holds (c opp) opp = c ;

theorem :: OPPCAT_1:3
for C being Category
for c being Object of C holds opp (c opp) = c ;

theorem :: OPPCAT_1:4
for C being Category
for c being Object of (C opp) holds (opp c) opp = c ;

theorem Th5: :: OPPCAT_1:5
for C being Category
for a, b being Object of C holds Hom (a,b) = Hom ((b opp),(a opp))
proofend;

theorem Th6: :: OPPCAT_1:6
for C being Category
for a, b being Object of (C opp) holds Hom (a,b) = Hom ((opp b),(opp a))
proofend;

definition
let C be Category;
let f be Morphism of C;
funcf opp  ->  Morphism of (C opp) equals :: OPPCAT_1:def 4
f;
coherence
 f is Morphism of (C opp) ;
end;

:: deftheorem  defines opp OPPCAT_1:def_4_:_
 for C being Category
for f being Morphism of C holds f opp = f;

definition
let C be Category;
let f be Morphism of (C opp);
func opp f ->  Morphism of C equals :: OPPCAT_1:def 5
f opp ;
coherence
 f opp is Morphism of C ;
end;

:: deftheorem  defines opp OPPCAT_1:def_5_:_
 for C being Category
for f being Morphism of (C opp) holds opp f = f opp ;

definition
let C be Category;
let a, b be Object of C;
assume Z: Hom (a,b) <> {} ;
let f be Morphism of a,b;
funcf opp  ->  Morphism of b opp ,a opp  equals :Def6: :: OPPCAT_1:def 6
f;
coherence
 f is Morphism of b opp ,a opp
proofend;
end;

:: deftheorem Def6 defines opp OPPCAT_1:def_6_:_
 for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds f opp = f;

definition
let C be Category;
let a, b be Object of C;
assume Z: Hom ((a opp),(b opp)) <> {} ;
let f be Morphism of a opp ,b opp ;
func opp f ->  Morphism of b,a equals :Def7: :: OPPCAT_1:def 7
f;
coherence
 f is Morphism of b,a
proofend;
end;

:: deftheorem Def7 defines opp OPPCAT_1:def_7_:_
 for C being Category
for a, b being Object of C st Hom ((a opp),(b opp)) <> {} holds
for f being Morphism of a opp ,b opp holds opp f = f;

theorem :: OPPCAT_1:7
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (f opp) opp = f
proofend;

theorem :: OPPCAT_1:8
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds opp (f opp) = f
proofend;

theorem :: OPPCAT_1:9
for C being Category
for a, b being Object of (C opp)
for f being Morphism of a,b holds (opp f) opp = f ;

theorem Th10: :: OPPCAT_1:10
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( dom (f opp) = cod f &amp; cod (f opp) = dom f )
proofend;

theorem :: OPPCAT_1:11
for C being Category
for a, b being Object of (C opp)
for f being Morphism of a,b holds
( dom (opp f) = cod f &amp; cod (opp f) = dom f ) ;

theorem :: OPPCAT_1:12
for C being Category
for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( (dom f) opp = cod (f opp) &amp; (cod f) opp = dom (f opp) ) by Th10;

theorem :: OPPCAT_1:13
for C being Category
for a, b being Object of (C opp) st Hom (a,b) <> {} holds
for f being Morphism of a,b holds
( opp (dom f) = cod (opp f) &amp; opp (cod f) = dom (opp f) ) ;

theorem :: OPPCAT_1:14
canceled;

theorem Th15: :: OPPCAT_1:15
for C being Category
for a, b being Object of (C opp)
for f being Morphism of a,b st Hom (a,b) <> {} holds
opp f is Morphism of opp b, opp a
proofend;

theorem Th16: :: OPPCAT_1:16
for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} &amp; Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
proofend;

theorem :: OPPCAT_1:17
for C being Category
for a, b, c being Object of C st Hom ((b opp),(a opp)) <> {} &amp; Hom ((c opp),(b opp)) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (g (*) f) opp = (f opp) (*) (g opp)
proofend;

theorem Th18: :: OPPCAT_1:18
for C being Category
for f, g being Morphism of (C opp) st dom g = cod f holds
opp (g (*) f) = (opp f) (*) (opp g)
proofend;

theorem :: OPPCAT_1:19
for C being Category
for a, b, c being Object of C
for f being Morphism of a,b
for g being Morphism of b,c st Hom (a,b) <> {} &amp; Hom (b,c) <> {} holds
(g * f) opp = (f opp) (*) (g opp)
proofend;

Lm1:  for C being Category
for a being Object of C
for b being Object of (C opp) holds
( ( Hom ((a opp),b) <> {} implies for f being Morphism of a opp ,b holds f (*) ((id a) opp) = f ) &amp; ( Hom (b,(a opp)) <> {} implies for f being Morphism of b,a opp holds ((id a) opp) (*) f = f ) )
proofend;

theorem Th20: :: OPPCAT_1:20
for C being Category
for a being Object of C holds (id a) opp = id (a opp)
proofend;

Lm2:  for C being Category
for a being Object of C holds id a = id (a opp)
proofend;

theorem Th21: :: OPPCAT_1:21
for C being Category
for a being Object of (C opp) holds opp (id a) = id (opp a)
proofend;

Lm3:  for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} &amp; Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (f opp) * (g opp)
proofend;

theorem :: OPPCAT_1:22
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f opp is monic iff f is epi )
proofend;

theorem :: OPPCAT_1:23
for C being Category
for b, c being Object of C st Hom (b,c) <> {} holds
for f being Morphism of b,c holds
( f opp is epi iff f is monic )
proofend;

theorem :: OPPCAT_1:24
for C being Category
for a, b being Object of C
for f being Morphism of a,b holds
( f opp is invertible iff f is invertible )
proofend;

theorem :: OPPCAT_1:25
for C being Category
for c being Object of C holds
( c is initial iff c opp is terminal )
proofend;

theorem :: OPPCAT_1:26
for C being Category
for c being Object of C holds
( c opp is initial iff c is terminal )
proofend;

:: Contravariant Functors
definition
let C, B be Category;
let S be Function of the carrier' of (C opp), the carrier' of B;
func /* S ->  Function of the carrier' of C, the carrier' of B means :Def8: :: OPPCAT_1:def 8
 for f being Morphism of C holds it . f = S . (f opp);
existence
 ex b1 being Function of the carrier' of C, the carrier' of B st
for f being Morphism of C holds b1 . f = S . (f opp)
proofend;
uniqueness
 for b1, b2 being Function of the carrier' of C, the carrier' of B st ( for f being Morphism of C holds b1 . f = S . (f opp) ) &amp; ( for f being Morphism of C holds b2 . f = S . (f opp) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines /* OPPCAT_1:def_8_:_
 for C, B being Category
for S being Function of the carrier' of (C opp), the carrier' of B
for b4 being Function of the carrier' of C, the carrier' of B holds
( b4 = /* S iff for f being Morphism of C holds b4 . f = S . (f opp) );

theorem :: OPPCAT_1:27
for C, B being Category
for S being Function of the carrier' of (C opp), the carrier' of B
for f being Morphism of (C opp) holds (/* S) . (opp f) = S . f
proofend;

Lm4:  for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
proofend;

theorem Th28: :: OPPCAT_1:28
for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
proofend;

theorem :: OPPCAT_1:29
for C, B being Category
for S being Functor of C opp ,B
for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
proofend;

Lm5:  for C, B being Category
for S being Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
proofend;

Lm6: now__::_thesis:_for_C,_B_being_Category
for_S_being_Functor_of_C_opp_,B
for_c_being_Object_of_C_ex_d_being_Object_of_B_st_(/*_S)_._(id_c)_=_id_d
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for c being Object of C ex d being Object of B st (/* S) . (id c) = id d
let S be Functor of C opp ,B; ::_thesis: for c being Object of C ex d being Object of B st (/* S) . (id c) = id d
let c be Object of C; ::_thesis: ex d being Object of B st (/* S) . (id c) = id d
 (/* S) . (id c) = id ((Obj (/* S)) . c) by Lm5;
hence  ex d being Object of B st (/* S) . (id c) = id d ; ::_thesis: verum
end;

Lm7:  for C, B being Category
for S being Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = cod ((/* S) . f) &amp; (Obj (/* S)) . (cod f) = dom ((/* S) . f) )
proofend;

Lm8: now__::_thesis:_for_C,_B_being_Category
for_S_being_Functor_of_C_opp_,B
for_f_being_Morphism_of_C_holds_
(_(/*_S)_._(id_(dom_f))_=_id_(cod_((/*_S)_._f))_&amp;_(/*_S)_._(id_(cod_f))_=_id_(dom_((/*_S)_._f))_)
let C, B be Category; ::_thesis: for S being Functor of C opp ,B
for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) &amp; (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )
let S be Functor of C opp ,B; ::_thesis: for f being Morphism of C holds
( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) &amp; (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )
let f be Morphism of C; ::_thesis: ( (/* S) . (id (dom f)) = id (cod ((/* S) . f)) &amp; (/* S) . (id (cod f)) = id (dom ((/* S) . f)) )
thus (/* S) . (id (dom f)) = id ((Obj (/* S)) . (dom f)) by Lm5
.= id (cod ((/* S) . f)) by Lm7 ; ::_thesis: (/* S) . (id (cod f)) = id (dom ((/* S) . f))
thus (/* S) . (id (cod f)) = id ((Obj (/* S)) . (cod f)) by Lm5
.= id (dom ((/* S) . f)) by Lm7 ; ::_thesis: verum
end;

Lm9:  for C, B being Category
for S being Functor of C opp ,B
for a, b, c being Object of C st Hom (a,b) <> {} &amp; Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds (/* S) . (g (*) f) = ((/* S) . f) (*) ((/* S) . g)
proofend;

definition
let C, D be Category;
mode Contravariant_Functor of C,D ->  Function of the carrier' of C, the carrier' of D means :Def9: :: OPPCAT_1:def 9
( ( for c being Object of C ex d being Object of D st it . (id c) = id d ) &amp; ( for f being Morphism of C holds
( it . (id (dom f)) = id (cod (it . f)) &amp; it . (id (cod f)) = id (dom (it . f)) ) ) &amp; ( for f, g being Morphism of C st dom g = cod f holds
it . (g (*) f) = (it . f) (*) (it . g) ) );
existence
 ex b1 being Function of the carrier' of C, the carrier' of D st
( ( for c being Object of C ex d being Object of D st b1 . (id c) = id d ) &amp; ( for f being Morphism of C holds
( b1 . (id (dom f)) = id (cod (b1 . f)) &amp; b1 . (id (cod f)) = id (dom (b1 . f)) ) ) &amp; ( for f, g being Morphism of C st dom g = cod f holds
b1 . (g (*) f) = (b1 . f) (*) (b1 . g) ) )
proofend;
end;

:: deftheorem Def9 defines Contravariant_Functor OPPCAT_1:def_9_:_
 for C, D being Category
for b3 being Function of the carrier' of C, the carrier' of D holds
( b3 is Contravariant_Functor of C,D iff ( ( for c being Object of C ex d being Object of D st b3 . (id c) = id d ) &amp; ( for f being Morphism of C holds
( b3 . (id (dom f)) = id (cod (b3 . f)) &amp; b3 . (id (cod f)) = id (dom (b3 . f)) ) ) &amp; ( for f, g being Morphism of C st dom g = cod f holds
b3 . (g (*) f) = (b3 . f) (*) (b3 . g) ) ) );

theorem Th30: :: OPPCAT_1:30
for C, D being Category
for S being Contravariant_Functor of C,D
for c being Object of C
for d being Object of D st S . (id c) = id d holds
(Obj S) . c = d
proofend;

theorem Th31: :: OPPCAT_1:31
for C, D being Category
for S being Contravariant_Functor of C,D
for c being Object of C holds S . (id c) = id ((Obj S) . c)
proofend;

theorem Th32: :: OPPCAT_1:32
for C, D being Category
for S being Contravariant_Functor of C,D
for f being Morphism of C holds
( (Obj S) . (dom f) = cod (S . f) &amp; (Obj S) . (cod f) = dom (S . f) )
proofend;

theorem Th33: :: OPPCAT_1:33
for C, D being Category
for S being Contravariant_Functor of C,D
for f, g being Morphism of C st dom g = cod f holds
dom (S . f) = cod (S . g)
proofend;

theorem Th34: :: OPPCAT_1:34
for C, B being Category
for S being Functor of C opp ,B holds /* S is Contravariant_Functor of C,B
proofend;

theorem Th35: :: OPPCAT_1:35
for C, B, D being Category
for S1 being Contravariant_Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Functor of C,D
proofend;

Lm10:  for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj S) . (c opp))
proofend;

theorem Th36: :: OPPCAT_1:36
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (Obj (/* S)) . c = (Obj S) . (c opp)
proofend;

theorem :: OPPCAT_1:37
for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of (C opp) holds (Obj (/* S)) . (opp c) = (Obj S) . c
proofend;

Lm11:  for C, B being Category
for S being Contravariant_Functor of C opp ,B
for c being Object of C holds (/* S) . (id c) = id ((Obj (/* S)) . c)
proofend;

Lm12:  for C, B being Category
for S being Contravariant_Functor of C opp ,B
for f being Morphism of C holds
( (Obj (/* S)) . (dom f) = dom ((/* S) . f) &amp; (Obj (/* S)) . (cod f) = cod ((/* S) . f) )
proofend;

theorem :: OPPCAT_1:38
for C, B being Category
for S being Contravariant_Functor of C opp ,B holds /* S is Functor of C,B
proofend;

:: Dualization functors
definition
let C, B be Category;
let S be Function of the carrier' of C, the carrier' of B;
func *' S ->  Function of the carrier' of (C opp), the carrier' of B means :Def10: :: OPPCAT_1:def 10
 for f being Morphism of (C opp) holds it . f = S . (opp f);
existence
 ex b1 being Function of the carrier' of (C opp), the carrier' of B st
for f being Morphism of (C opp) holds b1 . f = S . (opp f)
proofend;
uniqueness
 for b1, b2 being Function of the carrier' of (C opp), the carrier' of B st ( for f being Morphism of (C opp) holds b1 . f = S . (opp f) ) &amp; ( for f being Morphism of (C opp) holds b2 . f = S . (opp f) ) holds
b1 = b2
proofend;
funcS *'  ->  Function of the carrier' of C, the carrier' of (B opp) means :Def11: :: OPPCAT_1:def 11
 for f being Morphism of C holds it . f = (S . f) opp ;
existence
 ex b1 being Function of the carrier' of C, the carrier' of (B opp) st
for f being Morphism of C holds b1 . f = (S . f) opp
proofend;
uniqueness
 for b1, b2 being Function of the carrier' of C, the carrier' of (B opp) st ( for f being Morphism of C holds b1 . f = (S . f) opp ) &amp; ( for f being Morphism of C holds b2 . f = (S . f) opp ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines *' OPPCAT_1:def_10_:_
 for C, B being Category
for S being Function of the carrier' of C, the carrier' of B
for b4 being Function of the carrier' of (C opp), the carrier' of B holds
( b4 = *' S iff for f being Morphism of (C opp) holds b4 . f = S . (opp f) );

:: deftheorem Def11 defines *' OPPCAT_1:def_11_:_
 for C, B being Category
for S being Function of the carrier' of C, the carrier' of B
for b4 being Function of the carrier' of C, the carrier' of (B opp) holds
( b4 = S *' iff for f being Morphism of C holds b4 . f = (S . f) opp );

theorem :: OPPCAT_1:39
for C, B being Category
for S being Function of the carrier' of C, the carrier' of B
for f being Morphism of C holds (*' S) . (f opp) = S . f
proofend;

Lm13:  for C, B being Category
for S being Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
proofend;

theorem Th40: :: OPPCAT_1:40
for C, B being Category
for S being Functor of C,B
for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
proofend;

theorem :: OPPCAT_1:41
for C, B being Category
for S being Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
proofend;

Lm14:  for C, B being Category
for S being Functor of C,B
for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
proofend;

theorem Th42: :: OPPCAT_1:42
for C, B being Category
for S being Functor of C,B
for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
proofend;

Lm15:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj S) . (opp c))
proofend;

theorem Th43: :: OPPCAT_1:43
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (Obj (*' S)) . c = (Obj S) . (opp c)
proofend;

theorem :: OPPCAT_1:44
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (*' S)) . (c opp) = (Obj S) . c
proofend;

Lm16:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (S *') . (id c) = id (((Obj S) . c) opp)
proofend;

theorem Th45: :: OPPCAT_1:45
for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (Obj (S *')) . c = ((Obj S) . c) opp
proofend;

Lm17:  for C, D being Category
for F being Function of the carrier' of C, the carrier' of D
for f being Morphism of (C opp) holds ((*' F) *') . f = (F . (opp f)) opp
proofend;

theorem Th46: :: OPPCAT_1:46
for C, D being Category
for F being Function of the carrier' of C, the carrier' of D
for f being Morphism of C holds ((*' F) *') . (f opp) = (F . f) opp
proofend;

theorem Th47: :: OPPCAT_1:47
for C, D being Category
for S being Function of the carrier' of C, the carrier' of D holds /* (*' S) = S
proofend;

theorem :: OPPCAT_1:48
for C, D being Category
for S being Function of the carrier' of (C opp), the carrier' of D holds *' (/* S) = S
proofend;

theorem :: OPPCAT_1:49
for C, D being Category
for S being Function of the carrier' of C, the carrier' of D holds (*' S) *' = *' (S *')
proofend;

theorem :: OPPCAT_1:50
for C being Category
for D being strict Category
for S being Function of the carrier' of C, the carrier' of D holds (S *') *' = S
proofend;

theorem :: OPPCAT_1:51
for D being Category
for C being strict Category
for S being Function of the carrier' of C, the carrier' of D holds *' (*' S) = S
proofend;

Lm18:  for C, B, D being Category
for S being Function of the carrier' of (C opp), the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds /* (T * S) = T * (/* S)
proofend;

theorem :: OPPCAT_1:52
for C, B, D being Category
for S being Function of the carrier' of C, the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds *' (T * S) = T * (*' S)
proofend;

theorem :: OPPCAT_1:53
for C, B, D being Category
for S being Function of the carrier' of C, the carrier' of B
for T being Function of the carrier' of B, the carrier' of D holds (T * S) *' = (T *') * S
proofend;

theorem :: OPPCAT_1:54
for C, B, D being Category
for F1 being Function of the carrier' of C, the carrier' of B
for F2 being Function of the carrier' of B, the carrier' of D holds (*' (F2 * F1)) *' = ((*' F2) *') * ((*' F1) *')
proofend;

Lm19:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
proofend;

Lm20:  for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = dom ((*' S) . f) &amp; (Obj (*' S)) . (cod f) = cod ((*' S) . f) )
proofend;

theorem Th55: :: OPPCAT_1:55
for C, D being Category
for S being Contravariant_Functor of C,D holds *' S is Functor of C opp ,D
proofend;

Lm21:  for C, B being Category
for S being Contravariant_Functor of C,B
for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
proofend;

Lm22:  for C, B being Category
for S being Contravariant_Functor of C,B
for f being Morphism of C holds
( (Obj (S *')) . (dom f) = dom ((S *') . f) &amp; (Obj (S *')) . (cod f) = cod ((S *') . f) )
proofend;

theorem Th56: :: OPPCAT_1:56
for C, D being Category
for S being Contravariant_Functor of C,D holds S *' is Functor of C,D opp
proofend;

Lm23:  for C, B being Category
for S being Functor of C,B
for c being Object of (C opp) holds (*' S) . (id c) = id ((Obj (*' S)) . c)
proofend;

Lm24:  for C, B being Category
for S being Functor of C,B
for f being Morphism of (C opp) holds
( (Obj (*' S)) . (dom f) = cod ((*' S) . f) &amp; (Obj (*' S)) . (cod f) = dom ((*' S) . f) )
proofend;

theorem Th57: :: OPPCAT_1:57
for C, D being Category
for S being Functor of C,D holds *' S is Contravariant_Functor of C opp ,D
proofend;

Lm25:  for C, B being Category
for S being Functor of C,B
for c being Object of C holds (S *') . (id c) = id ((Obj (S *')) . c)
proofend;

Lm26:  for C, B being Category
for S being Functor of C,B
for f being Morphism of C holds
( (Obj (S *')) . (dom f) = cod ((S *') . f) &amp; (Obj (S *')) . (cod f) = dom ((S *') . f) )
proofend;

theorem Th58: :: OPPCAT_1:58
for C, D being Category
for S being Functor of C,D holds S *' is Contravariant_Functor of C,D opp
proofend;

theorem :: OPPCAT_1:59
for C, B, D being Category
for S1 being Contravariant_Functor of C,B
for S2 being Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
proofend;

theorem :: OPPCAT_1:60
for C, B, D being Category
for S1 being Functor of C,B
for S2 being Contravariant_Functor of B,D holds S2 * S1 is Contravariant_Functor of C,D
proofend;

theorem :: OPPCAT_1:61
for C, D being Category
for F being Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
proofend;

theorem :: OPPCAT_1:62
for C, D being Category
for F being Contravariant_Functor of C,D
for c being Object of C holds (Obj ((*' F) *')) . (c opp) = ((Obj F) . c) opp
proofend;

theorem :: OPPCAT_1:63
for C, D being Category
for F being Functor of C,D holds (*' F) *' is Functor of C opp ,D opp
proofend;

theorem :: OPPCAT_1:64
for C, D being Category
for F being Contravariant_Functor of C,D holds (*' F) *' is Contravariant_Functor of C opp ,D opp
proofend;

:: Duality Functors
definition
let C be Category;
func id* C ->  Contravariant_Functor of C,C opp  equals :: OPPCAT_1:def 12
(id C) *' ;
coherence
 (id C) *' is Contravariant_Functor of C,C opp by Th58;
func *id C ->  Contravariant_Functor of C opp ,C equals :: OPPCAT_1:def 13
 *' (id C);
coherence
 *' (id C) is Contravariant_Functor of C opp ,C by Th57;
end;

:: deftheorem  defines id* OPPCAT_1:def_12_:_
 for C being Category holds id* C = (id C) *' ;

:: deftheorem  defines *id OPPCAT_1:def_13_:_
 for C being Category holds *id C = *' (id C);

theorem Th65: :: OPPCAT_1:65
for C being Category
for f being Morphism of C holds (id* C) . f = f opp
proofend;

theorem :: OPPCAT_1:66
for C being Category
for c being Object of C holds (Obj (id* C)) . c = c opp
proofend;

theorem Th67: :: OPPCAT_1:67
for C being Category
for f being Morphism of (C opp) holds (*id C) . f = opp f
proofend;

theorem :: OPPCAT_1:68
for C being Category
for c being Object of (C opp) holds (Obj (*id C)) . c = opp c
proofend;

theorem :: OPPCAT_1:69
for C, D being Category
for S being Function of the carrier' of C, the carrier' of D holds
( *' S = S * (*id C) &amp; S *' = (id* D) * S )
proofend;

theorem :: OPPCAT_1:70
for C being Category
for a, b, c being Object of C st Hom (a,b) <> {} &amp; Hom (b,c) <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = (f opp) * (g opp) by Lm3;

theorem Th71: :: OPPCAT_1:71
for C being Category
for a being Object of C holds id a = id (a opp) by Lm2;

theorem :: OPPCAT_1:72
for C being Category
for a being Object of (C opp) holds id a = id (opp a)
proofend;