:: CAT_4 semantic presentation begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); redefine pred "a" "," "b" :::"are_isomorphic"::: means :: CAT_4:def 1 (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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," "b"(Bool "ex" (Set (Var "f9")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," "a" "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "b")) & (Bool (Set (Set (Var "f9")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "a")) ")" ))) ")" ); end; :: deftheorem defines :::"are_isomorphic"::: CAT_4:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_cat_1 :::"are_isomorphic"::: ) ) "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b"))(Bool "ex" (Set (Var "f9")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f9"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "f9")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) ")" ))) ")" ) ")" ))); begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); attr "C" is :::"with_finite_product"::: means :: CAT_4:def 2 (Bool "for" (Set (Var "I")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "C"(Bool "ex" (Set (Var "F9")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool "(" (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F9"))) ($#r2_funct_2 :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "a")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F9"))) ")" ))))); end; :: deftheorem defines :::"with_finite_product"::: CAT_4:def 2 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_cat_4 :::"with_finite_product"::: ) ) "iff" (Bool "for" (Set (Var "I")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool "ex" (Set (Var "F9")) "being" ($#m1_cat_3 :::"Projections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool "(" (Bool (Set ($#k3_cat_3 :::"cods"::: ) (Set (Var "F9"))) ($#r2_funct_2 :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "a")) ($#r1_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "F9"))) ")" ))))) ")" )); theorem :: CAT_4:1 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v1_cat_4 :::"with_finite_product"::: ) ) "iff" (Bool "(" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool "ex" (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 "c"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2"))) ")" ))) ")" ) ")" ) ")" )) ; definitionattr "c1" is :::"strict"::: ; struct :::"ProdCatStr"::: -> ($#l1_cat_1 :::"CatStr"::: ) ; aggr :::"ProdCatStr":::(# :::"carrier":::, :::"carrier'":::, :::"Source":::, :::"Target":::, :::"Comp":::, :::"TerminalObj":::, :::"CatProd":::, :::"Proj1":::, :::"Proj2"::: #) -> ($#l1_cat_4 :::"ProdCatStr"::: ) ; sel :::"TerminalObj"::: "c1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"CatProd"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"Proj1"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); sel :::"Proj2"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) for ($#l1_cat_4 :::"ProdCatStr"::: ) ; end; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_4 :::"ProdCatStr"::: ) ; func :::"[1]"::: "C" -> ($#m1_subset_1 :::"Object":::) "of" "C" equals :: CAT_4:def 3 (Set "the" ($#u1_cat_4 :::"TerminalObj"::: ) "of" "C"); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "a" :::"[x]"::: "b" -> ($#m1_subset_1 :::"Object":::) "of" "C" equals :: CAT_4:def 4 (Set (Set "the" ($#u2_cat_4 :::"CatProd"::: ) "of" "C") ($#k5_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); func :::"pr1"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Morphism":::) "of" "C" equals :: CAT_4:def 5 (Set (Set "the" ($#u3_cat_4 :::"Proj1"::: ) "of" "C") ($#k2_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); func :::"pr2"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Morphism":::) "of" "C" equals :: CAT_4:def 6 (Set (Set "the" ($#u4_cat_4 :::"Proj2"::: ) "of" "C") ($#k2_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); end; :: deftheorem defines :::"[1]"::: CAT_4:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_4 :::"ProdCatStr"::: ) "holds" (Bool (Set ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_cat_4 :::"TerminalObj"::: ) "of" (Set (Var "C"))))); :: deftheorem defines :::"[x]"::: CAT_4:def 4 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_4 :::"ProdCatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_cat_4 :::"CatProd"::: ) "of" (Set (Var "C"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); :: deftheorem defines :::"pr1"::: CAT_4:def 5 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_4 :::"ProdCatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k3_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_cat_4 :::"Proj1"::: ) "of" (Set (Var "C"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); :: deftheorem defines :::"pr2"::: CAT_4:def 6 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_4 :::"ProdCatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_cat_4 :::"Proj2"::: ) "of" (Set (Var "C"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); definitionlet "o", "m" be ($#m1_hidden :::"set"::: ) ; func :::"c1Cat"::: "(" "o" "," "m" ")" -> ($#v2_cat_4 :::"strict"::: ) ($#l1_cat_4 :::"ProdCatStr"::: ) equals :: CAT_4:def 7 (Set ($#g1_cat_4 :::"ProdCatStr"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) "o" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "m" ($#k1_tarski :::"}"::: ) ) "," (Set "(" "m" ($#k18_funcop_1 :::":->"::: ) "o" ")" ) "," (Set "(" "m" ($#k18_funcop_1 :::":->"::: ) "o" ")" ) "," (Set "(" "(" "m" "," "m" ")" ($#k17_funcop_1 :::":->"::: ) "m" ")" ) "," (Set "(" ($#k1_algstr_1 :::"Extract"::: ) "o" ")" ) "," (Set "(" "(" "o" "," "o" ")" ($#k17_funcop_1 :::":->"::: ) "o" ")" ) "," (Set "(" "(" "o" "," "o" ")" ($#k17_funcop_1 :::":->"::: ) "m" ")" ) "," (Set "(" "(" "o" "," "o" ")" ($#k17_funcop_1 :::":->"::: ) "m" ")" ) "#)" ); end; :: deftheorem defines :::"c1Cat"::: CAT_4:def 7 : (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_4 :::"ProdCatStr"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set (Var "o")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "m")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set (Var "m")) ($#k18_funcop_1 :::":->"::: ) (Set (Var "o")) ")" ) "," (Set "(" (Set (Var "m")) ($#k18_funcop_1 :::":->"::: ) (Set (Var "o")) ")" ) "," (Set "(" "(" (Set (Var "m")) "," (Set (Var "m")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_algstr_1 :::"Extract"::: ) (Set (Var "o")) ")" ) "," (Set "(" "(" (Set (Var "o")) "," (Set (Var "o")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "o")) ")" ) "," (Set "(" "(" (Set (Var "o")) "," (Set (Var "o")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "m")) ")" ) "," (Set "(" "(" (Set (Var "o")) "," (Set (Var "o")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "m")) ")" ) "#)" ))); registrationlet "o", "m" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_cat_4 :::"c1Cat"::: ) "(" "o" "," "m" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v15_struct_0 :::"trivial'"::: ) ($#v2_cat_4 :::"strict"::: ) ; end; theorem :: CAT_4:2 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" )) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" )) "," (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" )) "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" )) "," (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" )) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v2_cat_4 :::"strict"::: ) for ($#l1_cat_4 :::"ProdCatStr"::: ) ; end; registrationlet "o", "m" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k5_cat_4 :::"c1Cat"::: ) "(" "o" "," "m" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v2_cat_4 :::"strict"::: ) ; end; theorem :: CAT_4:3 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: CAT_4:4 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: CAT_4:5 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; theorem :: CAT_4:6 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "f")) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")))))) ; theorem :: CAT_4:7 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:8 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) ))) ; theorem :: CAT_4:9 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "c")) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Var "p1")) "," (Set (Var "p2")))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#l1_cat_4 :::"ProdCatStr"::: ) ; attr "IT" is :::"Cartesian"::: means :: CAT_4:def 8 (Bool "(" (Bool (Set "the" ($#u1_cat_4 :::"TerminalObj"::: ) "of" "IT") "is" ($#v10_cat_1 :::"terminal"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "IT" "holds" (Bool "(" (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set "the" ($#u3_cat_4 :::"Proj1"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set "the" ($#u4_cat_4 :::"Proj2"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "the" ($#u2_cat_4 :::"CatProd"::: ) "of" "IT") ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Set "the" ($#u3_cat_4 :::"Proj1"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set (Set "the" ($#u4_cat_4 :::"Proj2"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Cartesian"::: CAT_4:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#l1_cat_4 :::"ProdCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_cat_4 :::"Cartesian"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_cat_4 :::"TerminalObj"::: ) "of" (Set (Var "IT"))) "is" ($#v10_cat_1 :::"terminal"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set "the" ($#u3_cat_4 :::"Proj1"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set "the" ($#u4_cat_4 :::"Proj2"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "the" ($#u2_cat_4 :::"CatProd"::: ) "of" (Set (Var "IT"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set (Set "the" ($#u3_cat_4 :::"Proj1"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set (Set "the" ($#u4_cat_4 :::"Proj2"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) ")" ) ")" ) ")" )); theorem :: CAT_4:10 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_cat_4 :::"c1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ) "is" ($#v3_cat_4 :::"Cartesian"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v2_cat_4 :::"strict"::: ) ($#v3_cat_4 :::"Cartesian"::: ) for ($#l1_cat_4 :::"ProdCatStr"::: ) ; end; definitionmode Cartesian_category is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v3_cat_4 :::"Cartesian"::: ) ($#l1_cat_4 :::"ProdCatStr"::: ) ; end; theorem :: CAT_4:11 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) "holds" (Bool (Set ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C"))) "is" ($#v10_cat_1 :::"terminal"::: ) )) ; theorem :: CAT_4:12 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C"))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2")))))) ; theorem :: CAT_4:13 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"term"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set ($#k1_cat_4 :::"[1]"::: ) "C") means :: CAT_4:def 9 (Bool verum); end; :: deftheorem defines :::"term"::: CAT_4:def 9 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_cat_4 :::"term"::: ) (Set (Var "a")))) "iff" (Bool verum) ")" )))); theorem :: CAT_4:14 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k6_cat_4 :::"term"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k10_cat_3 :::"term"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ")" )))) ; theorem :: CAT_4:15 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k6_cat_4 :::"term"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k6_cat_4 :::"term"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")))) ")" ))) ; theorem :: CAT_4:16 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_cat_4 :::"term"::: ) (Set (Var "a")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: CAT_4:17 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k3_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k3_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: CAT_4:18 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k4_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k4_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); :: original: :::"pr1"::: redefine func :::"pr1"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k2_cat_4 :::"[x]"::: ) "b") "," "a"; :: original: :::"pr2"::: redefine func :::"pr2"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k2_cat_4 :::"[x]"::: ) "b") "," "b"; end; theorem :: CAT_4:19 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: CAT_4:20 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b"))) ($#r2_cat_3 :::"is_a_product_wrt"::: ) (Set ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; theorem :: CAT_4:21 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) "holds" (Bool (Set (Var "C")) "is" ($#v1_cat_4 :::"with_finite_product"::: ) )) ; theorem :: CAT_4:22 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_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 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_cat_3 :::"retraction"::: ) ) & (Bool (Set ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_cat_3 :::"retraction"::: ) ) ")" ))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a", "b", "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "c")) "," (Set (Const "a")); let "g" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "c")) "," (Set (Const "b")); assume (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Const "c")) "," (Set (Const "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Const "c")) "," (Set (Const "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; func :::"<:":::"f" "," "g":::":>"::: -> ($#m1_cat_1 :::"Morphism"::: ) "of" "c" "," (Set "a" ($#k2_cat_4 :::"[x]"::: ) "b") means :: CAT_4:def 10 (Bool "(" (Bool (Set (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" "a" "," "b" ")" ")" ) ($#k5_cat_1 :::"*"::: ) it) ($#r1_hidden :::"="::: ) "f") & (Bool (Set (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" "a" "," "b" ")" ")" ) ($#k5_cat_1 :::"*"::: ) it) ($#r1_hidden :::"="::: ) "g") ")" ); end; :: deftheorem defines :::"<:"::: CAT_4:def 10 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_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 "c")) "," (Set (Var "a")) (Bool "for" (Set (Var "g")) "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 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b"))) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k9_cat_4 :::":>"::: ) )) "iff" (Bool "(" (Bool (Set (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set (Var "b7"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) ")" )))))); theorem :: CAT_4:23 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_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 (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:24 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k9_cat_4 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ))))) ; theorem :: CAT_4:25 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "a")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "b")) (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (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 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "h")) ")" ) "," (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k9_cat_4 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k9_cat_4 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k9_cat_4 :::":>"::: ) ) ($#k5_cat_1 :::"*"::: ) (Set (Var "h"))))))))) ; theorem :: CAT_4:26 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_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")) "," (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "a")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "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 ($#k9_cat_4 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k9_cat_4 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set (Var "k")) "," (Set (Var "h")) ($#k9_cat_4 :::":>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" ))))) ; theorem :: CAT_4:27 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_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 "c")) "," (Set (Var "a")) (Bool "for" (Set (Var "g")) "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 "(" (Bool (Set (Var "f")) "is" ($#v7_cat_1 :::"monic"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v7_cat_1 :::"monic"::: ) ) ")" )) "holds" (Bool (Set ($#k9_cat_4 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k9_cat_4 :::":>"::: ) ) "is" ($#v7_cat_1 :::"monic"::: ) ))))) ; theorem :: CAT_4:28 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"lambda"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set "(" ($#k1_cat_4 :::"[1]"::: ) "C" ")" ) ($#k2_cat_4 :::"[x]"::: ) "a") "," "a" equals :: CAT_4:def 11 (Set ($#k8_cat_4 :::"pr2"::: ) "(" (Set "(" ($#k1_cat_4 :::"[1]"::: ) "C" ")" ) "," "a" ")" ); func :::"lambda'"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set (Set "(" ($#k1_cat_4 :::"[1]"::: ) "C" ")" ) ($#k2_cat_4 :::"[x]"::: ) "a") equals :: CAT_4:def 12 (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k6_cat_4 :::"term"::: ) "a" ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) "a" ")" ) ($#k9_cat_4 :::":>"::: ) ); func :::"rho"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k2_cat_4 :::"[x]"::: ) (Set "(" ($#k1_cat_4 :::"[1]"::: ) "C" ")" )) "," "a" equals :: CAT_4:def 13 (Set ($#k7_cat_4 :::"pr1"::: ) "(" "a" "," (Set "(" ($#k1_cat_4 :::"[1]"::: ) "C" ")" ) ")" ); func :::"rho'"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set "a" ($#k2_cat_4 :::"[x]"::: ) (Set "(" ($#k1_cat_4 :::"[1]"::: ) "C" ")" )) equals :: CAT_4:def 14 (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) "a" ")" ) "," (Set "(" ($#k6_cat_4 :::"term"::: ) "a" ")" ) ($#k9_cat_4 :::":>"::: ) ); end; :: deftheorem defines :::"lambda"::: CAT_4:def 11 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k10_cat_4 :::"lambda"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k8_cat_4 :::"pr2"::: ) "(" (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) "," (Set (Var "a")) ")" )))); :: deftheorem defines :::"lambda'"::: CAT_4:def 12 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k11_cat_4 :::"lambda'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k6_cat_4 :::"term"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k9_cat_4 :::":>"::: ) )))); :: deftheorem defines :::"rho"::: CAT_4:def 13 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k12_cat_4 :::"rho"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ")" )))); :: deftheorem defines :::"rho'"::: CAT_4:def 14 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k13_cat_4 :::"rho'"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k6_cat_4 :::"term"::: ) (Set (Var "a")) ")" ) ($#k9_cat_4 :::":>"::: ) )))); theorem :: CAT_4:29 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k10_cat_4 :::"lambda"::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k11_cat_4 :::"lambda'"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k11_cat_4 :::"lambda'"::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k10_cat_4 :::"lambda"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Set "(" ($#k12_cat_4 :::"rho"::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k13_cat_4 :::"rho'"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) & (Bool (Set (Set "(" ($#k13_cat_4 :::"rho'"::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k12_cat_4 :::"rho"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ")" ))) ")" ))) ; theorem :: CAT_4:30 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" )) ($#r1_cat_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "a")) "," (Set (Set "(" ($#k1_cat_4 :::"[1]"::: ) (Set (Var "C")) ")" ) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "a"))) ($#r1_cat_1 :::"are_isomorphic"::: ) ) ")" ))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"Switch"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k2_cat_4 :::"[x]"::: ) "b") "," (Set "b" ($#k2_cat_4 :::"[x]"::: ) "a") equals :: CAT_4:def 15 (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" "a" "," "b" ")" ")" ) "," (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" "a" "," "b" ")" ")" ) ($#k9_cat_4 :::":>"::: ) ); end; :: deftheorem defines :::"Switch"::: CAT_4:def 15 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k14_cat_4 :::"Switch"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k9_cat_4 :::":>"::: ) )))); theorem :: CAT_4:31 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) "," (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:32 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k14_cat_4 :::"Switch"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k14_cat_4 :::"Switch"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "a")) ")" ))))) ; theorem :: CAT_4:33 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b"))) "," (Set (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "a"))) ($#r1_cat_1 :::"are_isomorphic"::: ) ))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"Delta"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set "a" ($#k2_cat_4 :::"[x]"::: ) "a") equals :: CAT_4:def 16 (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) "a" ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) "a" ")" ) ($#k9_cat_4 :::":>"::: ) ); end; :: deftheorem defines :::"Delta"::: CAT_4:def 16 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k15_cat_4 :::"Delta"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k9_cat_4 :::":>"::: ) )))); theorem :: CAT_4:34 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:35 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_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 ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k9_cat_4 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "f")) ($#k9_cat_4 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_cat_4 :::"Delta"::: ) (Set (Var "b")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))))))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a", "b", "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"Alpha"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set "(" "a" ($#k2_cat_4 :::"[x]"::: ) "b" ")" ) ($#k2_cat_4 :::"[x]"::: ) "c") "," (Set "a" ($#k2_cat_4 :::"[x]"::: ) (Set "(" "b" ($#k2_cat_4 :::"[x]"::: ) "c" ")" )) equals :: CAT_4:def 17 (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" "a" "," "b" ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set "(" "a" ($#k2_cat_4 :::"[x]"::: ) "b" ")" ) "," "c" ")" ")" ) ")" ) "," (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" "a" "," "b" ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set "(" "a" ($#k2_cat_4 :::"[x]"::: ) "b" ")" ) "," "c" ")" ")" ) ")" ) "," (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set "(" "a" ($#k2_cat_4 :::"[x]"::: ) "b" ")" ) "," "c" ")" ")" ) ($#k9_cat_4 :::":>"::: ) ) ($#k9_cat_4 :::":>"::: ) ); func :::"Alpha'"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k2_cat_4 :::"[x]"::: ) (Set "(" "b" ($#k2_cat_4 :::"[x]"::: ) "c" ")" )) "," (Set (Set "(" "a" ($#k2_cat_4 :::"[x]"::: ) "b" ")" ) ($#k2_cat_4 :::"[x]"::: ) "c") equals :: CAT_4:def 18 (Set ($#k9_cat_4 :::"<:"::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" "a" "," (Set "(" "b" ($#k2_cat_4 :::"[x]"::: ) "c" ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" "b" "," "c" ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" "a" "," (Set "(" "b" ($#k2_cat_4 :::"[x]"::: ) "c" ")" ) ")" ")" ) ")" ) ($#k9_cat_4 :::":>"::: ) ) "," (Set "(" (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" "b" "," "c" ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" "a" "," (Set "(" "b" ($#k2_cat_4 :::"[x]"::: ) "c" ")" ) ")" ")" ) ")" ) ($#k9_cat_4 :::":>"::: ) ); end; :: deftheorem defines :::"Alpha"::: CAT_4:def 17 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k16_cat_4 :::"Alpha"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) "," (Set (Var "c")) ")" ")" ) ")" ) "," (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) "," (Set (Var "c")) ")" ")" ) ")" ) "," (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) "," (Set (Var "c")) ")" ")" ) ($#k9_cat_4 :::":>"::: ) ) ($#k9_cat_4 :::":>"::: ) )))); :: deftheorem defines :::"Alpha'"::: CAT_4:def 18 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k17_cat_4 :::"Alpha'"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) ")" ")" ) ")" ) ($#k9_cat_4 :::":>"::: ) ) "," (Set "(" (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) ")" ")" ) ")" ) ($#k9_cat_4 :::":>"::: ) )))); theorem :: CAT_4:36 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: CAT_4:37 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k16_cat_4 :::"Alpha"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k17_cat_4 :::"Alpha'"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ) ")" ))) & (Bool (Set (Set "(" ($#k17_cat_4 :::"Alpha'"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k16_cat_4 :::"Alpha"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" ))) ")" ))) ; theorem :: CAT_4:38 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c"))) "," (Set (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set "(" (Set (Var "b")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "c")) ")" )) ($#r1_cat_1 :::"are_isomorphic"::: ) ))) ; definitionlet "C" be ($#l1_cat_4 :::"Cartesian_category":::); let "a", "b", "c", "d" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); let "g" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "c")) "," (Set (Const "d")); func "f" :::"[x]"::: "g" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k2_cat_4 :::"[x]"::: ) "c") "," (Set "b" ($#k2_cat_4 :::"[x]"::: ) "d") equals :: CAT_4:def 19 (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" "f" ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" "a" "," "c" ")" ")" ) ")" ) "," (Set "(" "g" ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" "a" "," "c" ")" ")" ) ")" ) ($#k9_cat_4 :::":>"::: ) ); end; :: deftheorem defines :::"[x]"::: CAT_4:def 19 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "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 "c")) "," (Set (Var "d")) "holds" (Bool (Set (Set (Var "f")) ($#k18_cat_4 :::"[x]"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k7_cat_4 :::"pr1"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" ) "," (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k8_cat_4 :::"pr2"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ")" ) ")" ) ($#k9_cat_4 :::":>"::: ) )))))); theorem :: CAT_4:39 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (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 "c")) ")" ) ($#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 (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ) "," (Set "(" (Set (Var "c")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "d")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:40 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k18_cat_4 :::"[x]"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k2_cat_4 :::"[x]"::: ) (Set (Var "b")) ")" ))))) ; theorem :: CAT_4:41 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "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 "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "e")) "," (Set (Var "a")) (Bool "for" (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "e")) "," (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 "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "e")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "e")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k18_cat_4 :::"[x]"::: ) (Set (Var "h")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set (Var "g")) "," (Set (Var "k")) ($#k9_cat_4 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_cat_4 :::"<:"::: ) (Set "(" (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "k")) ")" ) ($#k9_cat_4 :::":>"::: ) )))))))) ; theorem :: CAT_4:42 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_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 "c")) "," (Set (Var "a")) (Bool "for" (Set (Var "g")) "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 :::"{}"::: ) ))) "holds" (Bool (Set ($#k9_cat_4 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k9_cat_4 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k18_cat_4 :::"[x]"::: ) (Set (Var "g")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k15_cat_4 :::"Delta"::: ) (Set (Var "c")) ")" ))))))) ; theorem :: CAT_4:43 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_4 :::"Cartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "s")) "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 "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "e")) "," (Set (Var "a")) (Bool "for" (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "s")) "," (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 "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "e")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "s")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k18_cat_4 :::"[x]"::: ) (Set (Var "h")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k18_cat_4 :::"[x]"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k18_cat_4 :::"[x]"::: ) (Set "(" (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "k")) ")" ))))))))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); attr "C" is :::"with_finite_coproduct"::: means :: CAT_4:def 20 (Bool "for" (Set (Var "I")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "C"(Bool "ex" (Set (Var "F9")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool "(" (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F9"))) ($#r2_funct_2 :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "a")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F9"))) ")" ))))); end; :: deftheorem defines :::"with_finite_coproduct"::: CAT_4:def 20 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_cat_4 :::"with_finite_coproduct"::: ) ) "iff" (Bool "for" (Set (Var "I")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool "ex" (Set (Var "F9")) "being" ($#m2_cat_3 :::"Injections_family"::: ) "of" (Set (Var "a")) "," (Set (Var "I")) "st" (Bool "(" (Bool (Set ($#k2_cat_3 :::"doms"::: ) (Set (Var "F9"))) ($#r2_funct_2 :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "a")) ($#r3_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "F9"))) ")" ))))) ")" )); theorem :: CAT_4:44 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_cat_4 :::"with_finite_coproduct"::: ) ) "iff" (Bool "(" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) )) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool "ex" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i1"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "i2"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (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 (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2"))) ")" ))) ")" ) ")" ) ")" )) ; definitionattr "c1" is :::"strict"::: ; struct :::"CoprodCatStr"::: -> ($#l1_cat_1 :::"CatStr"::: ) ; aggr :::"CoprodCatStr":::(# :::"carrier":::, :::"carrier'":::, :::"Source":::, :::"Target":::, :::"Comp":::, :::"Initial":::, :::"Coproduct":::, :::"Incl1":::, :::"Incl2"::: #) -> ($#l2_cat_4 :::"CoprodCatStr"::: ) ; sel :::"Initial"::: "c1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"Coproduct"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); sel :::"Incl1"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); sel :::"Incl2"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) for ($#l2_cat_4 :::"CoprodCatStr"::: ) ; end; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l2_cat_4 :::"CoprodCatStr"::: ) ; func :::"[[0]]"::: "C" -> ($#m1_subset_1 :::"Object":::) "of" "C" equals :: CAT_4:def 21 (Set "the" ($#u5_cat_4 :::"Initial"::: ) "of" "C"); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "a" :::"+"::: "b" -> ($#m1_subset_1 :::"Object":::) "of" "C" equals :: CAT_4:def 22 (Set (Set "the" ($#u6_cat_4 :::"Coproduct"::: ) "of" "C") ($#k5_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); func :::"in1"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Morphism":::) "of" "C" equals :: CAT_4:def 23 (Set (Set "the" ($#u7_cat_4 :::"Incl1"::: ) "of" "C") ($#k2_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); func :::"in2"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Morphism":::) "of" "C" equals :: CAT_4:def 24 (Set (Set "the" ($#u8_cat_4 :::"Incl2"::: ) "of" "C") ($#k2_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); end; :: deftheorem defines :::"[[0]]"::: CAT_4:def 21 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l2_cat_4 :::"CoprodCatStr"::: ) "holds" (Bool (Set ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_cat_4 :::"Initial"::: ) "of" (Set (Var "C"))))); :: deftheorem defines :::"+"::: CAT_4:def 22 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l2_cat_4 :::"CoprodCatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u6_cat_4 :::"Coproduct"::: ) "of" (Set (Var "C"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); :: deftheorem defines :::"in1"::: CAT_4:def 23 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l2_cat_4 :::"CoprodCatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k21_cat_4 :::"in1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u7_cat_4 :::"Incl1"::: ) "of" (Set (Var "C"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); :: deftheorem defines :::"in2"::: CAT_4:def 24 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l2_cat_4 :::"CoprodCatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k22_cat_4 :::"in2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u8_cat_4 :::"Incl2"::: ) "of" (Set (Var "C"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))); definitionlet "o", "m" be ($#m1_hidden :::"set"::: ) ; func :::"c1Cat*"::: "(" "o" "," "m" ")" -> ($#v5_cat_4 :::"strict"::: ) ($#l2_cat_4 :::"CoprodCatStr"::: ) equals :: CAT_4:def 25 (Set ($#g2_cat_4 :::"CoprodCatStr"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) "o" ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) "m" ($#k1_tarski :::"}"::: ) ) "," (Set "(" "m" ($#k18_funcop_1 :::":->"::: ) "o" ")" ) "," (Set "(" "m" ($#k18_funcop_1 :::":->"::: ) "o" ")" ) "," (Set "(" "(" "m" "," "m" ")" ($#k17_funcop_1 :::":->"::: ) "m" ")" ) "," (Set "(" ($#k1_algstr_1 :::"Extract"::: ) "o" ")" ) "," (Set "(" "(" "o" "," "o" ")" ($#k17_funcop_1 :::":->"::: ) "o" ")" ) "," (Set "(" "(" "o" "," "o" ")" ($#k17_funcop_1 :::":->"::: ) "m" ")" ) "," (Set "(" "(" "o" "," "o" ")" ($#k17_funcop_1 :::":->"::: ) "m" ")" ) "#)" ); end; :: deftheorem defines :::"c1Cat*"::: CAT_4:def 25 : (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g2_cat_4 :::"CoprodCatStr"::: ) "(#" (Set ($#k1_tarski :::"{"::: ) (Set (Var "o")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "m")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" (Set (Var "m")) ($#k18_funcop_1 :::":->"::: ) (Set (Var "o")) ")" ) "," (Set "(" (Set (Var "m")) ($#k18_funcop_1 :::":->"::: ) (Set (Var "o")) ")" ) "," (Set "(" "(" (Set (Var "m")) "," (Set (Var "m")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "m")) ")" ) "," (Set "(" ($#k1_algstr_1 :::"Extract"::: ) (Set (Var "o")) ")" ) "," (Set "(" "(" (Set (Var "o")) "," (Set (Var "o")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "o")) ")" ) "," (Set "(" "(" (Set (Var "o")) "," (Set (Var "o")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "m")) ")" ) "," (Set "(" "(" (Set (Var "o")) "," (Set (Var "o")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "m")) ")" ) "#)" ))); theorem :: CAT_4:45 canceled; registrationlet "o", "m" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k23_cat_4 :::"c1Cat*"::: ) "(" "o" "," "m" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v15_struct_0 :::"trivial'"::: ) ($#v5_cat_4 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v5_cat_4 :::"strict"::: ) for ($#l2_cat_4 :::"CoprodCatStr"::: ) ; end; registrationlet "o", "m" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k23_cat_4 :::"c1Cat*"::: ) "(" "o" "," "m" ")" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v5_cat_4 :::"strict"::: ) ; end; theorem :: CAT_4:46 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: CAT_4:47 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: CAT_4:48 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))) ; theorem :: CAT_4:49 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "f")) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")))))) ; theorem :: CAT_4:50 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:51 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ))) ; theorem :: CAT_4:52 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "i1")) "," (Set (Var "i2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "c")) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Var "i1")) "," (Set (Var "i2")))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#l2_cat_4 :::"CoprodCatStr"::: ) ; attr "IT" is :::"Cocartesian"::: means :: CAT_4:def 26 (Bool "(" (Bool (Set "the" ($#u5_cat_4 :::"Initial"::: ) "of" "IT") "is" ($#v11_cat_1 :::"initial"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "IT" "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set "the" ($#u7_cat_4 :::"Incl1"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set "the" ($#u8_cat_4 :::"Incl2"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "the" ($#u6_cat_4 :::"Coproduct"::: ) "of" "IT") ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Set "the" ($#u7_cat_4 :::"Incl1"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set (Set "the" ($#u8_cat_4 :::"Incl2"::: ) "of" "IT") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Cocartesian"::: CAT_4:def 26 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#l2_cat_4 :::"CoprodCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_cat_4 :::"Cocartesian"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u5_cat_4 :::"Initial"::: ) "of" (Set (Var "IT"))) "is" ($#v11_cat_1 :::"initial"::: ) ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "IT")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set "the" ($#u7_cat_4 :::"Incl1"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set "the" ($#u8_cat_4 :::"Incl2"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "the" ($#u6_cat_4 :::"Coproduct"::: ) "of" (Set (Var "IT"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set (Set "the" ($#u7_cat_4 :::"Incl1"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set (Set "the" ($#u8_cat_4 :::"Incl2"::: ) "of" (Set (Var "IT"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" ) ")" ) ")" ) ")" )); theorem :: CAT_4:53 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k23_cat_4 :::"c1Cat*"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ) "is" ($#v6_cat_4 :::"Cocartesian"::: ) )) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v5_cat_4 :::"strict"::: ) ($#v6_cat_4 :::"Cocartesian"::: ) for ($#l2_cat_4 :::"CoprodCatStr"::: ) ; end; definitionmode Cocartesian_category is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v6_cat_4 :::"Cocartesian"::: ) ($#l2_cat_4 :::"CoprodCatStr"::: ) ; end; theorem :: CAT_4:54 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) "holds" (Bool (Set ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C"))) "is" ($#v11_cat_1 :::"initial"::: ) )) ; theorem :: CAT_4:55 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C"))) "," (Set (Var "a")) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2")))))) ; definitionlet "C" be ($#l2_cat_4 :::"Cocartesian_category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"init"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set ($#k19_cat_4 :::"[[0]]"::: ) "C") "," "a" means :: CAT_4:def 27 (Bool verum); end; :: deftheorem defines :::"init"::: CAT_4:def 27 : (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C"))) "," (Set (Var "a")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k24_cat_4 :::"init"::: ) (Set (Var "a")))) "iff" (Bool verum) ")" )))); theorem :: CAT_4:56 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:57 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k24_cat_4 :::"init"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k11_cat_3 :::"init"::: ) "(" (Set "(" ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C")) ")" ) "," (Set (Var "a")) ")" )))) ; theorem :: CAT_4:58 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k24_cat_4 :::"init"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k24_cat_4 :::"init"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: CAT_4:59 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C")) ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k24_cat_4 :::"init"::: ) (Set (Var "a")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: CAT_4:60 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k21_cat_4 :::"in1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k21_cat_4 :::"in1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")))) ")" ))) ; theorem :: CAT_4:61 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k22_cat_4 :::"in2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k22_cat_4 :::"in2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")))) ")" ))) ; theorem :: CAT_4:62 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set "(" (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: CAT_4:63 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b"))) ($#r4_cat_3 :::"is_a_coproduct_wrt"::: ) (Set ($#k21_cat_4 :::"in1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set ($#k22_cat_4 :::"in2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))) ; theorem :: CAT_4:64 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) "holds" (Bool (Set (Var "C")) "is" ($#v4_cat_4 :::"with_finite_coproduct"::: ) )) ; definitionlet "C" be ($#l2_cat_4 :::"Cocartesian_category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); :: original: :::"in1"::: redefine func :::"in1"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set "a" ($#k20_cat_4 :::"+"::: ) "b"); :: original: :::"in2"::: redefine func :::"in2"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," (Set "a" ($#k20_cat_4 :::"+"::: ) "b"); end; theorem :: CAT_4:65 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_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 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k25_cat_4 :::"in1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_cat_3 :::"coretraction"::: ) ) & (Bool (Set ($#k26_cat_4 :::"in2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_cat_3 :::"coretraction"::: ) ) ")" ))) ; definitionlet "C" be ($#l2_cat_4 :::"Cocartesian_category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); :: original: :::"in1"::: redefine func :::"in1"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set "a" ($#k20_cat_4 :::"+"::: ) "b"); :: original: :::"in2"::: redefine func :::"in2"::: "(" "a" "," "b" ")" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," (Set "a" ($#k20_cat_4 :::"+"::: ) "b"); end; definitionlet "C" be ($#l2_cat_4 :::"Cocartesian_category":::); let "a", "b", "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "c")); let "g" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "b")) "," (Set (Const "c")); assume (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Const "a")) "," (Set (Const "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Const "b")) "," (Set (Const "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; func :::"[$":::"f" "," "g":::"$]"::: -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k20_cat_4 :::"+"::: ) "b") "," "c" means :: CAT_4:def 28 (Bool "(" (Bool (Set it ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k27_cat_4 :::"in1"::: ) "(" "a" "," "b" ")" ")" )) ($#r1_hidden :::"="::: ) "f") & (Bool (Set it ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k28_cat_4 :::"in2"::: ) "(" "a" "," "b" ")" ")" )) ($#r1_hidden :::"="::: ) "g") ")" ); end; :: deftheorem defines :::"[$"::: CAT_4:def 28 : (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_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 "c")) (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 "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 "b7")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b"))) "," (Set (Var "c")) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k29_cat_4 :::"[$"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k29_cat_4 :::"$]"::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "b7")) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k27_cat_4 :::"in1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "b7")) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k28_cat_4 :::"in2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ) ")" )))))); theorem :: CAT_4:66 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_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 (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:67 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k29_cat_4 :::"[$"::: ) (Set "(" ($#k27_cat_4 :::"in1"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set "(" ($#k28_cat_4 :::"in2"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k29_cat_4 :::"$]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")) ")" ))))) ; theorem :: CAT_4:68 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "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 "c")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "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 ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k29_cat_4 :::"[$"::: ) (Set "(" (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k29_cat_4 :::"$]"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set ($#k29_cat_4 :::"[$"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k29_cat_4 :::"$]"::: ) )))))))) ; theorem :: CAT_4:69 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_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 "f")) "," (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "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 ($#k29_cat_4 :::"[$"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k29_cat_4 :::"$]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k29_cat_4 :::"[$"::: ) (Set (Var "k")) "," (Set (Var "h")) ($#k29_cat_4 :::"$]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "h"))) ")" ))))) ; theorem :: CAT_4:70 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) (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 "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 "(" (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) ) "or" (Bool (Set (Var "g")) "is" ($#v8_cat_1 :::"epi"::: ) ) ")" )) "holds" (Bool (Set ($#k29_cat_4 :::"[$"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k29_cat_4 :::"$]"::: ) ) "is" ($#v8_cat_1 :::"epi"::: ) ))))) ; theorem :: CAT_4:71 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "," (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set "(" ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C")) ")" )) ($#r1_cat_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "a")) "," (Set (Set "(" ($#k19_cat_4 :::"[[0]]"::: ) (Set (Var "C")) ")" ) ($#k20_cat_4 :::"+"::: ) (Set (Var "a"))) ($#r1_cat_1 :::"are_isomorphic"::: ) ) ")" ))) ; theorem :: CAT_4:72 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b"))) "," (Set (Set (Var "b")) ($#k20_cat_4 :::"+"::: ) (Set (Var "a"))) ($#r1_cat_1 :::"are_isomorphic"::: ) ))) ; theorem :: CAT_4:73 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")) ")" ) ($#k20_cat_4 :::"+"::: ) (Set (Var "c"))) "," (Set (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k20_cat_4 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_cat_1 :::"are_isomorphic"::: ) ))) ; definitionlet "C" be ($#l2_cat_4 :::"Cocartesian_category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"nabla"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k20_cat_4 :::"+"::: ) "a") "," "a" equals :: CAT_4:def 29 (Set ($#k29_cat_4 :::"[$"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) "a" ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) "a" ")" ) ($#k29_cat_4 :::"$]"::: ) ); end; :: deftheorem defines :::"nabla"::: CAT_4:def 29 : (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k30_cat_4 :::"nabla"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k29_cat_4 :::"[$"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k29_cat_4 :::"$]"::: ) )))); definitionlet "C" be ($#l2_cat_4 :::"Cocartesian_category":::); let "a", "b", "c", "d" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "c")); let "g" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "b")) "," (Set (Const "d")); func "f" :::"+"::: "g" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "a" ($#k20_cat_4 :::"+"::: ) "b") "," (Set "c" ($#k20_cat_4 :::"+"::: ) "d") equals :: CAT_4:def 30 (Set ($#k29_cat_4 :::"[$"::: ) (Set "(" (Set "(" ($#k27_cat_4 :::"in1"::: ) "(" "c" "," "d" ")" ")" ) ($#k5_cat_1 :::"*"::: ) "f" ")" ) "," (Set "(" (Set "(" ($#k28_cat_4 :::"in2"::: ) "(" "c" "," "d" ")" ")" ) ($#k5_cat_1 :::"*"::: ) "g" ")" ) ($#k29_cat_4 :::"$]"::: ) ); end; :: deftheorem defines :::"+"::: CAT_4:def 30 : (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "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 "c")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "d")) "holds" (Bool (Set (Set (Var "f")) ($#k31_cat_4 :::"+"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k29_cat_4 :::"[$"::: ) (Set "(" (Set "(" ($#k27_cat_4 :::"in1"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set "(" ($#k28_cat_4 :::"in2"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k5_cat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k29_cat_4 :::"$]"::: ) )))))); theorem :: CAT_4:74 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (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 "c")) ")" ) ($#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 (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set "(" (Set (Var "c")) ($#k20_cat_4 :::"+"::: ) (Set (Var "d")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_4:75 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k31_cat_4 :::"+"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "a")) ($#k20_cat_4 :::"+"::: ) (Set (Var "b")) ")" ))))) ; theorem :: CAT_4:76 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "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 "c")) (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "d")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "e")) (Bool "for" (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "e")) "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 "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set ($#k29_cat_4 :::"[$"::: ) (Set (Var "g")) "," (Set (Var "k")) ($#k29_cat_4 :::"$]"::: ) ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k31_cat_4 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k29_cat_4 :::"[$"::: ) (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "k")) ($#k5_cat_1 :::"*"::: ) (Set (Var "h")) ")" ) ($#k29_cat_4 :::"$]"::: ) )))))))) ; theorem :: CAT_4:77 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "c")) (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 "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 (Set (Set "(" ($#k30_cat_4 :::"nabla"::: ) (Set (Var "c")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k31_cat_4 :::"+"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k29_cat_4 :::"[$"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k29_cat_4 :::"$]"::: ) )))))) ; theorem :: CAT_4:78 (Bool "for" (Set (Var "C")) "being" ($#l2_cat_4 :::"Cocartesian_category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "s")) "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 "c")) (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "d")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "e")) (Bool "for" (Set (Var "k")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "d")) "," (Set (Var "s")) "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 "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "d")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k31_cat_4 :::"+"::: ) (Set (Var "k")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k31_cat_4 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k31_cat_4 :::"+"::: ) (Set "(" (Set (Var "k")) ($#k5_cat_1 :::"*"::: ) (Set (Var "h")) ")" ))))))))) ;