:: OPPCAT_1 semantic presentation begin definitionlet "X", "Y", "Z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set (Const "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "Z")); :: original: :::"~"::: redefine func :::"~"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "Y" "," "X" ($#k2_zfmisc_1 :::":]"::: ) ) "," "Z"; end; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func "C" :::"opp"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"CatStr"::: ) equals :: OPPCAT_1:def 1 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "C") "," (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "C") "," (Set "(" ($#k1_oppcat_1 :::"~"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C") ")" ) "#)" ); end; :: deftheorem defines :::"opp"::: OPPCAT_1:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) "," (Set "(" ($#k1_oppcat_1 :::"~"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ")" ) "#)" ))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "c" :::"opp"::: -> ($#m1_subset_1 :::"Object":::) "of" (Set "(" "C" ($#k2_oppcat_1 :::"opp"::: ) ")" ) equals :: OPPCAT_1:def 2 "c"; end; :: deftheorem defines :::"opp"::: OPPCAT_1:def 2 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "c"))))); registrationlet "C" be ($#l1_cat_1 :::"Category":::); cluster (Set "C" ($#k2_oppcat_1 :::"opp"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ; end; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "c" be ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Const "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ); func :::"opp"::: "c" -> ($#m1_subset_1 :::"Object":::) "of" "C" equals :: OPPCAT_1:def 3 (Set "c" ($#k3_oppcat_1 :::"opp"::: ) ); end; :: deftheorem defines :::"opp"::: OPPCAT_1:def 3 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) )))); theorem :: OPPCAT_1:1 canceled; theorem :: OPPCAT_1:2 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: OPPCAT_1:3 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_oppcat_1 :::"opp"::: ) (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: OPPCAT_1:4 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c")) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: OPPCAT_1:5 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "b")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) ")" )))) ; theorem :: OPPCAT_1:6 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "b")) ")" ) "," (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "a")) ")" ) ")" )))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); func "f" :::"opp"::: -> ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "C" ($#k2_oppcat_1 :::"opp"::: ) ")" ) equals :: OPPCAT_1:def 4 "f"; end; :: deftheorem defines :::"opp"::: OPPCAT_1:def 4 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Const "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ); func :::"opp"::: "f" -> ($#m1_subset_1 :::"Morphism":::) "of" "C" equals :: OPPCAT_1:def 5 (Set "f" ($#k5_oppcat_1 :::"opp"::: ) ); end; :: deftheorem defines :::"opp"::: OPPCAT_1:def 5 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) )))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); assume (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Const "a")) "," (Set (Const "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); func "f" :::"opp"::: -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "b" ($#k3_oppcat_1 :::"opp"::: ) ) "," (Set "a" ($#k3_oppcat_1 :::"opp"::: ) ) equals :: OPPCAT_1:def 6 "f"; end; :: deftheorem defines :::"opp"::: OPPCAT_1:def 6 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); assume (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Const "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) "," (Set "(" (Set (Const "b")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set (Const "a")) ($#k3_oppcat_1 :::"opp"::: ) ) "," (Set (Set (Const "b")) ($#k3_oppcat_1 :::"opp"::: ) ); func :::"opp"::: "f" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," "a" equals :: OPPCAT_1:def 7 "f"; end; :: deftheorem defines :::"opp"::: OPPCAT_1:def 7 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "b")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ) "," (Set (Set (Var "b")) ($#k3_oppcat_1 :::"opp"::: ) ) "holds" (Bool (Set ($#k8_oppcat_1 :::"opp"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))); theorem :: OPPCAT_1:7 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" ) ($#k7_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: OPPCAT_1:8 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set ($#k8_oppcat_1 :::"opp"::: ) (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: OPPCAT_1:9 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: OPPCAT_1:10 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")))) ")" )))) ; theorem :: OPPCAT_1:11 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")))) ")" )))) ; theorem :: OPPCAT_1:12 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" ))) & (Bool (Set (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" ))) ")" )))) ; theorem :: OPPCAT_1:13 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set ($#k4_oppcat_1 :::"opp"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k4_oppcat_1 :::"opp"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: OPPCAT_1:14 canceled; theorem :: OPPCAT_1:15 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f"))) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "b"))) "," (Set ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "a"))))))) ; theorem :: OPPCAT_1:16 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "g")) ($#k7_oppcat_1 :::"opp"::: ) ")" ))))))) ; theorem :: OPPCAT_1:17 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "b")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "b")) ($#k3_oppcat_1 :::"opp"::: ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "g")) ($#k7_oppcat_1 :::"opp"::: ) ")" ))))))) ; theorem :: OPPCAT_1:18 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k6_oppcat_1 :::"opp"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "g")) ")" ))))) ; theorem :: OPPCAT_1:19 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k7_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "g")) ($#k7_oppcat_1 :::"opp"::: ) ")" ))))))) ; theorem :: OPPCAT_1:20 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k7_oppcat_1 :::"opp"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" ))))) ; theorem :: OPPCAT_1:21 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set ($#k6_oppcat_1 :::"opp"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "a")) ")" ))))) ; theorem :: OPPCAT_1:22 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ) "is" ($#v7_cat_1 :::"monic"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) ) ")" )))) ; theorem :: OPPCAT_1:23 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ) "is" ($#v8_cat_1 :::"epi"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v7_cat_1 :::"monic"::: ) ) ")" )))) ; theorem :: OPPCAT_1:24 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ) "is" ($#v9_cat_1 :::"invertible"::: ) ) "iff" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ) ")" )))) ; theorem :: OPPCAT_1:25 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "c")) "is" ($#v11_cat_1 :::"initial"::: ) ) "iff" (Bool (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ) "is" ($#v10_cat_1 :::"terminal"::: ) ) ")" ))) ; theorem :: OPPCAT_1:26 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ) "is" ($#v11_cat_1 :::"initial"::: ) ) "iff" (Bool (Set (Var "c")) "is" ($#v10_cat_1 :::"terminal"::: ) ) ")" ))) ; definitionlet "C", "B" be ($#l1_cat_1 :::"Category":::); let "S" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Const "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "B"))); func :::"/*"::: "S" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "B") means :: OPPCAT_1:def 8 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "S" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" )))); end; :: deftheorem defines :::"/*"::: OPPCAT_1:def 8 : (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" )))) ")" )))); theorem :: OPPCAT_1:27 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))))))) ; theorem :: OPPCAT_1:28 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" )))))) ; theorem :: OPPCAT_1:29 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))))))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); mode :::"Contravariant_Functor"::: "of" "C" "," "D" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "D") means :: OPPCAT_1:def 9 (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" "D" "st" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Contravariant_Functor"::: OPPCAT_1:def 9 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ))) ")" ) ")" ) ")" ))); theorem :: OPPCAT_1:30 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: OPPCAT_1:31 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" )))))) ; theorem :: OPPCAT_1:32 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: OPPCAT_1:33 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" )))))) ; theorem :: OPPCAT_1:34 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "B")) "holds" (Bool (Set ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S"))) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B"))))) ; theorem :: OPPCAT_1:35 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S1")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "S2")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "S2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "S1"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")))))) ; theorem :: OPPCAT_1:36 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" )))))) ; theorem :: OPPCAT_1:37 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))))))) ; theorem :: OPPCAT_1:38 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "B")) "holds" (Bool (Set ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B"))))) ; definitionlet "C", "B" be ($#l1_cat_1 :::"Category":::); let "S" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "B"))); func :::"*'"::: "S" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" "C" ($#k2_oppcat_1 :::"opp"::: ) ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "B") means :: OPPCAT_1:def 10 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "C" ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "S" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" )))); func "S" :::"*'"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" "B" ($#k2_oppcat_1 :::"opp"::: ) ")" )) means :: OPPCAT_1:def 11 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "S" ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ))); end; :: deftheorem defines :::"*'"::: OPPCAT_1:def 10 : (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" )))) ")" )))); :: deftheorem defines :::"*'"::: OPPCAT_1:def 11 : (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "B")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) )) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ))) ")" )))); theorem :: OPPCAT_1:39 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))))))) ; theorem :: OPPCAT_1:40 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c")) ")" )))))) ; theorem :: OPPCAT_1:41 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))))))) ; theorem :: OPPCAT_1:42 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ))))) ; theorem :: OPPCAT_1:43 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c")) ")" )))))) ; theorem :: OPPCAT_1:44 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))))))) ; theorem :: OPPCAT_1:45 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ))))) ; theorem :: OPPCAT_1:46 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "F")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ))))) ; theorem :: OPPCAT_1:47 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set ($#k9_oppcat_1 :::"/*"::: ) (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "S"))))) ; theorem :: OPPCAT_1:48 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set ($#k10_oppcat_1 :::"*'"::: ) (Set "(" ($#k9_oppcat_1 :::"/*"::: ) (Set (Var "S")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "S"))))) ; theorem :: OPPCAT_1:49 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k10_oppcat_1 :::"*'"::: ) (Set "(" (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) ")" ))))) ; theorem :: OPPCAT_1:50 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "being" ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ) ($#r1_funct_2 :::"="::: ) (Set (Var "S")))))) ; theorem :: OPPCAT_1:51 (Bool "for" (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "C")) "being" ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set ($#k10_oppcat_1 :::"*'"::: ) (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" )) ($#r1_funct_2 :::"="::: ) (Set (Var "S")))))) ; theorem :: OPPCAT_1:52 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set ($#k10_oppcat_1 :::"*'"::: ) (Set "(" (Set (Var "T")) ($#k1_partfun1 :::"*"::: ) (Set (Var "S")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "T")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S")) ")" )))))) ; theorem :: OPPCAT_1:53 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k1_partfun1 :::"*"::: ) (Set (Var "S")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "S"))))))) ; theorem :: OPPCAT_1:54 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) (Bool "for" (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool (Set (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set "(" (Set (Var "F2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "F1")) ")" ) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "F2")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "F1")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ")" )))))) ; theorem :: OPPCAT_1:55 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "D"))))) ; theorem :: OPPCAT_1:56 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) ) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Set (Var "D")) ($#k2_oppcat_1 :::"opp"::: ) )))) ; theorem :: OPPCAT_1:57 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S"))) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Var "D"))))) ; theorem :: OPPCAT_1:58 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) ) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Set (Var "D")) ($#k2_oppcat_1 :::"opp"::: ) )))) ; theorem :: OPPCAT_1:59 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S1")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "S2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "S2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "S1"))) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")))))) ; theorem :: OPPCAT_1:60 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "B")) (Bool "for" (Set (Var "S2")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "S2")) ($#k1_partfun1 :::"*"::: ) (Set (Var "S1"))) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")))))) ; theorem :: OPPCAT_1:61 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "F")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ))))) ; theorem :: OPPCAT_1:62 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "F")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_oppcat_1 :::"opp"::: ) ))))) ; theorem :: OPPCAT_1:63 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "F")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Set (Var "D")) ($#k2_oppcat_1 :::"opp"::: ) )))) ; theorem :: OPPCAT_1:64 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Set "(" ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "F")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ) "is" ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ) "," (Set (Set (Var "D")) ($#k2_oppcat_1 :::"opp"::: ) )))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"id*"::: "C" -> ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" "C" "," (Set "C" ($#k2_oppcat_1 :::"opp"::: ) ) equals :: OPPCAT_1:def 12 (Set (Set "(" ($#k10_cat_1 :::"id"::: ) "C" ")" ) ($#k11_oppcat_1 :::"*'"::: ) ); func :::"*id"::: "C" -> ($#m1_oppcat_1 :::"Contravariant_Functor"::: ) "of" (Set "C" ($#k2_oppcat_1 :::"opp"::: ) ) "," "C" equals :: OPPCAT_1:def 13 (Set ($#k10_oppcat_1 :::"*'"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) "C" ")" )); end; :: deftheorem defines :::"id*"::: OPPCAT_1:def 12 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k12_oppcat_1 :::"id*"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "C")) ")" ) ($#k11_oppcat_1 :::"*'"::: ) ))); :: deftheorem defines :::"*id"::: OPPCAT_1:def 13 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k13_oppcat_1 :::"*id"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k10_oppcat_1 :::"*'"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "C")) ")" )))); theorem :: OPPCAT_1:65 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k12_oppcat_1 :::"id*"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) )))) ; theorem :: OPPCAT_1:66 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k12_oppcat_1 :::"id*"::: ) (Set (Var "C")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) )))) ; theorem :: OPPCAT_1:67 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k13_oppcat_1 :::"*id"::: ) (Set (Var "C")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")))))) ; theorem :: OPPCAT_1:68 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k13_oppcat_1 :::"*id"::: ) (Set (Var "C")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c")))))) ; theorem :: OPPCAT_1:69 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool "(" (Bool (Set ($#k10_oppcat_1 :::"*'"::: ) (Set (Var "S"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "S")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k13_oppcat_1 :::"*id"::: ) (Set (Var "C")) ")" ))) & (Bool (Set (Set (Var "S")) ($#k11_oppcat_1 :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k12_oppcat_1 :::"id*"::: ) (Set (Var "D")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "S")))) ")" ))) ; theorem :: OPPCAT_1:70 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k7_oppcat_1 :::"opp"::: ) ")" ))))))) ; theorem :: OPPCAT_1:71 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k3_oppcat_1 :::"opp"::: ) ")" ))))) ; theorem :: OPPCAT_1:72 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "a")) ")" ))))) ;