:: YONEDA_1  semantic presentation begin  












definitionlet "A" be   ($#l1_cat_1 :::"Category":::); func  :::"EnsHom"::: "A" ->   ($#l1_cat_1 :::"Category":::) equals :: YONEDA_1:def 1 (Set   ($#k11_ens_1 :::"Ens"::: )  (Set  "("  ($#k16_ens_1 :::"Hom"::: )  "A" ")" )); end; 





:: deftheorem    defines :::"EnsHom"::: YONEDA_1:def 1 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::) "holds"  (Bool (Set   ($#k1_yoneda_1 :::"EnsHom"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k11_ens_1 :::"Ens"::: )  (Set  "("  ($#k16_ens_1 :::"Hom"::: )  (Set (Var "A")) ")" )))); 
 
theorem :: YONEDA_1:1 (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "m1")) "," (Set (Var "m2")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set  "("  ($#k1_yoneda_1 :::"EnsHom"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set   ($#k4_graph_1 :::"cod"::: )  (Set (Var "m1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_graph_1 :::"dom"::: )  (Set (Var "m2")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k9_cat_2 :::"["::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "m1")) ")" ) "," (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "m1")) ")" ) ($#k9_cat_2 :::"]"::: ) ) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "m1"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k9_cat_2 :::"["::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "m2")) ")" ) "," (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "m2")) ")" ) ($#k9_cat_2 :::"]"::: ) ) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Var "m2")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k9_cat_2 :::"["::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "m1")) ")" ) "," (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "m2")) ")" ) ($#k9_cat_2 :::"]"::: ) ) "," (Set  "(" (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set (Var "m2"))  ($#k1_cat_1 :::"(*)"::: )  (Set (Var "m1"))))))) ; 
 definitionlet "A" be   ($#l1_cat_1 :::"Category":::); let "a" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")); func :::"<|":::"a":::",?>"::: ->    ($#m2_cat_1 :::"Functor"::: )   "of" "A" "," (Set   ($#k1_yoneda_1 :::"EnsHom"::: )  "A") equals :: YONEDA_1:def 2 (Set   ($#k19_ens_1 :::"hom?-"::: )  "a"); end; 






:: deftheorem    defines :::"<|"::: YONEDA_1:def 2 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds"  (Bool (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set (Var "a")) ($#k2_yoneda_1 :::",?>"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k19_ens_1 :::"hom?-"::: )  (Set (Var "a")))))); 
 
theorem :: YONEDA_1:2 (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds"  (Bool (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) )  ($#r2_nattra_1 :::"is_naturally_transformable_to"::: )  (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) )))) ; 
 definitionlet "A" be   ($#l1_cat_1 :::"Category":::); let "f" be   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "A")); func :::"<|":::"f":::",?>"::: ->    ($#m2_nattra_1 :::"natural_transformation"::: )   "of" (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k4_graph_1 :::"cod"::: )  "f" ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) "," (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  "f" ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) means :: YONEDA_1:def 3 (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" "A" "holds"  (Bool (Set it  ($#k4_nattra_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "("  ($#k4_graph_1 :::"cod"::: )  "f" ")" ) "," (Set (Var "o")) ")"  ")" ) "," (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "("  ($#k3_graph_1 :::"dom"::: )  "f" ")" ) "," (Set (Var "o")) ")"  ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set  "("  ($#k21_ens_1 :::"hom"::: )   "(" "f" "," (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "o")) ")" ) ")"  ")" ) ($#k4_tarski :::"]"::: ) ))); end; 






:: deftheorem    defines :::"<|"::: YONEDA_1:def 3 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m2_nattra_1 :::"natural_transformation"::: )   "of" (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) "," (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_yoneda_1 :::"<|"::: ) (Set (Var "f")) ($#k3_yoneda_1 :::",?>"::: ) )) "iff" (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k4_nattra_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) "," (Set (Var "o")) ")"  ")" ) "," (Set  "("  ($#k2_cat_1 :::"Hom"::: )   "(" (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) "," (Set (Var "o")) ")"  ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set  "("  ($#k21_ens_1 :::"hom"::: )   "(" (Set (Var "f")) "," (Set  "("  ($#k4_cat_1 :::"id"::: )  (Set (Var "o")) ")" ) ")"  ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )))); 
 
theorem :: YONEDA_1:3 (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "A"))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) "," (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k3_yoneda_1 :::"<|"::: ) (Set (Var "f")) ($#k3_yoneda_1 :::",?>"::: ) ) ($#k4_tarski :::"]"::: ) ) "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set  "("  ($#k11_nattra_1 :::"Functors"::: )   "(" (Set (Var "A")) "," (Set  "("  ($#k1_yoneda_1 :::"EnsHom"::: )  (Set (Var "A")) ")" ) ")"  ")" ))))) ; 
 definitionlet "A" be   ($#l1_cat_1 :::"Category":::); func  :::"Yoneda"::: "A" ->    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" "A" "," (Set   ($#k11_nattra_1 :::"Functors"::: )   "(" "A" "," (Set  "("  ($#k1_yoneda_1 :::"EnsHom"::: )  "A" ")" ) ")" ) means :: YONEDA_1:def 4 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" "A" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) "," (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k3_yoneda_1 :::"<|"::: ) (Set (Var "f")) ($#k3_yoneda_1 :::",?>"::: ) ) ($#k4_tarski :::"]"::: ) ))); end; 





:: deftheorem    defines :::"Yoneda"::: YONEDA_1:def 4 :  (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Var "A")) "," (Set   ($#k11_nattra_1 :::"Functors"::: )   "(" (Set (Var "A")) "," (Set  "("  ($#k1_yoneda_1 :::"EnsHom"::: )  (Set (Var "A")) ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_yoneda_1 :::"Yoneda"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "b2"))  ($#k3_funct_2 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  ($#k4_tarski :::"["::: ) (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k4_graph_1 :::"cod"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) "," (Set  ($#k2_yoneda_1 :::"<|"::: ) (Set  "("  ($#k3_graph_1 :::"dom"::: )  (Set (Var "f")) ")" ) ($#k2_yoneda_1 :::",?>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k3_yoneda_1 :::"<|"::: ) (Set (Var "f")) ($#k3_yoneda_1 :::",?>"::: ) ) ($#k4_tarski :::"]"::: ) )))  ")" ))); 
 definitionlet "A", "B" be   ($#l1_cat_1 :::"Category":::); let "F" be    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Const "A")) "," (Set (Const "B")); let "c" be   ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")); func "F" :::"."::: "c" ->   ($#m1_subset_1 :::"Object":::) "of" "B" equals :: YONEDA_1:def 5 (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  "F" ")" )  ($#k3_funct_2 :::"."::: )  "c"); end; 








:: deftheorem    defines :::"."::: YONEDA_1:def 5 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "c")) "being"   ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds"  (Bool (Set (Set (Var "F"))  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_cat_1 :::"Obj"::: )  (Set (Var "F")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "c"))))))); 
 
theorem :: YONEDA_1:4 (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m2_cat_1 :::"Functor"::: )   "of" (Set (Var "A")) "," (Set   ($#k11_nattra_1 :::"Functors"::: )   "(" (Set (Var "A")) "," (Set  "("  ($#k1_yoneda_1 :::"EnsHom"::: )  (Set (Var "A")) ")" ) ")" )  "st" (Bool (Bool (Set   ($#k7_cat_1 :::"Obj"::: )  (Set (Var "F"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v14_cat_1 :::"faithful"::: )  )) "holds"  (Bool (Set (Var "F")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))) ; 
 definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); let "T" be    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "D")); attr "T" is  :::"faithful":::  means :: YONEDA_1:def 6 (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 :::"faithful"::: YONEDA_1:def 6 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "T")) "being"    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v1_yoneda_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 :: YONEDA_1:5 (Bool  "for" (Set (Var "A")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "F")) "being"    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Var "A")) "," (Set   ($#k11_nattra_1 :::"Functors"::: )   "(" (Set (Var "A")) "," (Set  "("  ($#k1_yoneda_1 :::"EnsHom"::: )  (Set (Var "A")) ")" ) ")" )  "st" (Bool (Bool (Set   ($#k7_cat_1 :::"Obj"::: )  (Set (Var "F"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "F")) "is"   ($#v1_yoneda_1 :::"faithful"::: )  )) "holds"  (Bool (Set (Var "F")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ))) ; 
 registrationlet "A" be   ($#l1_cat_1 :::"Category":::); 
cluster (Set   ($#k4_yoneda_1 :::"Yoneda"::: )  "A") ->   ($#v1_yoneda_1 :::"faithful"::: )   ; 
end; registrationlet "A" be   ($#l1_cat_1 :::"Category":::); 
cluster (Set   ($#k4_yoneda_1 :::"Yoneda"::: )  "A") ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; definitionlet "C", "D" be   ($#l1_cat_1 :::"Category":::); let "T" be    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Const "C")) "," (Set (Const "D")); attr "T" is  :::"full":::  means :: YONEDA_1:def 7 (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"  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c9")) ")" ) "," (Set  "(" "T"  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c")) ")" ) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "g")) "being"    ($#m1_cat_1 :::"Morphism"::: )   "of" (Set "T"  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c9"))) "," (Set "T"  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c"))) "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")))))  ")" ))); end; 






:: deftheorem    defines :::"full"::: YONEDA_1:def 7 :  (Bool  "for" (Set (Var "C")) "," (Set (Var "D")) "being"   ($#l1_cat_1 :::"Category":::)  (Bool  "for" (Set (Var "T")) "being"    ($#m1_oppcat_1 :::"Contravariant_Functor"::: )   "of" (Set (Var "C")) "," (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v2_yoneda_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"))  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c9")) ")" ) "," (Set  "(" (Set (Var "T"))  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c")) ")" ) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "for" (Set (Var "g")) "being"    ($#m1_cat_1 :::"Morphism"::: )   "of" (Set (Set (Var "T"))  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c9"))) "," (Set (Set (Var "T"))  ($#k5_yoneda_1 :::"."::: )  (Set (Var "c"))) "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")))))  ")" )))  ")" ))); 
 registrationlet "A" be   ($#l1_cat_1 :::"Category":::); 
cluster (Set   ($#k4_yoneda_1 :::"Yoneda"::: )  "A") ->   ($#v2_yoneda_1 :::"full"::: )   ; 
end;