:: ISOCAT_2 semantic presentation begin definitionlet "A", "B", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Const "B")) "," (Set (Const "C")) ")" ")" ); :: original: :::"uncurry"::: redefine func :::"uncurry"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) "," "C"; end; theorem :: ISOCAT_2:1 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set ($#k11_funct_5 :::"curry"::: ) (Set "(" ($#k1_isocat_2 :::"uncurry"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: ISOCAT_2:2 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k1_isocat_2 :::"uncurry"::: ) (Set (Var "f")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k10_funct_5 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))))))) ; theorem :: ISOCAT_2:3 canceled; theorem :: ISOCAT_2:4 canceled; theorem :: ISOCAT_2:5 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: ISOCAT_2:6 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: ISOCAT_2:7 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "o")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" )) "iff" (Bool (Set (Var "o")) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" ))) ; theorem :: ISOCAT_2:8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) (Bool "ex" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "F2"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ")" ))))) ; begin definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")); func "a" :::"|->"::: "B" -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k11_nattra_1 :::"Functors"::: ) "(" "A" "," "B" ")" ) "," "B" means :: ISOCAT_2:def 1 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) "a")))); end; :: deftheorem defines :::"|->"::: ISOCAT_2:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_isocat_2 :::"|->"::: ) (Set (Var "B")))) "iff" (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")))))) ")" )))); theorem :: ISOCAT_2:9 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "A")) ")" ) ($#r1_isocat_1 :::"~="::: ) (Set (Var "A"))))) ; begin theorem :: ISOCAT_2:10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k9_cat_2 :::"]"::: ) ))))))) ; theorem :: ISOCAT_2:11 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "iff" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "b1")) ($#k9_cat_2 :::"]"::: ) ) "," (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "b2")) ($#k9_cat_2 :::"]"::: ) ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )))) ; theorem :: ISOCAT_2:12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "b1")) ($#k9_cat_2 :::"]"::: ) ) "," (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "b2")) ($#k9_cat_2 :::"]"::: ) ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) ) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "b1")) ($#k9_cat_2 :::"]"::: ) ) "," (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "b2")) ($#k9_cat_2 :::"]"::: ) )) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a1")) "," (Set (Var "a2"))) & (Bool (Set (Var "g")) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b1")) "," (Set (Var "b2"))) ")" ) ")" )))))) ; theorem :: ISOCAT_2:13 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "F1")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a"))) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Set (Var "F2")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "t")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Set (Var "F1")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a"))) "," (Set (Set (Var "F2")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a")))) ")" ))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Const "C")); let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "A")); func :::"curry"::: "(" "F" "," "f" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "B") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") equals :: ISOCAT_2:def 2 (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) "F" ")" ) ($#k1_funct_1 :::"."::: ) "f"); end; :: deftheorem defines :::"curry"::: ISOCAT_2:def 2 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k3_isocat_2 :::"curry"::: ) "(" (Set (Var "F")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))))))); theorem :: ISOCAT_2:14 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) ")" ))) "holds" (Bool (Set ($#k10_cat_2 :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k10_cat_2 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a1")) "," (Set (Var "b1")) ($#k9_cat_2 :::"]"::: ) ) "," (Set ($#k9_cat_2 :::"["::: ) (Set (Var "a2")) "," (Set (Var "b2")) ($#k9_cat_2 :::"]"::: ) ) ")" ))))))) ; theorem :: ISOCAT_2:15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "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 (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a"))) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "b")))) & (Bool (Set (Set "(" ($#k3_isocat_2 :::"curry"::: ) "(" (Set (Var "F")) "," (Set (Var "f")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_isocat_1 :::"IdMap"::: ) (Set (Var "B")) ")" )) "is" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a"))) "," (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "b")))) ")" ))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Const "C")); let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "A")); func "F" :::"?-"::: "f" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set "F" ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) "f" ")" )) "," (Set "F" ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) "f" ")" )) equals :: ISOCAT_2:def 3 (Set (Set "(" ($#k3_isocat_2 :::"curry"::: ) "(" "F" "," "f" ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_isocat_1 :::"IdMap"::: ) "B" ")" )); end; :: deftheorem defines :::"?-"::: ISOCAT_2:def 3 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "F")) ($#k4_isocat_2 :::"?-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_isocat_2 :::"curry"::: ) "(" (Set (Var "F")) "," (Set (Var "f")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_isocat_1 :::"IdMap"::: ) (Set (Var "B")) ")" )))))); theorem :: ISOCAT_2:16 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" )) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")) ")" )))))) ; theorem :: ISOCAT_2:17 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_isocat_2 :::"?-"::: ) (Set (Var "f")) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k11_cat_2 :::"."::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" ) ")" )))))) ; theorem :: ISOCAT_2:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k6_nattra_1 :::"id"::: ) (Set "(" (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k4_isocat_2 :::"?-"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )))))) ; theorem :: ISOCAT_2:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )) "," (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "g")) ")" )) "st" (Bool (Bool (Set (Var "t")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k4_isocat_2 :::"?-"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "F")) ($#k4_isocat_2 :::"?-"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_isocat_2 :::"?-"::: ) (Set (Var "g")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t")))))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Const "C")); func :::"export"::: "F" -> ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," (Set ($#k11_nattra_1 :::"Functors"::: ) "(" "B" "," "C" ")" ) means :: ISOCAT_2:def 4 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" "F" ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" "F" ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" "F" ($#k4_isocat_2 :::"?-"::: ) (Set (Var "f")) ")" ) ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"export"::: ISOCAT_2:def 4 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "b5")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "F")) ($#k4_isocat_2 :::"?-"::: ) (Set (Var "f")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" )))); theorem :: ISOCAT_2:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k12_cat_2 :::"?-"::: ) (Set (Var "a"))))))) ; theorem :: ISOCAT_2:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")))))) ; theorem :: ISOCAT_2:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1"))) ($#r2_funct_2 :::"="::: ) (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2"))))) "holds" (Bool (Set (Var "F1")) ($#r2_funct_2 :::"="::: ) (Set (Var "F2"))))) ; theorem :: ISOCAT_2:23 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1"))) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2")))) & (Bool "ex" (Set (Var "G")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1"))) "," (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2"))) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool (Bool (Set (Var "t")) ($#r1_funct_2 :::"="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "G")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k9_cat_2 :::"["::: ) (Set "(" (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k9_cat_2 :::"]"::: ) ) "," (Set "(" (Set "(" ($#k11_funct_5 :::"curry"::: ) (Set (Var "s")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_tarski :::"]"::: ) ))))) ")" )))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Const "C")); assume (Bool (Set (Const "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "F2"))) ; let "t" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); func :::"export"::: "t" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set ($#k5_isocat_2 :::"export"::: ) "F1") "," (Set ($#k5_isocat_2 :::"export"::: ) "F2") means :: ISOCAT_2:def 5 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "st" (Bool (Bool "t" ($#r1_funct_2 :::"="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Set it ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k9_cat_2 :::"["::: ) (Set "(" (Set "(" ($#k5_isocat_2 :::"export"::: ) "F1" ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set "(" ($#k5_isocat_2 :::"export"::: ) "F2" ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k9_cat_2 :::"]"::: ) ) "," (Set "(" (Set "(" ($#k11_funct_5 :::"curry"::: ) (Set (Var "s")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_tarski :::"]"::: ) )))); end; :: deftheorem defines :::"export"::: ISOCAT_2:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "b7")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1"))) "," (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2"))) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k6_isocat_2 :::"export"::: ) (Set (Var "t")))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool (Bool (Set (Var "t")) ($#r1_funct_2 :::"="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b7")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k9_cat_2 :::"["::: ) (Set "(" (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k9_cat_2 :::"]"::: ) ) "," (Set "(" (Set "(" ($#k11_funct_5 :::"curry"::: ) (Set (Var "s")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_tarski :::"]"::: ) )))) ")" ))))); theorem :: ISOCAT_2:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "holds" (Bool (Set ($#k6_nattra_1 :::"id"::: ) (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_isocat_2 :::"export"::: ) (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "F")) ")" ))))) ; theorem :: ISOCAT_2:25 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F3")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t2")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "holds" (Bool (Set ($#k6_isocat_2 :::"export"::: ) (Set "(" (Set (Var "t2")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t1")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_isocat_2 :::"export"::: ) (Set (Var "t2")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" ($#k6_isocat_2 :::"export"::: ) (Set (Var "t1")) ")" ))))))) ; theorem :: ISOCAT_2:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set ($#k6_isocat_2 :::"export"::: ) (Set (Var "t1"))) ($#r2_funct_2 :::"="::: ) (Set ($#k6_isocat_2 :::"export"::: ) (Set (Var "t2"))))) "holds" (Bool (Set (Var "t1")) ($#r2_funct_2 :::"="::: ) (Set (Var "t2")))))) ; theorem :: ISOCAT_2:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ) (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Set (Var "G")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F"))))))) ; theorem :: ISOCAT_2:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1"))) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2"))))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1"))) "," (Set ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2"))) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool "ex" (Set (Var "u")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Set (Var "t")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_isocat_2 :::"export"::: ) (Set (Var "u"))))) ")" )))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); func :::"export"::: "(" "A" "," "B" "," "C" ")" -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set ($#k8_cat_2 :::"[:"::: ) "A" "," "B" ($#k8_cat_2 :::":]"::: ) ) "," "C" ")" ) "," (Set ($#k11_nattra_1 :::"Functors"::: ) "(" "A" "," (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" "B" "," "C" ")" ")" ) ")" ) means :: ISOCAT_2:def 6 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) "A" "," "B" ($#k8_cat_2 :::":]"::: ) ) "," "C" "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1")) ")" ) "," (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_isocat_2 :::"export"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) )))); end; :: deftheorem defines :::"export"::: ISOCAT_2:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b4")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) ")" ) "," (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_isocat_2 :::"export"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )) "iff" (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F1")) ")" ) "," (Set "(" ($#k5_isocat_2 :::"export"::: ) (Set (Var "F2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_isocat_2 :::"export"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) )))) ")" ))); registrationlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); cluster (Set ($#k7_isocat_2 :::"export"::: ) "(" "A" "," "B" "," "C" ")" ) -> ($#v12_cat_1 :::"isomorphic"::: ) ; end; theorem :: ISOCAT_2:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) ")" ) ($#r1_isocat_1 :::"~="::: ) (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ))) ; begin theorem :: ISOCAT_2:30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_relat_1 :::"*"::: ) (Set (Var "t")))))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "C")); :: original: :::"<:"::: redefine func :::"<:":::"F" "," "G":::":>"::: -> ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," (Set ($#k8_cat_2 :::"[:"::: ) "B" "," "C" ($#k8_cat_2 :::":]"::: ) ); end; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Const "B")) "," (Set (Const "C")) ($#k8_cat_2 :::":]"::: ) ); func :::"Pr1"::: "F" -> ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B" equals :: ISOCAT_2:def 7 (Set (Set "(" ($#k14_cat_2 :::"pr1"::: ) "(" "B" "," "C" ")" ")" ) ($#k9_cat_1 :::"*"::: ) "F"); func :::"Pr2"::: "F" -> ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "C" equals :: ISOCAT_2:def 8 (Set (Set "(" ($#k15_cat_2 :::"pr2"::: ) "(" "B" "," "C" ")" ")" ) ($#k9_cat_1 :::"*"::: ) "F"); end; :: deftheorem defines :::"Pr1"::: ISOCAT_2:def 7 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "holds" (Bool (Set ($#k9_isocat_2 :::"Pr1"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_cat_2 :::"pr1"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")))))); :: deftheorem defines :::"Pr2"::: ISOCAT_2:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "holds" (Bool (Set ($#k10_isocat_2 :::"Pr2"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_cat_2 :::"pr2"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")))))); theorem :: ISOCAT_2:31 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k9_isocat_2 :::"Pr1"::: ) (Set ($#k8_isocat_2 :::"<:"::: ) (Set (Var "F")) "," (Set (Var "G")) ($#k8_isocat_2 :::":>"::: ) )) ($#r2_funct_2 :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k10_isocat_2 :::"Pr2"::: ) (Set ($#k8_isocat_2 :::"<:"::: ) (Set (Var "F")) "," (Set (Var "G")) ($#k8_isocat_2 :::":>"::: ) )) ($#r2_funct_2 :::"="::: ) (Set (Var "G"))) ")" )))) ; theorem :: ISOCAT_2:32 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "st" (Bool (Bool (Set ($#k9_isocat_2 :::"Pr1"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_isocat_2 :::"Pr1"::: ) (Set (Var "G")))) & (Bool (Set ($#k10_isocat_2 :::"Pr2"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k10_isocat_2 :::"Pr2"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "F")) ($#r2_funct_2 :::"="::: ) (Set (Var "G"))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Const "B")) "," (Set (Const "C")) ($#k8_cat_2 :::":]"::: ) ); let "t" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); func :::"Pr1"::: "t" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set ($#k9_isocat_2 :::"Pr1"::: ) "F1") "," (Set ($#k9_isocat_2 :::"Pr1"::: ) "F2") equals :: ISOCAT_2:def 9 (Set (Set "(" ($#k14_cat_2 :::"pr1"::: ) "(" "B" "," "C" ")" ")" ) ($#k4_isocat_1 :::"*"::: ) "t"); func :::"Pr2"::: "t" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set ($#k10_isocat_2 :::"Pr2"::: ) "F1") "," (Set ($#k10_isocat_2 :::"Pr2"::: ) "F2") equals :: ISOCAT_2:def 10 (Set (Set "(" ($#k15_cat_2 :::"pr2"::: ) "(" "B" "," "C" ")" ")" ) ($#k4_isocat_1 :::"*"::: ) "t"); end; :: deftheorem defines :::"Pr1"::: ISOCAT_2:def 9 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set ($#k11_isocat_2 :::"Pr1"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k14_cat_2 :::"pr1"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ($#k4_isocat_1 :::"*"::: ) (Set (Var "t"))))))); :: deftheorem defines :::"Pr2"::: ISOCAT_2:def 10 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set ($#k12_isocat_2 :::"Pr2"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_cat_2 :::"pr2"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ($#k4_isocat_1 :::"*"::: ) (Set (Var "t"))))))); theorem :: ISOCAT_2:33 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set ($#k11_isocat_2 :::"Pr1"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set ($#k11_isocat_2 :::"Pr1"::: ) (Set (Var "t")))) & (Bool (Set ($#k12_isocat_2 :::"Pr2"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set ($#k12_isocat_2 :::"Pr2"::: ) (Set (Var "t"))))) "holds" (Bool (Set (Var "s")) ($#r2_funct_2 :::"="::: ) (Set (Var "t"))))))) ; theorem :: ISOCAT_2:34 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "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 ($#k8_isocat_2 :::"<:"::: ) (Set (Var "F")) "," (Set (Var "G")) ($#k8_isocat_2 :::":>"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cat_2 :::"["::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ($#k10_cat_2 :::"]"::: ) ))))))) ; theorem :: ISOCAT_2:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set ($#k8_isocat_2 :::"<:"::: ) (Set (Var "F")) "," (Set (Var "G")) ($#k8_isocat_2 :::":>"::: ) ) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_2 :::"["::: ) (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "G")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k9_cat_2 :::"]"::: ) )))))) ; theorem :: ISOCAT_2:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F2")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set ($#k8_isocat_2 :::"<:"::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k8_isocat_2 :::":>"::: ) ) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set ($#k8_isocat_2 :::"<:"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k8_isocat_2 :::":>"::: ) ))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F1", "G1" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "F2", "G2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "C")); assume (Bool "(" (Bool (Set (Const "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "G1"))) & (Bool (Set (Const "F2")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "G2"))) ")" ) ; let "t1" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "G1")); let "t2" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F2")) "," (Set (Const "G2")); func :::"<:":::"t1" "," "t2":::":>"::: -> ($#m1_nattra_1 :::"transformation"::: ) "of" (Set ($#k8_isocat_2 :::"<:"::: ) "F1" "," "F2" ($#k8_isocat_2 :::":>"::: ) ) "," (Set ($#k8_isocat_2 :::"<:"::: ) "G1" "," "G2" ($#k8_isocat_2 :::":>"::: ) ) equals :: ISOCAT_2:def 11 (Set ($#k14_funct_3 :::"<:"::: ) "t1" "," "t2" ($#k14_funct_3 :::":>"::: ) ); end; :: deftheorem defines :::"<:"::: ISOCAT_2:def 11 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F2")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "G1")) (Bool "for" (Set (Var "t2")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "G2")) "holds" (Bool (Set ($#k13_isocat_2 :::"<:"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k13_isocat_2 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k14_funct_3 :::"<:"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k14_funct_3 :::":>"::: ) ))))))); theorem :: ISOCAT_2:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F2")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "G1")) (Bool "for" (Set (Var "t2")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "G2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set ($#k13_isocat_2 :::"<:"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k13_isocat_2 :::":>"::: ) ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cat_2 :::"["::: ) (Set "(" (Set (Var "t1")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "t2")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k10_cat_2 :::"]"::: ) )))))))) ; theorem :: ISOCAT_2:38 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F2")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set ($#k8_isocat_2 :::"<:"::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k8_isocat_2 :::":>"::: ) ) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set ($#k8_isocat_2 :::"<:"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k8_isocat_2 :::":>"::: ) ))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F1", "G1" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "F2", "G2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "C")); assume (Bool "(" (Bool (Set (Const "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "G1"))) & (Bool (Set (Const "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "G2"))) ")" ) ; let "t1" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "G1")); let "t2" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F2")) "," (Set (Const "G2")); func :::"<:":::"t1" "," "t2":::":>"::: -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set ($#k8_isocat_2 :::"<:"::: ) "F1" "," "F2" ($#k8_isocat_2 :::":>"::: ) ) "," (Set ($#k8_isocat_2 :::"<:"::: ) "G1" "," "G2" ($#k8_isocat_2 :::":>"::: ) ) equals :: ISOCAT_2:def 12 (Set ($#k13_isocat_2 :::"<:"::: ) "t1" "," "t2" ($#k13_isocat_2 :::":>"::: ) ); end; :: deftheorem defines :::"<:"::: ISOCAT_2:def 12 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F2")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "G1")) (Bool "for" (Set (Var "t2")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "G2")) "holds" (Bool (Set ($#k14_isocat_2 :::"<:"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k14_isocat_2 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k13_isocat_2 :::"<:"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k13_isocat_2 :::":>"::: ) ))))))); theorem :: ISOCAT_2:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "G1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F2")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G1"))) & (Bool (Set (Var "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "G1")) (Bool "for" (Set (Var "t2")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "G2")) "holds" (Bool "(" (Bool (Set ($#k11_isocat_2 :::"Pr1"::: ) (Set ($#k14_isocat_2 :::"<:"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k14_isocat_2 :::":>"::: ) )) ($#r2_funct_2 :::"="::: ) (Set (Var "t1"))) & (Bool (Set ($#k12_isocat_2 :::"Pr2"::: ) (Set ($#k14_isocat_2 :::"<:"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k14_isocat_2 :::":>"::: ) )) ($#r2_funct_2 :::"="::: ) (Set (Var "t2"))) ")" )))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); func :::"distribute"::: "(" "A" "," "B" "," "C" ")" -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k11_nattra_1 :::"Functors"::: ) "(" "A" "," (Set ($#k8_cat_2 :::"[:"::: ) "B" "," "C" ($#k8_cat_2 :::":]"::: ) ) ")" ) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" "A" "," "B" ")" ")" ) "," (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" "A" "," "C" ")" ")" ) ($#k8_cat_2 :::":]"::: ) ) means :: ISOCAT_2:def 13 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," (Set ($#k8_cat_2 :::"[:"::: ) "B" "," "C" ($#k8_cat_2 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k9_isocat_2 :::"Pr1"::: ) (Set (Var "F1")) ")" ) "," (Set "(" ($#k9_isocat_2 :::"Pr1"::: ) (Set (Var "F2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k11_isocat_2 :::"Pr1"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k10_isocat_2 :::"Pr2"::: ) (Set (Var "F1")) ")" ) "," (Set "(" ($#k10_isocat_2 :::"Pr2"::: ) (Set (Var "F2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k12_isocat_2 :::"Pr2"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))); end; :: deftheorem defines :::"distribute"::: ISOCAT_2:def 13 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b4")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) ")" ) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "," (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ($#k8_cat_2 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k15_isocat_2 :::"distribute"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) ")" )) "iff" (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k9_isocat_2 :::"Pr1"::: ) (Set (Var "F1")) ")" ) "," (Set "(" ($#k9_isocat_2 :::"Pr1"::: ) (Set (Var "F2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k11_isocat_2 :::"Pr1"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k10_isocat_2 :::"Pr2"::: ) (Set (Var "F1")) ")" ) "," (Set "(" ($#k10_isocat_2 :::"Pr2"::: ) (Set (Var "F2")) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k12_isocat_2 :::"Pr2"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )))) ")" ))); registrationlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); cluster (Set ($#k15_isocat_2 :::"distribute"::: ) "(" "A" "," "B" "," "C" ")" ) -> ($#v12_cat_1 :::"isomorphic"::: ) ; end; theorem :: ISOCAT_2:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) ")" ) ($#r1_isocat_1 :::"~="::: ) (Set ($#k8_cat_2 :::"[:"::: ) (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "," (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ($#k8_cat_2 :::":]"::: ) ))) ;