:: CAT_3 semantic presentation begin scheme :: CAT_3:sch 1 LambdaIdx{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )))) proof end; theorem :: CAT_3:1 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "F1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Var "F1")) ($#r2_funct_2 :::"="::: ) (Set (Var "F2")))))) ; scheme :: CAT_3:sch 2 FuncIdxcorrectness{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "(" (Bool "ex" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )))) & (Bool "(" "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "F1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "F2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Var "F1")) ($#r2_funct_2 :::"="::: ) (Set (Var "F2"))) ")" ) ")" ) proof end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::".-->"::: redefine func "x" :::".-->"::: "a" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) "," "A"; end; theorem :: CAT_3:2 (Bool "for" (Set (Var "I")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "a")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ; theorem :: CAT_3:3 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ) ($#k10_funct_2 :::"/."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ) ($#k10_funct_2 :::"/."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" )))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))); func :::"doms"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") means :: CAT_3:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))); func :::"cods"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") means :: CAT_3:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"doms"::: CAT_3:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))) ")" ))))); :: deftheorem defines :::"cods"::: CAT_3:def 2 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))) ")" ))))); theorem :: CAT_3:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (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 ($#k2_cat_3 :::"doms"::: ) (Set "(" (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )))))) ; theorem :: CAT_3:5 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (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 ($#k3_cat_3 :::"cods"::: ) (Set "(" (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" )))))) ; theorem :: CAT_3:6 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "p2")) ")" ) ")" ))))) ; theorem :: CAT_3:7 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "p2")) ")" ) ")" ))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))); func "F" :::"opp"::: -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" "C" ($#k2_oppcat_1 :::"opp"::: ) ")" )) means :: CAT_3:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ))); end; :: deftheorem defines :::"opp"::: CAT_3:def 3 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_cat_3 :::"opp"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k5_oppcat_1 :::"opp"::: ) ))) ")" ))))); theorem :: CAT_3:8 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (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 "(" (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ($#k4_cat_3 :::"opp"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" )))))) ; theorem :: CAT_3:9 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" ) ($#k4_cat_3 :::"opp"::: ) ) ($#r2_funct_2 :::"="::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" (Set (Var "p1")) ($#k5_oppcat_1 :::"opp"::: ) ")" ) "," (Set "(" (Set (Var "p2")) ($#k5_oppcat_1 :::"opp"::: ) ")" ) ")" ))))) ; theorem :: CAT_3:10 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_cat_3 :::"opp"::: ) ")" ) ($#k4_cat_3 :::"opp"::: ) ) ($#r1_funct_2 :::"="::: ) (Set (Var "F")))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Const "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )); func :::"opp"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") means :: CAT_3:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_oppcat_1 :::"opp"::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"opp"::: CAT_3:def 4 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_cat_3 :::"opp"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_oppcat_1 :::"opp"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))) ")" ))))); theorem :: CAT_3:11 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (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 ($#k5_cat_3 :::"opp"::: ) (Set "(" (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "f")) ")" )))))) ; theorem :: CAT_3:12 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool (Set ($#k5_cat_3 :::"opp"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k6_oppcat_1 :::"opp"::: ) (Set (Var "p2")) ")" ) ")" ))))) ; theorem :: CAT_3:13 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set ($#k5_cat_3 :::"opp"::: ) (Set "(" (Set (Var "F")) ($#k4_cat_3 :::"opp"::: ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "F")))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))); let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); func "F" :::"*"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") means :: CAT_3:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k1_cat_1 :::"(*)"::: ) "f"))); func "f" :::"*"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") means :: CAT_3:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_cat_1 :::"(*)"::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"*"::: CAT_3:def 5 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k6_cat_3 :::"*"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))) ")" )))))); :: deftheorem defines :::"*"::: CAT_3:def 6 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))) ")" )))))); theorem :: CAT_3:14 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" ) ($#k6_cat_3 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" (Set (Var "p1")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "p2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" ) ")" ))))) ; theorem :: CAT_3:15 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "p1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "p2")) ")" ) ")" ))))) ; theorem :: CAT_3:16 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set "(" (Set (Var "F")) ($#k6_cat_3 :::"*"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set "(" (Set (Var "F")) ($#k6_cat_3 :::"*"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F")))) ")" ))))) ; theorem :: CAT_3:17 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "(" (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set "(" (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set (Var "F")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F")))) & (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set "(" (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set (Var "F")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ))) ")" ))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))); func "F" :::""*""::: "G" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") means :: CAT_3:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" "G" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::""*""::: CAT_3:def 7 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_cat_3 :::""*""::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "G")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )))) ")" )))); theorem :: CAT_3:18 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "G"))))) "holds" (Bool "(" (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set "(" (Set (Var "F")) ($#k8_cat_3 :::""*""::: ) (Set (Var "G")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "G")))) & (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set "(" (Set (Var "F")) ($#k8_cat_3 :::""*""::: ) (Set (Var "G")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F")))) ")" )))) ; theorem :: CAT_3:19 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" ) ($#k8_cat_3 :::""*""::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "q1")) "," (Set (Var "q2")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" (Set (Var "p1")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "q1")) ")" ) "," (Set "(" (Set (Var "p2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "q2")) ")" ) ")" ))))) ; theorem :: CAT_3:20 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Set (Var "F")) ($#k6_cat_3 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k8_cat_3 :::""*""::: ) (Set "(" (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: CAT_3:21 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ($#k8_cat_3 :::""*""::: ) (Set (Var "F")))))))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "IT" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); attr "IT" is :::"retraction"::: means :: CAT_3:def 8 (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," "b" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "b" "," "a" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," "a" "st" (Bool (Set "IT" ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "b"))) ")" ); attr "IT" is :::"coretraction"::: means :: CAT_3:def 9 (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," "b" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "b" "," "a" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," "a" "st" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) "IT") ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "a"))) ")" ); end; :: deftheorem defines :::"retraction"::: CAT_3:def 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")) (Bool "for" (Set (Var "IT")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_cat_3 :::"retraction"::: ) ) "iff" (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 "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool (Set (Set (Var "IT")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b"))))) ")" ) ")" )))); :: deftheorem defines :::"coretraction"::: CAT_3:def 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 (Var "C")) (Bool "for" (Set (Var "IT")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_cat_3 :::"coretraction"::: ) ) "iff" (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 "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "IT"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))))) ")" ) ")" )))); theorem :: CAT_3: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")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_cat_3 :::"retraction"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) )))) ; theorem :: CAT_3:23 (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")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v7_cat_1 :::"monic"::: ) )))) ; theorem :: CAT_3:24 (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 (Var "f")) "is" ($#v1_cat_3 :::"retraction"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_cat_3 :::"retraction"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#v1_cat_3 :::"retraction"::: ) ))))) ; theorem :: CAT_3:25 (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 (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_cat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#v2_cat_3 :::"coretraction"::: ) ))))) ; theorem :: CAT_3:26 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (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")) (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 "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#v1_cat_3 :::"retraction"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v1_cat_3 :::"retraction"::: ) ))))) ; theorem :: CAT_3:27 (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 "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#v2_cat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) ))))) ; theorem :: CAT_3:28 (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")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_cat_3 :::"retraction"::: ) ) & (Bool (Set (Var "f")) "is" ($#v7_cat_1 :::"monic"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )))) ; theorem :: CAT_3:29 (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")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) ) & (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )))) ; theorem :: CAT_3:30 (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 (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_cat_3 :::"retraction"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) ) ")" ) ")" )))) ; 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 "D" be ($#l1_cat_1 :::"Category":::); let "T" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); func "T" :::"/."::: "f" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "T" ($#k8_cat_1 :::"."::: ) "a") "," (Set "T" ($#k8_cat_1 :::"."::: ) "b") equals :: CAT_3:def 10 (Set "T" ($#k3_funct_2 :::"."::: ) "f"); end; :: deftheorem defines :::"/."::: CAT_3:def 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 "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "T")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))))))))); theorem :: CAT_3:31 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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")) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_cat_3 :::"retraction"::: ) )) "holds" (Bool (Set (Set (Var "T")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f"))) "is" ($#v1_cat_3 :::"retraction"::: ) ))))) ; theorem :: CAT_3:32 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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")) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Set (Var "T")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f"))) "is" ($#v2_cat_3 :::"coretraction"::: ) ))))) ; theorem :: CAT_3:33 (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 (Var "f")) "is" ($#v1_cat_3 :::"retraction"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ) "is" ($#v2_cat_3 :::"coretraction"::: ) ) ")" )))) ; theorem :: CAT_3:34 (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 (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) ) "iff" (Bool (Set (Set (Var "f")) ($#k7_oppcat_1 :::"opp"::: ) ) "is" ($#v1_cat_3 :::"retraction"::: ) ) ")" )))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); assume (Bool (Set (Const "b")) "is" ($#v10_cat_1 :::"terminal"::: ) ) ; func :::"term"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," "b" means :: CAT_3:def 11 (Bool verum); end; :: deftheorem defines :::"term"::: CAT_3:def 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 (Var "C")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k10_cat_3 :::"term"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool verum) ")" )))); theorem :: CAT_3:35 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k10_cat_3 :::"term"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k10_cat_3 :::"term"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: CAT_3:36 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v10_cat_1 :::"terminal"::: ) ) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k10_cat_3 :::"term"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: CAT_3:37 (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")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool (Set ($#k10_cat_3 :::"term"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); assume (Bool (Set (Const "a")) "is" ($#v11_cat_1 :::"initial"::: ) ) ; func :::"init"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," "b" means :: CAT_3:def 12 (Bool verum); end; :: deftheorem defines :::"init"::: CAT_3:def 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 (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_cat_3 :::"init"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool verum) ")" )))); theorem :: CAT_3:38 (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 (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k11_cat_3 :::"init"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k11_cat_3 :::"init"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: CAT_3:39 (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_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k11_cat_3 :::"init"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: CAT_3:40 (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")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool (Set ($#k11_cat_3 :::"init"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "I" be ($#m1_hidden :::"set"::: ) ; mode :::"Projections_family"::: "of" "a" "," "I" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") means :: CAT_3:def 13 (Bool (Set ($#k2_cat_3 :::"doms"::: ) it) ($#r2_funct_2 :::"="::: ) (Set "I" ($#k8_funcop_1 :::"-->"::: ) "a")); end; :: deftheorem defines :::"Projections_family"::: CAT_3:def 13 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I"))) "iff" (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "b4"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "a")))) ")" ))))); theorem :: CAT_3:41 (Bool "for" (Set (Var "I")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))))))) ; theorem :: CAT_3:42 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Var "F")) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: CAT_3:43 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "y")) ($#k1_cat_3 :::".-->"::: ) (Set (Var "f"))) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: CAT_3:44 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )))))) ; theorem :: CAT_3:45 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "F")) ($#k6_cat_3 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) "," (Set (Var "I")))))))) ; theorem :: CAT_3:46 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) (Bool "for" (Set (Var "G")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "F")) ($#k8_cat_3 :::""*""::: ) (Set (Var "G"))) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")))))))) ; theorem :: CAT_3:47 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) "," (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" ) ($#k7_cat_3 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k4_cat_3 :::"opp"::: ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_cat_3 :::"*"::: ) (Set (Var "f")) ")" ) ($#k4_cat_3 :::"opp"::: ) )))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))); pred "a" :::"is_a_product_wrt"::: "F" means :: CAT_3:def 14 (Bool "(" (Bool "F" "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" "a" "," "I") & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" (Bool "for" (Set (Var "F9")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "b")) "," "I" "st" (Bool (Bool (Set ($#k3_cat_3 :::"cods"::: ) "F") ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F9"))))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," "a" ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," "a" ")" ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F9")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_a_product_wrt"::: CAT_3:def 14 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I"))) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F9")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "b")) "," (Set (Var "I")) "st" (Bool (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F9"))))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F9")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ) ")" ))))); theorem :: CAT_3:48 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I")) (Bool "for" (Set (Var "F9")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "d")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "c")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Var "d")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F9"))) & (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F9"))))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_cat_1 :::"are_isomorphic"::: ) )))))) ; theorem :: CAT_3:49 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "c")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x1")) ")" ) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "f")) "is" ($#v1_cat_3 :::"retraction"::: ) )))))))) ; theorem :: CAT_3:50 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) ) ")" )))) ; theorem :: CAT_3:51 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (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_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "a")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Var "b")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Set (Var "F")) ($#k6_cat_3 :::"*"::: ) (Set (Var "f"))))))))) ; theorem :: CAT_3:52 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (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 (Var "a")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Set (Var "y")) ($#k1_cat_3 :::".-->"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )))))) ; theorem :: CAT_3:53 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "a")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )) "is" ($#v10_cat_1 :::"terminal"::: ) ) ")" )) "holds" (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) ))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "p1", "p2" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); pred "c" :::"is_a_product_wrt"::: "p1" "," "p2" means :: CAT_3:def 15 (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) "p1") ($#r1_hidden :::"="::: ) "c") & (Bool (Set ($#k3_graph_1 :::"dom"::: ) "p2") ($#r1_hidden :::"="::: ) "c") & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) "p1" ")" ) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) "p2" ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," "c" ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," "c" ")" ))) "holds" (Bool "(" (Bool "(" (Bool (Set "p1" ($#k1_cat_1 :::"(*)"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set "p2" ($#k1_cat_1 :::"(*)"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_a_product_wrt"::: CAT_3:def 15 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "p1")) ")" ) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "p2")) ")" ) ")" ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "p1")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "p2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ) ")" )))); theorem :: CAT_3:54 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool (Set (Var "c")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )) ")" ))))) ; theorem :: CAT_3:55 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (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 "c")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "p1")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "a")) (Bool "for" (Set (Var "p2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "a")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "b")) (Bool "ex" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "c")) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "c")) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "p1")) ($#k5_cat_1 :::"*"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "p2")) ($#k5_cat_1 :::"*"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" )))) ")" ) ")" )) ")" ))))) ; theorem :: CAT_3:56 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "q1")) "," (Set (Var "q2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "d")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "q1")) "," (Set (Var "q2"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "q1")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "q2"))))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_cat_1 :::"are_isomorphic"::: ) )))) ; theorem :: CAT_3:57 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "a")) (Bool "for" (Set (Var "p2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (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 "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "p1")) "is" ($#v1_cat_3 :::"retraction"::: ) ) & (Bool (Set (Var "p2")) "is" ($#v1_cat_3 :::"retraction"::: ) ) ")" ))))) ; theorem :: CAT_3:58 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c")) ")" )) & (Bool (Set (Set (Var "p1")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Set (Var "p2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "p2")))) "holds" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "c"))))))) ; theorem :: CAT_3:59 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "d")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Var "d")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Set (Var "p1")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) "," (Set (Set (Var "p2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")))))))) ; theorem :: CAT_3:60 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p2"))) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool (Set (Var "c")) "," (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p1"))) ($#r1_cat_1 :::"are_isomorphic"::: ) )))) ; theorem :: CAT_3:61 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p1"))) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool (Set (Var "c")) "," (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p2"))) ($#r1_cat_1 :::"are_isomorphic"::: ) )))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "I" be ($#m1_hidden :::"set"::: ) ; mode :::"Injections_family"::: "of" "c" "," "I" -> ($#m1_subset_1 :::"Function":::) "of" "I" "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") means :: CAT_3:def 16 (Bool (Set ($#k3_cat_3 :::"cods"::: ) it) ($#r2_funct_2 :::"="::: ) (Set "I" ($#k8_funcop_1 :::"-->"::: ) "c")); end; :: deftheorem defines :::"Injections_family"::: CAT_3:def 16 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I"))) "iff" (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "b4"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "c")))) ")" ))))); theorem :: CAT_3:62 (Bool "for" (Set (Var "I")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "c"))))))) ; theorem :: CAT_3:63 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool (Set (Var "F")) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "a")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: CAT_3:64 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set (Set (Var "y")) ($#k1_cat_3 :::".-->"::: ) (Set (Var "f"))) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "a")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: CAT_3:65 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "holds" (Bool (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "c")) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )))))) ; theorem :: CAT_3:66 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "b")) "," (Set (Var "I")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set (Var "F"))) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) "," (Set (Var "I")))))))) ; theorem :: CAT_3:67 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "b")) "," (Set (Var "I")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "F")) ($#k8_cat_3 :::""*""::: ) (Set (Var "G"))) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "b")) "," (Set (Var "I")))))))) ; theorem :: CAT_3:68 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I"))) "iff" (Bool (Set (Set (Var "F")) ($#k4_cat_3 :::"opp"::: ) ) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ) "," (Set (Var "I"))) ")" ))))) ; theorem :: CAT_3:69 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I"))) "iff" (Bool (Set ($#k5_cat_3 :::"opp"::: ) (Set (Var "F"))) "is" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set ($#k4_oppcat_1 :::"opp"::: ) (Set (Var "c"))) "," (Set (Var "I"))) ")" ))))) ; theorem :: CAT_3:70 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) "," (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k4_cat_3 :::"opp"::: ) ")" ) ($#k6_cat_3 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k5_oppcat_1 :::"opp"::: ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set (Var "F")) ")" ) ($#k4_cat_3 :::"opp"::: ) )))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "I" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))); pred "c" :::"is_a_coproduct_wrt"::: "F" means :: CAT_3:def 17 (Bool "(" (Bool "F" "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" "c" "," "I") & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" (Bool "for" (Set (Var "F9")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "d")) "," "I" "st" (Bool (Bool (Set ($#k2_cat_3 :::"doms"::: ) "F") ($#r2_funct_2 :::"="::: ) (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F9"))))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" "c" "," (Set (Var "d")) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" "c" "," (Set (Var "d")) ")" ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set (Set (Var "k")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" "F" ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F9")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_a_coproduct_wrt"::: CAT_3:def 17 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F"))) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F9")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "d")) "," (Set (Var "I")) "st" (Bool (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F9"))))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "k")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F9")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ) ")" ))))); theorem :: CAT_3:71 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F"))) "iff" (Bool (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Set (Var "F")) ($#k4_cat_3 :::"opp"::: ) )) ")" ))))) ; theorem :: CAT_3:72 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I")) (Bool "for" (Set (Var "F9")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "d")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "c")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Var "d")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F9"))) & (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F9"))))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_cat_1 :::"are_isomorphic"::: ) )))))) ; theorem :: CAT_3:73 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "c")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "c")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x1")) ")" ) ")" ) "," (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x2")) ")" ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "f")) "is" ($#v2_cat_3 :::"coretraction"::: ) )))))))) ; theorem :: CAT_3:74 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (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")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "a")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Var "b")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Set (Var "f")) ($#k7_cat_3 :::"*"::: ) (Set (Var "F"))))))))) ; theorem :: CAT_3:75 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "a")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F"))) "iff" (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ) ")" )))) ; theorem :: CAT_3:76 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (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 (Var "a")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Set (Var "y")) ($#k1_cat_3 :::".-->"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )))))) ; theorem :: CAT_3:77 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool (Bool (Set (Var "a")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")) ")" )) "is" ($#v11_cat_1 :::"initial"::: ) ) ")" )) "holds" (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "i1", "i2" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); pred "c" :::"is_a_coproduct_wrt"::: "i1" "," "i2" means :: CAT_3:def 18 (Bool "(" (Bool (Set ($#k4_graph_1 :::"cod"::: ) "i1") ($#r1_hidden :::"="::: ) "c") & (Bool (Set ($#k4_graph_1 :::"cod"::: ) "i2") ($#r1_hidden :::"="::: ) "c") & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) "i1" ")" ) "," (Set (Var "d")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) "i2" ")" ) "," (Set (Var "d")) ")" ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" "c" "," (Set (Var "d")) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" "c" "," (Set (Var "d")) ")" ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "k")) ($#k1_cat_1 :::"(*)"::: ) "i1") ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "k")) ($#k1_cat_1 :::"(*)"::: ) "i2") ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"is_a_coproduct_wrt"::: CAT_3:def 18 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) "iff" (Bool "(" (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "i2"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "i1")) ")" ) "," (Set (Var "d")) ")" )) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "i2")) ")" ) "," (Set (Var "d")) ")" ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "k")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "k")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i2"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" ) ")" ) ")" ))) ")" ) ")" ) ")" )))); theorem :: CAT_3:78 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) "iff" (Bool (Set (Set (Var "c")) ($#k3_oppcat_1 :::"opp"::: ) ) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Set (Var "p1")) ($#k5_oppcat_1 :::"opp"::: ) ) "," (Set (Set (Var "p2")) ($#k5_oppcat_1 :::"opp"::: ) )) ")" )))) ; theorem :: CAT_3:79 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) "iff" (Bool (Set (Var "c")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set (Var "i1")) "," (Set (Var "i2")) ")" )) ")" ))))) ; theorem :: CAT_3:80 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "j1")) "," (Set (Var "j2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "d")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "j1")) "," (Set (Var "j2"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "j1")))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i2"))) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "j2"))))) "holds" (Bool (Set (Var "c")) "," (Set (Var "d")) ($#r1_cat_1 :::"are_isomorphic"::: ) )))) ; theorem :: CAT_3:81 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (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 "c")) ")" ) ($#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 "i1")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) (Bool "for" (Set (Var "i2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "d")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "d")) (Bool "ex" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool "for" (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "holds" (Bool "(" (Bool "(" (Bool (Set (Set (Var "k")) ($#k5_cat_1 :::"*"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "k")) ($#k5_cat_1 :::"*"::: ) (Set (Var "i2"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) "iff" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) ")" )))) ")" ) ")" )) ")" ))))) ; theorem :: CAT_3:82 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) (Bool "for" (Set (Var "i2")) "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 "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) & (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 "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "i1")) "is" ($#v2_cat_3 :::"coretraction"::: ) ) & (Bool (Set (Var "i2")) "is" ($#v2_cat_3 :::"coretraction"::: ) ) ")" ))))) ; theorem :: CAT_3:83 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c")) ")" )) & (Bool (Set (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set (Var "i1"))) & (Bool (Set (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i2"))) ($#r1_hidden :::"="::: ) (Set (Var "i2")))) "holds" (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "c"))))))) ; theorem :: CAT_3:84 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Var "d")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i1"))) "," (Set (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i2")))))))) ; theorem :: CAT_3:85 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i2"))) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i1"))) "," (Set (Var "c")) ($#r1_cat_1 :::"are_isomorphic"::: ) )))) ; theorem :: CAT_3:86 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i1"))) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i2"))) "," (Set (Var "c")) ($#r1_cat_1 :::"are_isomorphic"::: ) )))) ;