:: COMMACAT  semantic presentation begin  





































definitionlet "C", "D", "E" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "E")); let "G" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "D")) "," (Set (Const "E")); given "c1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")), "d1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "D")), "f1" being   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "E")) such that 
(Bool (Set (Const "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Const "F"))  ($#k8_cat_1 :::"."::: )  (Set (Const "c1")) ")" ) "," (Set  "(" (Set (Const "G"))  ($#k8_cat_1 :::"."::: )  (Set (Const "d1")) ")" ) ")" ))
 ; func  :::"commaObjs":::  "(" "F" "," "G" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "C") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "D") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "E") ($#k2_zfmisc_1 :::":]"::: ) ) equals :: COMMACAT:def 1  "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where c "is"   ($#m1_subset_1 :::"Object":::) "of" "C", d "is"   ($#m1_subset_1 :::"Object":::) "of" "D", f "is"   ($#m1_subset_1 :::"Morphism":::) "of" "E" : (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" "F"  ($#k8_cat_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" "G"  ($#k8_cat_1 :::"."::: )  (Set (Var "d")) ")" ) ")" ))  "}"  ; end; 










:: deftheorem    defines :::"commaObjs"::: COMMACAT:def 1 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "D")) "," (Set (Var "E"))  "st" (Bool (Bool  "ex" (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool  "ex" (Set (Var "d1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D"))(Bool  "ex" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set (Var "c1")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set (Var "d1")) ")" ) ")" )))))) "holds"  (Bool (Set   ($#k1_commacat :::"commaObjs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where c "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")), d "is"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")), f "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) : (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set (Var "d")) ")" ) ")" ))  "}"  )))); 
 





theorem :: COMMACAT:1 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "D")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "o")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_commacat :::"commaObjs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )  "st" (Bool (Bool  "ex" (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"))(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set (Var "d")) ")" ) ")" )))))) "holds"  (Bool  "("  (Bool (Set (Var "o"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "o"))  ($#k14_domain_1 :::"`11"::: )  ")" ) "," (Set  "(" (Set (Var "o"))  ($#k15_domain_1 :::"`12"::: )  ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set  "(" (Set (Var "o"))  ($#k3_domain_1 :::"`2"::: )  ")" ) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Set (Var "o"))  ($#k3_domain_1 :::"`2"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set  "(" (Set (Var "o"))  ($#k14_domain_1 :::"`11"::: )  ")" ) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set  "(" (Set (Var "o"))  ($#k15_domain_1 :::"`12"::: )  ")" ) ")" ) ")" )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set  "(" (Set (Var "o"))  ($#k3_domain_1 :::"`2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set  "(" (Set (Var "o"))  ($#k14_domain_1 :::"`11"::: )  ")" ))) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set  "(" (Set (Var "o"))  ($#k3_domain_1 :::"`2"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set  "(" (Set (Var "o"))  ($#k15_domain_1 :::"`12"::: )  ")" )))  ")" ))))) ; 
 definitionlet "C", "D", "E" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "E")); let "G" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "D")) "," (Set (Const "E")); given "c1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")), "d1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "D")), "f1" being   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "E")) such that 
