:: ALTCAT_3 semantic presentation begin definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); let "B" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o2")) "," (Set (Const "o1")); pred "A" :::"is_left_inverse_of"::: "B" means :: ALTCAT_3:def 1 (Bool (Set "A" ($#k5_altcat_1 :::"*"::: ) "B") ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) "o2")); end; :: deftheorem defines :::"is_left_inverse_of"::: ALTCAT_3:def 1 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o1")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r1_altcat_3 :::"is_left_inverse_of"::: ) (Set (Var "B"))) "iff" (Bool (Set (Set (Var "A")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o2")))) ")" ))))); notationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); let "B" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o2")) "," (Set (Const "o1")); synonym "B" :::"is_right_inverse_of"::: "A" for "A" :::"is_left_inverse_of"::: "B"; end; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); attr "A" is :::"retraction"::: means :: ALTCAT_3:def 2 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "o2" "," "o1" "st" (Bool (Set (Var "B")) ($#r1_altcat_3 :::"is_right_inverse_of"::: ) "A")); end; :: deftheorem defines :::"retraction"::: ALTCAT_3:def 2 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o1")) "st" (Bool (Set (Var "B")) ($#r1_altcat_3 :::"is_right_inverse_of"::: ) (Set (Var "A")))) ")" )))); definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); attr "A" is :::"coretraction"::: means :: ALTCAT_3:def 3 (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "o2" "," "o1" "st" (Bool (Set (Var "B")) ($#r1_altcat_3 :::"is_left_inverse_of"::: ) "A")); end; :: deftheorem defines :::"coretraction"::: ALTCAT_3:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) ) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o1")) "st" (Bool (Set (Var "B")) ($#r1_altcat_3 :::"is_left_inverse_of"::: ) (Set (Var "A")))) ")" )))); theorem :: ALTCAT_3:1 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o"))) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o"))) "is" ($#v2_altcat_3 :::"coretraction"::: ) ) ")" ))) ; definitionlet "C" be ($#l2_altcat_1 :::"category":::); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); assume that (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Const "o1")) "," (Set (Const "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) and (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Const "o2")) "," (Set (Const "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); assume (Bool "(" (Bool (Set (Const "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Const "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) ) ")" ) ; func "A" :::"""::: -> ($#m1_subset_1 :::"Morphism":::) "of" "o2" "," "o1" means :: ALTCAT_3:def 4 (Bool "(" (Bool it ($#r1_altcat_3 :::"is_left_inverse_of"::: ) "A") & (Bool it ($#r1_altcat_3 :::"is_right_inverse_of"::: ) "A") ")" ); end; :: deftheorem defines :::"""::: ALTCAT_3:def 4 : (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) )) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o1")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k1_altcat_3 :::"""::: ) )) "iff" (Bool "(" (Bool (Set (Var "b5")) ($#r1_altcat_3 :::"is_left_inverse_of"::: ) (Set (Var "A"))) & (Bool (Set (Var "b5")) ($#r1_altcat_3 :::"is_right_inverse_of"::: ) (Set (Var "A"))) ")" ) ")" ))))); theorem :: ALTCAT_3:2 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_altcat_3 :::"""::: ) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o1")))) & (Bool (Set (Set (Var "A")) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k1_altcat_3 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o2")))) ")" )))) ; theorem :: ALTCAT_3:3 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "A")) ($#k1_altcat_3 :::"""::: ) ")" ) ($#k1_altcat_3 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "A")))))) ; theorem :: ALTCAT_3:4 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o")) ")" ) ($#k1_altcat_3 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o")))))) ; definitionlet "C" be ($#l2_altcat_1 :::"category":::); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); attr "A" is :::"iso"::: means :: ALTCAT_3:def 5 (Bool "(" (Bool (Set "A" ($#k5_altcat_1 :::"*"::: ) (Set "(" "A" ($#k1_altcat_3 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) "o2")) & (Bool (Set (Set "(" "A" ($#k1_altcat_3 :::"""::: ) ")" ) ($#k5_altcat_1 :::"*"::: ) "A") ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) "o1")) ")" ); end; :: deftheorem defines :::"iso"::: ALTCAT_3:def 5 : (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) ) "iff" (Bool "(" (Bool (Set (Set (Var "A")) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "A")) ($#k1_altcat_3 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o2")))) & (Bool (Set (Set "(" (Set (Var "A")) ($#k1_altcat_3 :::"""::: ) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o1")))) ")" ) ")" )))); theorem :: ALTCAT_3:5 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) ) ")" )))) ; theorem :: ALTCAT_3:6 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) ) "iff" (Bool "(" (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) ) ")" ) ")" )))) ; theorem :: ALTCAT_3:7 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) ) & (Bool (Set (Var "B")) "is" ($#v3_altcat_3 :::"iso"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v3_altcat_3 :::"iso"::: ) ) & (Bool (Set (Set "(" (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A")) ")" ) ($#k1_altcat_3 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k1_altcat_3 :::"""::: ) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "B")) ($#k1_altcat_3 :::"""::: ) ")" ))) ")" ))))) ; definitionlet "C" be ($#l2_altcat_1 :::"category":::); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); pred "o1" "," "o2" :::"are_iso"::: means :: ALTCAT_3:def 6 (Bool "(" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) "o1" "," "o2" ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) "o2" "," "o1" ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "o1" "," "o2" "st" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )) ")" ); reflexivity (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")) "holds" (Bool "(" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o1")) "st" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )) ")" )) ; symmetry (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o1")) "st" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )) ")" )) ; end; :: deftheorem defines :::"are_iso"::: ALTCAT_3:def 6 : (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o1")) "," (Set (Var "o2")) ($#r2_altcat_3 :::"are_iso"::: ) ) "iff" (Bool "(" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )) ")" ) ")" ))); theorem :: ALTCAT_3:8 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o1")) "," (Set (Var "o2")) ($#r2_altcat_3 :::"are_iso"::: ) ) & (Bool (Set (Var "o2")) "," (Set (Var "o3")) ($#r2_altcat_3 :::"are_iso"::: ) )) "holds" (Bool (Set (Var "o1")) "," (Set (Var "o3")) ($#r2_altcat_3 :::"are_iso"::: ) ))) ; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); attr "A" is :::"mono"::: means :: ALTCAT_3:def 7 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," "o1" ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," "o1" "st" (Bool (Bool (Set "A" ($#k5_altcat_1 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set "A" ($#k5_altcat_1 :::"*"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))))); end; :: deftheorem defines :::"mono"::: ALTCAT_3:def 7 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_altcat_3 :::"mono"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o1")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))))) ")" )))); definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); attr "A" is :::"epi"::: means :: ALTCAT_3:def 8 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) "o2" "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "o2" "," (Set (Var "o")) "st" (Bool (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) "A") ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k5_altcat_1 :::"*"::: ) "A"))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))))); end; :: deftheorem defines :::"epi"::: ALTCAT_3:def 8 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_altcat_3 :::"epi"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o")) "st" (Bool (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "C"))))) ")" )))); theorem :: ALTCAT_3:9 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_altcat_3 :::"mono"::: ) ) & (Bool (Set (Var "B")) "is" ($#v4_altcat_3 :::"mono"::: ) )) "holds" (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v4_altcat_3 :::"mono"::: ) ))))) ; theorem :: ALTCAT_3:10 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v5_altcat_3 :::"epi"::: ) ) & (Bool (Set (Var "B")) "is" ($#v5_altcat_3 :::"epi"::: ) )) "holds" (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v5_altcat_3 :::"epi"::: ) ))))) ; theorem :: ALTCAT_3:11 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v4_altcat_3 :::"mono"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v4_altcat_3 :::"mono"::: ) ))))) ; theorem :: ALTCAT_3:12 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v5_altcat_3 :::"epi"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v5_altcat_3 :::"epi"::: ) ))))) ; theorem :: ALTCAT_3:13 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" ($#k7_altcat_1 :::"EnsCat"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_altcat_3 :::"mono"::: ) ) "iff" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ))))) ; theorem :: ALTCAT_3:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set "(" ($#k7_altcat_1 :::"EnsCat"::: ) (Set (Var "X")) ")" ) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "A")))) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v5_altcat_3 :::"epi"::: ) ) "iff" (Bool (Set (Var "F")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ))))) ; theorem :: ALTCAT_3:15 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v5_altcat_3 :::"epi"::: ) )))) ; theorem :: ALTCAT_3:16 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v4_altcat_3 :::"mono"::: ) )))) ; theorem :: ALTCAT_3:17 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v4_altcat_3 :::"mono"::: ) ) & (Bool (Set (Var "A")) "is" ($#v5_altcat_3 :::"epi"::: ) ) ")" )))) ; theorem :: ALTCAT_3:18 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Var "B")) "is" ($#v1_altcat_3 :::"retraction"::: ) )) "holds" (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v1_altcat_3 :::"retraction"::: ) ))))) ; theorem :: ALTCAT_3:19 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_altcat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v2_altcat_3 :::"coretraction"::: ) ))))) ; theorem :: ALTCAT_3:20 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v1_altcat_3 :::"retraction"::: ) ) & (Bool (Set (Var "A")) "is" ($#v4_altcat_3 :::"mono"::: ) ) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )))) ; theorem :: ALTCAT_3:21 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) ) & (Bool (Set (Var "A")) "is" ($#v5_altcat_3 :::"epi"::: ) ) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )))) ; theorem :: ALTCAT_3:22 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v1_altcat_3 :::"retraction"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v1_altcat_3 :::"retraction"::: ) ))))) ; theorem :: ALTCAT_3:23 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))) "is" ($#v2_altcat_3 :::"coretraction"::: ) )) "holds" (Bool (Set (Var "A")) "is" ($#v2_altcat_3 :::"coretraction"::: ) ))))) ; theorem :: ALTCAT_3:24 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) "st" (Bool (Bool "(" "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A1")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool (Set (Var "A1")) "is" ($#v1_altcat_3 :::"retraction"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) "is" ($#v3_altcat_3 :::"iso"::: ) )))) ; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); cluster ($#v1_altcat_3 :::"retraction"::: ) ($#v2_altcat_3 :::"coretraction"::: ) ($#v4_altcat_3 :::"mono"::: ) ($#v5_altcat_3 :::"epi"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_altcat_1 :::"<^"::: ) "o" "," "o" ($#k1_altcat_1 :::"^>"::: ) ); end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); cluster ($#v1_altcat_3 :::"retraction"::: ) ($#v2_altcat_3 :::"coretraction"::: ) ($#v3_altcat_3 :::"iso"::: ) ($#v4_altcat_3 :::"mono"::: ) ($#v5_altcat_3 :::"epi"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_altcat_1 :::"<^"::: ) "o" "," "o" ($#k1_altcat_1 :::"^>"::: ) ); end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A", "B" be ($#v4_altcat_3 :::"mono"::: ) ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o")) "," (Set (Const "o")); cluster (Set "A" ($#k5_altcat_1 :::"*"::: ) "B") -> ($#v4_altcat_3 :::"mono"::: ) ; end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A", "B" be ($#v5_altcat_3 :::"epi"::: ) ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o")) "," (Set (Const "o")); cluster (Set "A" ($#k5_altcat_1 :::"*"::: ) "B") -> ($#v5_altcat_3 :::"epi"::: ) ; end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A", "B" be ($#v3_altcat_3 :::"iso"::: ) ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o")) "," (Set (Const "o")); cluster (Set "A" ($#k5_altcat_1 :::"*"::: ) "B") -> ($#v3_altcat_3 :::"iso"::: ) ; end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A", "B" be ($#v1_altcat_3 :::"retraction"::: ) ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o")) "," (Set (Const "o")); cluster (Set "A" ($#k5_altcat_1 :::"*"::: ) "B") -> ($#v1_altcat_3 :::"retraction"::: ) ; end; registrationlet "C" be ($#l2_altcat_1 :::"category":::); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "A", "B" be ($#v2_altcat_3 :::"coretraction"::: ) ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o")) "," (Set (Const "o")); cluster (Set "A" ($#k5_altcat_1 :::"*"::: ) "B") -> ($#v2_altcat_3 :::"coretraction"::: ) ; end; definitionlet "C" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); attr "o" is :::"initial"::: means :: ALTCAT_3:def 9 (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" "C" (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "o" "," (Set (Var "o1")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) "o" "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) "o" "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) ")" ))); end; :: deftheorem defines :::"initial"::: ALTCAT_3:def 9 : (Bool "for" (Set (Var "C")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v6_altcat_3 :::"initial"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o1")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) ")" ))) ")" ))); theorem :: ALTCAT_3:25 (Bool "for" (Set (Var "C")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v6_altcat_3 :::"initial"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o1")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool "(" "for" (Set (Var "M1")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o1")) "st" (Bool (Bool (Set (Var "M1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o1")) ($#k1_altcat_1 :::"^>"::: ) ))) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Var "M1"))) ")" ) ")" ))) ")" ))) ; theorem :: ALTCAT_3:26 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o1")) "is" ($#v6_altcat_3 :::"initial"::: ) ) & (Bool (Set (Var "o2")) "is" ($#v6_altcat_3 :::"initial"::: ) )) "holds" (Bool (Set (Var "o1")) "," (Set (Var "o2")) ($#r2_altcat_3 :::"are_iso"::: ) ))) ; definitionlet "C" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); attr "o" is :::"terminal"::: means :: ALTCAT_3:def 10 (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" "C" (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," "o" "st" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," "o" ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," "o" ($#k1_altcat_1 :::"^>"::: ) ) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) ")" ))); end; :: deftheorem defines :::"terminal"::: ALTCAT_3:def 10 : (Bool "for" (Set (Var "C")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v7_altcat_3 :::"terminal"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) "is" ($#v1_zfmisc_1 :::"trivial"::: ) ) ")" ))) ")" ))); theorem :: ALTCAT_3:27 (Bool "for" (Set (Var "C")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v7_altcat_3 :::"terminal"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "M")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o")) "st" (Bool "(" (Bool (Set (Var "M")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) )) & (Bool "(" "for" (Set (Var "M1")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o")) "st" (Bool (Bool (Set (Var "M1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ))) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Var "M1"))) ")" ) ")" ))) ")" ))) ; theorem :: ALTCAT_3:28 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o1")) "is" ($#v7_altcat_3 :::"terminal"::: ) ) & (Bool (Set (Var "o2")) "is" ($#v7_altcat_3 :::"terminal"::: ) )) "holds" (Bool (Set (Var "o1")) "," (Set (Var "o2")) ($#r2_altcat_3 :::"are_iso"::: ) ))) ; definitionlet "C" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); attr "o" is :::"_zero"::: means :: ALTCAT_3:def 11 (Bool "(" (Bool "o" "is" ($#v6_altcat_3 :::"initial"::: ) ) & (Bool "o" "is" ($#v7_altcat_3 :::"terminal"::: ) ) ")" ); end; :: deftheorem defines :::"_zero"::: ALTCAT_3:def 11 : (Bool "for" (Set (Var "C")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "o")) "is" ($#v8_altcat_3 :::"_zero"::: ) ) "iff" (Bool "(" (Bool (Set (Var "o")) "is" ($#v6_altcat_3 :::"initial"::: ) ) & (Bool (Set (Var "o")) "is" ($#v7_altcat_3 :::"terminal"::: ) ) ")" ) ")" ))); theorem :: ALTCAT_3:29 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o1")) "is" ($#v8_altcat_3 :::"_zero"::: ) ) & (Bool (Set (Var "o2")) "is" ($#v8_altcat_3 :::"_zero"::: ) )) "holds" (Bool (Set (Var "o1")) "," (Set (Var "o2")) ($#r2_altcat_3 :::"are_iso"::: ) ))) ; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C")); let "M" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); attr "M" is :::"_zero"::: means :: ALTCAT_3:def 12 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "C" "st" (Bool (Bool (Set (Var "o")) "is" ($#v8_altcat_3 :::"_zero"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "o1" "," (Set (Var "o")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," "o2" "holds" (Bool "M" ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))))))); end; :: deftheorem defines :::"_zero"::: ALTCAT_3:def 12 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "M")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#v9_altcat_3 :::"_zero"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "o")) "is" ($#v8_altcat_3 :::"_zero"::: ) )) "holds" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o2")) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set (Var "B")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "A"))))))) ")" )))); theorem :: ALTCAT_3:30 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "M1")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "M2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Var "M1")) "is" ($#v9_altcat_3 :::"_zero"::: ) ) & (Bool (Set (Var "M2")) "is" ($#v9_altcat_3 :::"_zero"::: ) )) "holds" (Bool (Set (Set (Var "M2")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "M1"))) "is" ($#v9_altcat_3 :::"_zero"::: ) ))))) ;