:: CAT_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"CatStr"::: -> ($#l1_graph_1 :::"MultiGraphStruct"::: ) ; aggr :::"CatStr":::(# :::"carrier":::, :::"carrier'":::, :::"Source":::, :::"Target":::, :::"Comp"::: #) -> ($#l1_cat_1 :::"CatStr"::: ) ; sel :::"Comp"::: "c1" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "c1"); end; definitionlet "C" be ($#l1_cat_1 :::"CatStr"::: ) ; mode Object of "C" is ($#m1_subset_1 :::"Element":::) "of" "C"; mode Morphism of "C" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) for ($#l1_cat_1 :::"CatStr"::: ) ; end; definitionlet "C" be ($#l1_cat_1 :::"CatStr"::: ) ; let "f", "g" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); assume (Bool (Set ($#k4_tarski :::"["::: ) (Set (Const "g")) "," (Set (Const "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Const "C"))))) ; func "g" :::"(*)"::: "f" -> ($#m1_subset_1 :::"Morphism":::) "of" "C" equals :: CAT_1:def 1 (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C") ($#k1_binop_1 :::"."::: ) "(" "g" "," "f" ")" ); end; :: deftheorem defines :::"(*)"::: CAT_1:def 1 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"CatStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C")))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))); definitioncanceled; canceled; let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"Hom"::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") equals :: CAT_1:def 4 "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Morphism":::) "of" "C" : (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "a") & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "b") ")" ) "}" ; end; :: deftheorem CAT_1:def 2 : canceled; :: deftheorem CAT_1:def 3 : canceled; :: deftheorem defines :::"Hom"::: CAT_1: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_1 :::"CatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set (Var "f")) where f "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) : (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) "}" ))); theorem :: CAT_1:1 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" ) ")" )))) ; theorem :: CAT_1:2 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); assume (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Const "a")) "," (Set (Const "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; mode :::"Morphism"::: "of" "a" "," "b" -> ($#m1_subset_1 :::"Morphism":::) "of" "C" means :: CAT_1:def 5 (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," "b" ")" )); end; :: deftheorem defines :::"Morphism"::: CAT_1: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_1 :::"CatStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool (Set (Var "b4")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) ")" )))); theorem :: CAT_1:3 canceled; theorem :: CAT_1: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_1 :::"CatStr"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Var "f")) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) "," (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))))) ; theorem :: CAT_1: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_1 :::"CatStr"::: ) (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 "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" )))) ; theorem :: CAT_1: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_1 :::"CatStr"::: ) (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 "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 "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 (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "h")))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ))))) ; theorem :: CAT_1:7 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) (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_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))))) ; theorem :: CAT_1:8 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) (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 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" )) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: CAT_1:9 (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) (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")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "," (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r2_tarski :::"are_equipotent"::: ) ) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "d")) "st" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "h")) ($#k1_tarski :::"}"::: ) )))))) ; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) ; attr "C" is :::"Category-like"::: means :: CAT_1:def 6 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C"))) "iff" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) ")" )); attr "C" is :::"transitive"::: means :: CAT_1:def 7 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")))) ")" )); attr "C" is :::"associative"::: means :: CAT_1:def 8 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))); attr "C" is :::"reflexive"::: means :: CAT_1:def 9 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "C" "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); attr "C" is :::"with_identities"::: means :: CAT_1:def 10 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "C" (Bool "ex" (Set (Var "i")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" "C" "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "holds" (Bool (Set (Set (Var "i")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" ")" )))); end; :: deftheorem defines :::"Category-like"::: CAT_1: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_1 :::"CatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v2_cat_1 :::"Category-like"::: ) ) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))))) "iff" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) ")" )) ")" )); :: deftheorem defines :::"transitive"::: CAT_1:def 7 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v3_cat_1 :::"transitive"::: ) ) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")))) ")" )) ")" )); :: deftheorem defines :::"associative"::: CAT_1:def 8 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v4_cat_1 :::"associative"::: ) ) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))))) ")" )); :: deftheorem defines :::"reflexive"::: CAT_1:def 9 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v5_cat_1 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )); :: deftheorem defines :::"with_identities"::: CAT_1:def 10 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_cat_1 :::"CatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v6_cat_1 :::"with_identities"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "i")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "st" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ")" & "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "holds" (Bool (Set (Set (Var "i")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" ")" )))) ")" )); definitionlet "o", "m" be ($#m1_hidden :::"set"::: ) ; func :::"1Cat"::: "(" "o" "," "m" ")" -> ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"CatStr"::: ) equals :: CAT_1:def 11 (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (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" ")" ) "#)" ); end; :: deftheorem defines :::"1Cat"::: CAT_1:def 11 : (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (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")) ")" ) "#)" ))); registrationlet "o", "m" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_cat_1 :::"1Cat"::: ) "(" "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'"::: ) ($#v1_cat_1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v3_cat_1 :::"transitive"::: ) ($#v5_cat_1 :::"reflexive"::: ) for ($#l1_cat_1 :::"CatStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v15_struct_0 :::"trivial'"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v4_cat_1 :::"associative"::: ) ($#v6_cat_1 :::"with_identities"::: ) for ($#l1_cat_1 :::"CatStr"::: ) ; end; registrationlet "o", "m" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k3_cat_1 :::"1Cat"::: ) "(" "o" "," "m" ")" ) -> ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v1_cat_1 :::"strict"::: ) ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) for ($#l1_cat_1 :::"CatStr"::: ) ; end; definitionmode 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"::: ) ($#l1_cat_1 :::"CatStr"::: ) ; end; registrationlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_cat_1 :::"reflexive"::: ) ($#l1_cat_1 :::"CatStr"::: ) ; let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); cluster (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," "a" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#l1_cat_1 :::"CatStr"::: ) ; let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"id"::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," "a" means :: CAT_1:def 12 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) it) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" & "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," "a" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," "a" "holds" (Bool (Set it ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" ")" )); end; :: deftheorem defines :::"id"::: CAT_1:def 12 : (Bool "for" (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#l1_cat_1 :::"CatStr"::: ) (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 (Var "a")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "f")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" & "(" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ")" ")" )) ")" )))); theorem :: CAT_1:10 canceled; theorem :: CAT_1:11 (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 "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (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_1:12 (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 "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (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_1:13 (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 "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (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_1:14 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) (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 (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))))) ; theorem :: CAT_1:15 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))))) ")" ))) ; theorem :: CAT_1:16 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: CAT_1:17 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")))) ")" ))) ; theorem :: CAT_1:18 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")))) & (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")))))) ; theorem :: CAT_1:19 canceled; theorem :: CAT_1:20 canceled; theorem :: CAT_1:21 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: CAT_1:22 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g")))))) ; theorem :: CAT_1:23 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )))))) ; definitionlet "C" be ($#l1_cat_1 :::"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 "b")); 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 "b")) ")" ) ($#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 "g" :::"*"::: "f" -> ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," "c" equals :: CAT_1:def 13 (Set "g" ($#k1_cat_1 :::"(*)"::: ) "f"); end; :: deftheorem defines :::"*"::: CAT_1:def 13 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")))))))); theorem :: CAT_1:24 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: CAT_1:25 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"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 "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 "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" )))))))) ; theorem :: CAT_1:26 canceled; theorem :: CAT_1:27 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" )))) ; theorem :: CAT_1:28 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: CAT_1:29 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "b")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g")))))) ; registrationlet "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "a")); reduce ; reduce ; end; theorem :: CAT_1:30 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "b", "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "g" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "b")) "," (Set (Const "c")); attr "g" is :::"monic"::: means :: CAT_1:def 14 (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "b" "," "c" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," "b" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," "b" "st" (Bool (Bool (Set "g" ($#k5_cat_1 :::"*"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set "g" ($#k5_cat_1 :::"*"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2")))) ")" ) ")" ); end; :: deftheorem defines :::"monic"::: CAT_1:def 14 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v7_cat_1 :::"monic"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2")))) ")" ) ")" ) ")" )))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); attr "f" is :::"epi"::: means :: CAT_1:def 15 (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," "b" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "b" "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," (Set (Var "c")) "st" (Bool (Bool (Set (Set (Var "g1")) ($#k5_cat_1 :::"*"::: ) "f") ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k5_cat_1 :::"*"::: ) "f"))) "holds" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) ")" ) ")" ); end; :: deftheorem defines :::"epi"::: CAT_1:def 15 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Set (Var "g1")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2")))) ")" ) ")" ) ")" )))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); attr "f" is :::"invertible"::: means :: CAT_1:def 16 (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," "b" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "b" "," "a" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," "a" "st" (Bool "(" (Bool (Set "f" ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "b")) & (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "a")) ")" )) ")" ); end; :: deftheorem defines :::"invertible"::: CAT_1:def 16 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) ")" )) ")" ) ")" )))); theorem :: CAT_1:31 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "g")) "is" ($#v7_cat_1 :::"monic"::: ) ) "iff" (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 (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ")" )))) ; theorem :: CAT_1:32 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (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 (Var "g")) "is" ($#v7_cat_1 :::"monic"::: ) ) & (Bool (Set (Var "h")) "is" ($#v7_cat_1 :::"monic"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) "is" ($#v7_cat_1 :::"monic"::: ) ))))) ; theorem :: CAT_1:33 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (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 "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 :::"{}"::: ) )) & (Bool (Set (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) "is" ($#v7_cat_1 :::"monic"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v7_cat_1 :::"monic"::: ) ))))) ; theorem :: CAT_1:34 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "g")) "is" ($#v7_cat_1 :::"monic"::: ) ))))) ; theorem :: CAT_1:35 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b"))) "is" ($#v7_cat_1 :::"monic"::: ) ))) ; theorem :: CAT_1:36 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) ) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "g1")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g2")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2"))))) ")" )))) ; theorem :: CAT_1:37 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) ) & (Bool (Set (Var "g")) "is" ($#v8_cat_1 :::"epi"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#v8_cat_1 :::"epi"::: ) ))))) ; theorem :: CAT_1:38 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#v8_cat_1 :::"epi"::: ) )) "holds" (Bool (Set (Var "g")) "is" ($#v8_cat_1 :::"epi"::: ) ))))) ; theorem :: CAT_1:39 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "h")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "h")) "is" ($#v8_cat_1 :::"epi"::: ) ))))) ; theorem :: CAT_1:40 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b"))) "is" ($#v8_cat_1 :::"epi"::: ) ))) ; theorem :: CAT_1:41 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) ")" )) ")" ) ")" )))) ; theorem :: CAT_1:42 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#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 "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "g1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "g2")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))))) "holds" (Bool (Set (Var "g1")) ($#r1_hidden :::"="::: ) (Set (Var "g2"))))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a", "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); let "f" be ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); assume (Bool (Set (Const "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ) ; func "f" :::"""::: -> ($#m1_cat_1 :::"Morphism"::: ) "of" "b" "," "a" means :: CAT_1:def 17 (Bool "(" (Bool (Set "f" ($#k5_cat_1 :::"*"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "b")) & (Bool (Set it ($#k5_cat_1 :::"*"::: ) "f") ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) "a")) ")" ); end; :: deftheorem defines :::"""::: CAT_1:def 17 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_cat_1 :::"""::: ) )) "iff" (Bool "(" (Bool (Set (Set (Var "f")) ($#k5_cat_1 :::"*"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b")))) & (Bool (Set (Set (Var "b5")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))) ")" ) ")" ))))); theorem :: CAT_1:43 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_cat_1 :::"monic"::: ) ) & (Bool (Set (Var "f")) "is" ($#v8_cat_1 :::"epi"::: ) ) ")" )))) ; theorem :: CAT_1:44 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) "is" ($#v9_cat_1 :::"invertible"::: ) ))) ; theorem :: CAT_1:45 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ) & (Bool (Set (Var "g")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#v9_cat_1 :::"invertible"::: ) ))))) ; theorem :: CAT_1:46 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k6_cat_1 :::"""::: ) ) "is" ($#v9_cat_1 :::"invertible"::: ) )))) ; theorem :: CAT_1:47 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "c")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ) & (Bool (Set (Var "g")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k6_cat_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k6_cat_1 :::"""::: ) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k6_cat_1 :::"""::: ) ")" ))))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); attr "a" is :::"terminal"::: means :: CAT_1:def 18 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "b")) "," "a" ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," "a" "st" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," "a" "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ")" )); attr "a" is :::"initial"::: means :: CAT_1:def 19 (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" "a" "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set (Var "b")) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," (Set (Var "b")) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ")" )); let "b" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); pred "a" "," "b" :::"are_isomorphic"::: means :: CAT_1:def 20 (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" "a" "," "b" "st" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )); reflexivity (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")) (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "st" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ))) ; symmetry (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")) "st" (Bool (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "st" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) ))) ; end; :: deftheorem defines :::"terminal"::: CAT_1:def 18 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (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 "b")) "," (Set (Var "a")) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "b")) "," (Set (Var "a")) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ")" )) ")" ))); :: deftheorem defines :::"initial"::: CAT_1:def 19 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ")" )) ")" ))); :: deftheorem defines :::"are_isomorphic"::: CAT_1:def 20 : (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 "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) ")" ))); theorem :: CAT_1:48 (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")))) ")" ))) ")" ) ")" ))) ; theorem :: CAT_1:49 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ) "iff" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )))) ")" ))) ; theorem :: CAT_1:50 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))))) ; theorem :: CAT_1:51 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ) & (Bool (Set (Var "b")) "is" ($#v11_cat_1 :::"initial"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_cat_1 :::"are_isomorphic"::: ) ))) ; theorem :: CAT_1:52 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v11_cat_1 :::"initial"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_cat_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "b")) "is" ($#v11_cat_1 :::"initial"::: ) ))) ; theorem :: CAT_1:53 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b")) "is" ($#v10_cat_1 :::"terminal"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )))) ")" ))) ; theorem :: CAT_1:54 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "a")) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))))) ; theorem :: CAT_1:55 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) ) & (Bool (Set (Var "b")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_cat_1 :::"are_isomorphic"::: ) ))) ; theorem :: CAT_1:56 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "b")) "is" ($#v10_cat_1 :::"terminal"::: ) ) & (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_cat_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) ))) ; theorem :: CAT_1:57 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "a")) "is" ($#v10_cat_1 :::"terminal"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v7_cat_1 :::"monic"::: ) )))) ; registrationlet "C" be ($#l1_cat_1 :::"Category":::); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); reduce ; reduce ; end; theorem :: CAT_1:58 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" ))) ; theorem :: CAT_1:59 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))) ; theorem :: CAT_1:60 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) ($#r1_cat_1 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "b")) "," (Set (Var "c")) ($#r1_cat_1 :::"are_isomorphic"::: ) )) "holds" (Bool (Set (Var "a")) "," (Set (Var "c")) ($#r1_cat_1 :::"are_isomorphic"::: ) ))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); mode :::"Functor"::: "of" "C" "," "D" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "D") means :: CAT_1:def 21 (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "C" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "D" "st" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Functor"::: CAT_1:def 21 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C")))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" ) ")" ) ")" ))); theorem :: CAT_1:61 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D"))))) ; theorem :: CAT_1:62 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d")))))))) ; theorem :: CAT_1:63 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" )))) ; theorem :: CAT_1:64 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: CAT_1:65 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")))))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Const "D"))); assume (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "D")) "st" (Bool (Set (Set (Const "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d")))))) ; func :::"Obj"::: "F" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "D") means :: CAT_1:def 22 (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" "C" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" "D" "st" (Bool (Bool (Set "F" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))); end; :: deftheorem defines :::"Obj"::: CAT_1:def 22 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D"))) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ")" )))); theorem :: CAT_1:66 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D"))) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" )) "holds" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: CAT_1:67 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: CAT_1:68 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" )))))) ; theorem :: CAT_1:69 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" )))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); let "T" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); let "c" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "T" :::"."::: "c" -> ($#m1_subset_1 :::"Object":::) "of" "D" equals :: CAT_1:def 23 (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) "T" ")" ) ($#k3_funct_2 :::"."::: ) "c"); end; :: deftheorem defines :::"."::: CAT_1:def 23 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))))))); theorem :: CAT_1:70 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: CAT_1:71 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" )))))) ; theorem :: CAT_1:72 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: CAT_1:73 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "S")) ($#k1_partfun1 :::"*"::: ) (Set (Var "T"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "D")))))) ; definitionlet "B", "C", "D" be ($#l1_cat_1 :::"Category":::); let "T" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); let "S" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"*"::: redefine func "S" :::"*"::: "T" -> ($#m2_cat_1 :::"Functor"::: ) "of" "B" "," "D"; end; theorem :: CAT_1:74 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C")))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "C")))) ; theorem :: CAT_1:75 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set (Var "S")) ($#k9_cat_1 :::"*"::: ) (Set (Var "T")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "S")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ))))))) ; theorem :: CAT_1:76 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k9_cat_1 :::"*"::: ) (Set (Var "T")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k8_cat_1 :::"."::: ) (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "b")) ")" ))))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"id"::: "C" -> ($#m2_cat_1 :::"Functor"::: ) "of" "C" "," "C" equals :: CAT_1:def 24 (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C")); end; :: deftheorem defines :::"id"::: CAT_1:def 24 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C")))))); theorem :: CAT_1:77 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "C")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; theorem :: CAT_1:78 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k7_cat_1 :::"Obj"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "C")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))))) ; theorem :: CAT_1:79 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "C")) ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); let "T" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); attr "T" is :::"isomorphic"::: means :: CAT_1:def 25 (Bool "(" (Bool "T" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "T") ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "D")) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_cat_1 :::"Obj"::: ) "T" ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "D")) ")" ); attr "T" is :::"full"::: means :: CAT_1:def 26 (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" "T" ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" "T" ($#k8_cat_1 :::"."::: ) (Set (Var "c9")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "T" ($#k8_cat_1 :::"."::: ) (Set (Var "c"))) "," (Set "T" ($#k8_cat_1 :::"."::: ) (Set (Var "c9"))) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "c9")) "st" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "T" ($#k3_funct_2 :::"."::: ) (Set (Var "f"))))) ")" ))); attr "T" is :::"faithful"::: means :: CAT_1:def 27 (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "c9")) "st" (Bool (Bool (Set "T" ($#k3_funct_2 :::"."::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set "T" ($#k3_funct_2 :::"."::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))); end; :: deftheorem defines :::"isomorphic"::: CAT_1:def 25 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v12_cat_1 :::"isomorphic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "T")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "D")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "D")))) ")" ) ")" ))); :: deftheorem defines :::"full"::: CAT_1:def 26 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v13_cat_1 :::"full"::: ) ) "iff" (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c"))) "," (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9"))) "holds" (Bool "(" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "c9")) "st" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))))) ")" ))) ")" ))); :: deftheorem defines :::"faithful"::: CAT_1:def 27 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v14_cat_1 :::"faithful"::: ) ) "iff" (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "c9")) "st" (Bool (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ")" ))); theorem :: CAT_1:80 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "C"))) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) ; theorem :: CAT_1:81 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ))) "holds" (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9")) ")" ) ")" )))))) ; theorem :: CAT_1:82 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "c9")) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9")) ")" ) ")" )))))) ; theorem :: CAT_1:83 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "c9")) "holds" (Bool (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c"))) "," (Set (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9")))))))) ; theorem :: CAT_1:84 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: CAT_1:85 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v13_cat_1 :::"full"::: ) ) & (Bool (Set (Var "S")) "is" ($#v13_cat_1 :::"full"::: ) )) "holds" (Bool (Set (Set (Var "S")) ($#k9_cat_1 :::"*"::: ) (Set (Var "T"))) "is" ($#v13_cat_1 :::"full"::: ) )))) ; theorem :: CAT_1:86 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "S")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v14_cat_1 :::"faithful"::: ) ) & (Bool (Set (Var "S")) "is" ($#v14_cat_1 :::"faithful"::: ) )) "holds" (Bool (Set (Set (Var "S")) ($#k9_cat_1 :::"*"::: ) (Set (Var "T"))) "is" ($#v14_cat_1 :::"faithful"::: ) )))) ; theorem :: CAT_1:87 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "T")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9")) ")" ) ")" ))))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); let "T" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); let "c", "c9" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func :::"hom"::: "(" "T" "," "c" "," "c9" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" "c" "," "c9" ")" ")" ) "," (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" "T" ($#k8_cat_1 :::"."::: ) "c" ")" ) "," (Set "(" "T" ($#k8_cat_1 :::"."::: ) "c9" ")" ) ")" ")" ) equals :: CAT_1:def 28 (Set "T" ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" "c" "," "c9" ")" ")" )); end; :: deftheorem defines :::"hom"::: CAT_1:def 28 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k11_cat_1 :::"hom"::: ) "(" (Set (Var "T")) "," (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ")" )))))); theorem :: CAT_1:88 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c")) "," (Set (Var "c9")) "holds" (Bool (Set (Set "(" ($#k11_cat_1 :::"hom"::: ) "(" (Set (Var "T")) "," (Set (Var "c")) "," (Set (Var "c9")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")))))))) ; theorem :: CAT_1:89 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v13_cat_1 :::"full"::: ) ) "iff" (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k11_cat_1 :::"hom"::: ) "(" (Set (Var "T")) "," (Set (Var "c")) "," (Set (Var "c9")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "T")) ($#k8_cat_1 :::"."::: ) (Set (Var "c9")) ")" ) ")" ))) ")" ))) ; theorem :: CAT_1:90 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "T")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v14_cat_1 :::"faithful"::: ) ) "iff" (Bool "for" (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set ($#k11_cat_1 :::"hom"::: ) "(" (Set (Var "T")) "," (Set (Var "c")) "," (Set (Var "c9")) ")" ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ")" ))) ;