(Bool (Set (Const "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Const "F"))  ($#k8_cat_1 :::"."::: )  (Set (Const "c1")) ")" ) "," (Set  "(" (Set (Const "G"))  ($#k8_cat_1 :::"."::: )  (Set (Const "d1")) ")" ) ")" ))
 ; func  :::"commaMorphs":::  "(" "F" "," "G" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  "("  ($#k1_commacat :::"commaObjs"::: )   "(" "F" "," "G" ")"  ")" ) "," (Set  "("  ($#k1_commacat :::"commaObjs"::: )   "(" "F" "," "G" ")"  ")" ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "C") "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "D") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: COMMACAT:def 2  "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) where g "is"   ($#m1_subset_1 :::"Morphism":::) "of" "C", h "is"   ($#m1_subset_1 :::"Morphism":::) "of" "D", o1, o2 "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_commacat :::"commaObjs"::: )   "(" "F" "," "G" ")" ) : (Bool  "("  (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o1"))  ($#k14_domain_1 :::"`11"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o2"))  ($#k14_domain_1 :::"`11"::: )  )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o1"))  ($#k15_domain_1 :::"`12"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o2"))  ($#k15_domain_1 :::"`12"::: )  )) & (Bool (Set (Set  "(" (Set (Var "o2"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" "F"  ($#k3_funct_2 :::"."::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "G"  ($#k3_funct_2 :::"."::: )  (Set (Var "h")) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "o1"))  ($#k3_domain_1 :::"`2"::: )  ")" )))  ")" )  "}"  ; end; 










:: deftheorem    defines :::"commaMorphs"::: COMMACAT:def 2 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "D")) "," (Set (Var "E"))  "st" (Bool (Bool  "ex" (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool  "ex" (Set (Var "d1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D"))(Bool  "ex" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set (Var "c1")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set (Var "d1")) ")" ) ")" )))))) "holds"  (Bool (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ) where g "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")), h "is"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "D")), o1, o2 "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_commacat :::"commaObjs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) : (Bool  "("  (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o1"))  ($#k14_domain_1 :::"`11"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o2"))  ($#k14_domain_1 :::"`11"::: )  )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o1"))  ($#k15_domain_1 :::"`12"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o2"))  ($#k15_domain_1 :::"`12"::: )  )) & (Bool (Set (Set  "(" (Set (Var "o2"))  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_funct_2 :::"."::: )  (Set (Var "h")) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "o1"))  ($#k3_domain_1 :::"`2"::: )  ")" )))  ")" )  "}"  )))); 
 





definitionlet "C", "D", "E" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "E")); let "G" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "D")) "," (Set (Const "E")); let "k" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Const "F")) "," (Set (Const "G")) ")" ); :: original: :::"`11"::: redefine func "k" :::"`11":::  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_commacat :::"commaObjs"::: )   "(" "F" "," "G" ")" ); :: original: :::"`12"::: redefine func "k" :::"`12":::  ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k1_commacat :::"commaObjs"::: )   "(" "F" "," "G" ")" ); end; 
theorem :: COMMACAT:2 (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "D")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )  "st" (Bool (Bool  "ex" (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"))(Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set (Var "c")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set (Var "d")) ")" ) ")" )))))) "holds"  (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "k"))  ($#k3_commacat :::"`11"::: )  ")" ) "," (Set  "(" (Set (Var "k"))  ($#k4_commacat :::"`12"::: )  ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "k"))  ($#k16_domain_1 :::"`21"::: )  ")" ) "," (Set  "(" (Set (Var "k"))  ($#k17_domain_1 :::"`22"::: )  ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set  "(" (Set (Var "k"))  ($#k16_domain_1 :::"`21"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k3_commacat :::"`11"::: )  ")" )  ($#k14_domain_1 :::"`11"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set  "(" (Set (Var "k"))  ($#k16_domain_1 :::"`21"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k4_commacat :::"`12"::: )  ")" )  ($#k14_domain_1 :::"`11"::: )  )) & (Bool (Set   ($#k3_graph_1 :::"dom"::: )  (Set  "(" (Set (Var "k"))  ($#k17_domain_1 :::"`22"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k3_commacat :::"`11"::: )  ")" )  ($#k15_domain_1 :::"`12"::: )  )) & (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set  "(" (Set (Var "k"))  ($#k17_domain_1 :::"`22"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k4_commacat :::"`12"::: )  ")" )  ($#k15_domain_1 :::"`12"::: )  )) & (Bool (Set (Set  "(" (Set  "(" (Set (Var "k"))  ($#k4_commacat :::"`12"::: )  ")" )  ($#k3_domain_1 :::"`2"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "F"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k16_domain_1 :::"`21"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "G"))  ($#k3_funct_2 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k17_domain_1 :::"`22"::: )  ")" ) ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set  "(" (Set (Var "k"))  ($#k3_commacat :::"`11"::: )  ")" )  ($#k3_domain_1 :::"`2"::: )  ")" )))  ")" ))))) ; 
 definitionlet "C", "D", "E" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "E")); let "G" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "D")) "," (Set (Const "E")); let "k1", "k2" be    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Const "F")) "," (Set (Const "G")) ")" ); given "c1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")), "d1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "D")), "f1" being   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "E")) such that 
(Bool (Set (Const "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Const "F"))  ($#k8_cat_1 :::"."::: )  (Set (Const "c1")) ")" ) "," (Set  "(" (Set (Const "G"))  ($#k8_cat_1 :::"."::: )  (Set (Const "d1")) ")" ) ")" ))
 ; assume 
(Bool (Set (Set (Const "k1"))  ($#k4_commacat :::"`12"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Const "k2"))  ($#k3_commacat :::"`11"::: )  ))
 ; func "k2" :::"*"::: "k1" ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")" ) equals :: COMMACAT:def 3 (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" "k1"  ($#k3_commacat :::"`11"::: )  ")" ) "," (Set  "(" "k2"  ($#k4_commacat :::"`12"::: )  ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" "k2"  ($#k16_domain_1 :::"`21"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" "k1"  ($#k16_domain_1 :::"`21"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" "k2"  ($#k17_domain_1 :::"`22"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" "k1"  ($#k17_domain_1 :::"`22"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) ); end; 












:: deftheorem    defines :::"*"::: COMMACAT:def 3 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "D")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )  "st" (Bool (Bool  "ex" (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool  "ex" (Set (Var "d1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D"))(Bool  "ex" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set (Var "c1")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set (Var "d1")) ")" ) ")" ))))) & (Bool (Set (Set (Var "k1"))  ($#k4_commacat :::"`12"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "k2"))  ($#k3_commacat :::"`11"::: )  ))) "holds"  (Bool (Set (Set (Var "k2"))  ($#k5_commacat :::"*"::: )  (Set (Var "k1")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set (Var "k1"))  ($#k3_commacat :::"`11"::: )  ")" ) "," (Set  "(" (Set (Var "k2"))  ($#k4_commacat :::"`12"::: )  ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set  ($#k1_domain_1 :::"["::: ) (Set  "(" (Set  "(" (Set (Var "k2"))  ($#k16_domain_1 :::"`21"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "k1"))  ($#k16_domain_1 :::"`21"::: )  ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "k2"))  ($#k17_domain_1 :::"`22"::: )  ")" )  ($#k1_cat_1 :::"(*)"::: )  (Set  "(" (Set (Var "k1"))  ($#k17_domain_1 :::"`22"::: )  ")" ) ")" ) ($#k1_domain_1 :::"]"::: ) ) ($#k1_domain_1 :::"]"::: ) )))))); 
 definitionlet "C", "D", "E" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "E")); let "G" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "D")) "," (Set (Const "E")); func  :::"commaComp":::  "(" "F" "," "G" ")"  ->   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  "("  ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")"  ")" ) "," (Set  "("  ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")"  ")" ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set  "("  ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")"  ")" ) means :: COMMACAT:def 4 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "k1")) "," (Set (Var "k2")) ($#k1_domain_1 :::"]"::: ) ) where k1, k2 "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")" ) : (Bool (Set (Set (Var "k1"))  ($#k3_commacat :::"`11"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "k2"))  ($#k4_commacat :::"`12"::: )  ))  "}"  ) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "k9")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")" )  "st" (Bool (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "k")) "," (Set (Var "k9")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "k")) "," (Set (Var "k9")) ($#k1_domain_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_commacat :::"*"::: )  (Set (Var "k9"))))  ")" )  ")" ); end; 









:: deftheorem    defines :::"commaComp"::: COMMACAT:def 4 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "D")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "b6")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set  ($#k8_mcart_1 :::"[:"::: ) (Set  "("  ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")"  ")" ) "," (Set  "("  ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")"  ")" ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set  "("  ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_commacat :::"commaComp"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b6")))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "k1")) "," (Set (Var "k2")) ($#k1_domain_1 :::"]"::: ) ) where k1, k2 "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) : (Bool (Set (Set (Var "k1"))  ($#k3_commacat :::"`11"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "k2"))  ($#k4_commacat :::"`12"::: )  ))  "}"  ) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "k9")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )  "st" (Bool (Bool (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "k")) "," (Set (Var "k9")) ($#k1_domain_1 :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b6"))))) "holds"  (Bool (Set (Set (Var "b6"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_domain_1 :::"["::: ) (Set (Var "k")) "," (Set (Var "k9")) ($#k1_domain_1 :::"]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k5_commacat :::"*"::: )  (Set (Var "k9"))))  ")" )  ")" )  ")" ))))); 
 definitionlet "C", "D", "E" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "E")); let "G" be    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Const "D")) "," (Set (Const "E")); given "c1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")), "d1" being   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "D")), "f1" being   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "E")) such that 
(Bool (Set (Const "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Const "F"))  ($#k8_cat_1 :::"."::: )  (Set (Const "c1")) ")" ) "," (Set  "(" (Set (Const "G"))  ($#k8_cat_1 :::"."::: )  (Set (Const "d1")) ")" ) ")" ))
 ; func "F" :::"comma"::: "G" ->   ($#v1_cat_1 :::"strict"::: )    ($#l1_cat_1 :::"Category":::) means :: COMMACAT:def 5 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_commacat :::"commaObjs"::: )   "(" "F" "," "G" ")" )) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")" ) "holds"  (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" it)  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k3_commacat :::"`11"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" "F" "," "G" ")" ) "holds"  (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" it)  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_commacat :::"`12"::: )  ))  ")" ) & (Bool (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k6_commacat :::"commaComp"::: )   "(" "F" "," "G" ")" ))  ")" ); end; 










:: deftheorem    defines :::"comma"::: COMMACAT:def 5 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "E"))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "D")) "," (Set (Var "E"))  "st" (Bool (Bool  "ex" (Set (Var "c1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C"))(Bool  "ex" (Set (Var "d1")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D"))(Bool  "ex" (Set (Var "f1")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "E")) "st" (Bool (Set (Var "f1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "(" (Set (Var "F"))  ($#k8_cat_1 :::"."::: )  (Set (Var "c1")) ")" ) "," (Set  "(" (Set (Var "G"))  ($#k8_cat_1 :::"."::: )  (Set (Var "d1")) ")" ) ")" )))))) "holds"  (Bool  "for" (Set (Var "b6")) "being"   ($#v1_cat_1 :::"strict"::: )    ($#l1_cat_1 :::"Category":::) "holds"   (Bool  "("  (Bool (Set (Var "b6"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k7_commacat :::"comma"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b6")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_commacat :::"commaObjs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "b6")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) "holds"  (Bool (Set (Set  "the"  ($#u1_graph_1 :::"Source"::: )  "of" (Set (Var "b6")))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k3_commacat :::"`11"::: )  ))  ")" ) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k2_commacat :::"commaMorphs"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" ) "holds"  (Bool (Set (Set  "the"  ($#u2_graph_1 :::"Target"::: )  "of" (Set (Var "b6")))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k4_commacat :::"`12"::: )  ))  ")" ) & (Bool (Set  "the"  ($#u1_cat_1 :::"Comp"::: )  "of" (Set (Var "b6")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_commacat :::"commaComp"::: )   "(" (Set (Var "F")) "," (Set (Var "G")) ")" ))  ")" )  ")" ))))); 
 
theorem :: COMMACAT:3 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k3_cat_1 :::"1Cat"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set  "("  ($#k3_cat_1 :::"1Cat"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ")" )) ; 
 
theorem :: COMMACAT:4 (Bool  "for" (Set (Var "y")) "," (Set (Var "x")) "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 "x")) "," (Set (Var "y")) ")"  ")" ) "holds"  (Bool (Set   ($#k2_cat_1 :::"Hom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))) ; 
 definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "c" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func  :::"1Cat"::: "c" ->   ($#v1_cat_1 :::"strict"::: )     ($#m3_cat_2 :::"Subcategory"::: )   "of" "C" equals :: COMMACAT:def 6 (Set   ($#k3_cat_1 :::"1Cat"::: )   "(" "c" "," (Set  "("  ($#k4_cat_1 :::"id"::: )  "c" ")" ) ")" ); end; 






:: deftheorem    defines :::"1Cat"::: COMMACAT:def 6 :  (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   ($#k8_commacat :::"1Cat"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_cat_1 :::"1Cat"::: )   "(" (Set (Var "c")) "," (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "c")) ")" ) ")" )))); 
 definitionlet "C" be   ($#l1_cat_1 :::"Category":::); let "c" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "C")); func "c" :::"comma"::: "C" ->   ($#v1_cat_1 :::"strict"::: )    ($#l1_cat_1 :::"Category":::) equals :: COMMACAT:def 7 (Set (Set  "("  ($#k5_cat_2 :::"incl"::: )  (Set  "("  ($#k8_commacat :::"1Cat"::: )  "c" ")" ) ")" )  ($#k7_commacat :::"comma"::: )  (Set  "("  ($#k10_cat_1 :::"id"::: )  "C" ")" )); func "C" :::"comma"::: "c" ->   ($#v1_cat_1 :::"strict"::: )    ($#l1_cat_1 :::"Category":::) equals :: COMMACAT:def 8 (Set (Set  "("  ($#k10_cat_1 :::"id"::: )  "C" ")" )  ($#k7_commacat :::"comma"::: )  (Set  "("  ($#k5_cat_2 :::"incl"::: )  (Set  "("  ($#k8_commacat :::"1Cat"::: )  "c" ")" ) ")" )); end; 












:: deftheorem    defines :::"comma"::: COMMACAT:def 7 :  (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 (Var "c"))  ($#k9_commacat :::"comma"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_cat_2 :::"incl"::: )  (Set  "("  ($#k8_commacat :::"1Cat"::: )  (Set (Var "c")) ")" ) ")" )  ($#k7_commacat :::"comma"::: )  (Set  "("  ($#k10_cat_1 :::"id"::: )  (Set (Var "C")) ")" ))))); 
 
:: deftheorem    defines :::"comma"::: COMMACAT:def 8 :  (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 (Var "C"))  ($#k10_commacat :::"comma"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_cat_1 :::"id"::: )  (Set (Var "C")) ")" )  ($#k7_commacat :::"comma"::: )  (Set  "("  ($#k5_cat_2 :::"incl"::: )  (Set  "("  ($#k8_commacat :::"1Cat"::: )  (Set (Var "c")) ")" ) ")" )))));