:: NATTRA_1 semantic presentation begin definitionlet "A1" be ($#m1_hidden :::"set"::: ) ; let "B1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A1")) "," (Set (Const "B1")); let "Y1" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A1")); :: original: :::"|"::: redefine func "f" :::"|"::: "Y1" -> ($#m1_subset_1 :::"Function":::) "of" "Y1" "," "B1"; end; theorem :: NATTRA_1:1 (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "," (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B2")) (Bool "for" (Set (Var "Y1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "Y2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A2")) "holds" (Bool (Set (Set ($#k6_cat_2 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k6_cat_2 :::":]"::: ) ) ($#k1_nattra_1 :::"|"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k8_mcart_1 :::":]"::: ) )) ($#r8_binop_1 :::"="::: ) (Set ($#k6_cat_2 :::"[:"::: ) (Set "(" (Set (Var "f")) ($#k1_nattra_1 :::"|"::: ) (Set (Var "Y1")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_nattra_1 :::"|"::: ) (Set (Var "Y2")) ")" ) ($#k6_cat_2 :::":]"::: ) ))))))) ; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "A")); let "B1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "B")); let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Const "A1")) "," (Set (Const "A1")) ($#k8_mcart_1 :::":]"::: ) ) "," (Set (Const "A1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Const "B1")) "," (Set (Const "B1")) ($#k8_mcart_1 :::":]"::: ) ) "," (Set (Const "B1")); :: original: :::"|:"::: redefine func :::"|:":::"f" "," "g":::":|"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) "A1" "," "B1" ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_mcart_1 :::"[:"::: ) "A1" "," "B1" ($#k8_mcart_1 :::":]"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_mcart_1 :::"[:"::: ) "A1" "," "B1" ($#k8_mcart_1 :::":]"::: ) ); end; theorem :: NATTRA_1:2 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A1")) (Bool "for" (Set (Var "Y2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A2")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A1")) "," (Set (Var "A1")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "A1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A2")) "," (Set (Var "A2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "A2")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y1")) ($#k8_mcart_1 :::":]"::: ) ) "," (Set (Var "Y1")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_realset1 :::"||"::: ) (Set (Var "Y1"))))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "Y2")) "," (Set (Var "Y2")) ($#k8_mcart_1 :::":]"::: ) ) "," (Set (Var "Y2")) "st" (Bool (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_realset1 :::"||"::: ) (Set (Var "Y2"))))) "holds" (Bool (Set ($#k2_nattra_1 :::"|:"::: ) (Set (Var "F")) "," (Set (Var "G")) ($#k2_nattra_1 :::":|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_cat_2 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k7_cat_2 :::":|"::: ) ) ($#k1_realset1 :::"||"::: ) (Set ($#k8_mcart_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k8_mcart_1 :::":]"::: ) )))))))))) ; theorem :: NATTRA_1:3 canceled; theorem :: NATTRA_1:4 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: NATTRA_1:5 (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 ($#k10_cat_2 :::"["::: ) (Set ($#k10_cat_2 :::"["::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k10_cat_2 :::"]"::: ) ) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k10_cat_2 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "A")))))) ; theorem :: NATTRA_1:6 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "m")) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: NATTRA_1:7 (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 ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ")" ) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "A"))))) ; theorem :: NATTRA_1:8 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "C")) "being" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "A"))) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) & (Bool (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "A"))) ($#k5_relat_1 :::"|"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) & (Bool (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "A"))) ($#k1_realset1 :::"||"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) ")" ))) ; theorem :: NATTRA_1:9 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "O")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "M")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "A"))) "st" (Bool (Bool "(" "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "o")) ($#r2_hidden :::"in"::: ) (Set (Var "O")))) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "o"))) ($#r2_hidden :::"in"::: ) (Set (Var "M"))) ")" )) "holds" (Bool "for" (Set (Var "DOM")) "," (Set (Var "COD")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "M")) "," (Set (Var "O")) "st" (Bool (Bool (Set (Var "DOM")) ($#r1_funct_2 :::"="::: ) (Set (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "A"))) ($#k1_nattra_1 :::"|"::: ) (Set (Var "M")))) & (Bool (Set (Var "COD")) ($#r1_funct_2 :::"="::: ) (Set (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "A"))) ($#k1_nattra_1 :::"|"::: ) (Set (Var "M"))))) "holds" (Bool "for" (Set (Var "COMP")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "M")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "M")) "st" (Bool (Bool (Set (Var "COMP")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "A"))) ($#k1_realset1 :::"||"::: ) (Set (Var "M"))))) "holds" (Bool (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set (Var "O")) "," (Set (Var "M")) "," (Set (Var "DOM")) "," (Set (Var "COD")) "," (Set (Var "COMP")) "#)" ) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "A")))))))) ; theorem :: NATTRA_1:10 (Bool "for" (Set (Var "C")) "being" ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "A")) "being" ($#v1_cat_1 :::"strict"::: ) ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C"))))) ; begin definitioncanceled; end; :: deftheorem NATTRA_1:def 1 : canceled; theorem :: NATTRA_1:11 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k9_cat_3 :::"/."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k9_cat_3 :::"/."::: ) (Set "(" (Set (Var "F")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" )))))))) ; theorem :: NATTRA_1:12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set (Var "F1")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F2")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))))) ")" )) "holds" (Bool (Set (Var "F1")) ($#r2_funct_2 :::"="::: ) (Set (Var "F2"))))) ; theorem :: NATTRA_1:13 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (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 "c")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (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")) "holds" (Bool (Set (Set (Var "F")) ($#k9_cat_3 :::"/."::: ) (Set "(" (Set (Var "g")) ($#k5_cat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k9_cat_3 :::"/."::: ) (Set (Var "g")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" )))))))) ; theorem :: NATTRA_1:14 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k9_cat_3 :::"/."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: NATTRA_1:15 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "F")) ($#k9_cat_3 :::"/."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" )))))) ; theorem :: NATTRA_1:16 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "A")) ")" ) ($#k9_cat_3 :::"/."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: NATTRA_1:17 (Bool "for" (Set (Var "A")) "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 "A")) "st" (Bool (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ))) ; begin definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); pred "F1" :::"is_transformable_to"::: "F2" means :: NATTRA_1:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" "F1" ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" "F2" ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); reflexivity (Bool "for" (Set (Var "F1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "F1")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F1")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; end; :: deftheorem defines :::"is_transformable_to"::: NATTRA_1:def 2 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "F1")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F2")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))); theorem :: NATTRA_1:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "F")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2"))))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; mode :::"transformation"::: "of" "F1" "," "F2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "B") means :: NATTRA_1:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "F1" ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) "," (Set "F2" ($#k8_cat_1 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"transformation"::: NATTRA_1:def 3 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B"))) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) "is" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Set (Var "F1")) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "F2")) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))))) ")" )))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); func :::"id"::: "F" -> ($#m1_nattra_1 :::"transformation"::: ) "of" "F" "," "F" means :: NATTRA_1:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" "F" ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" )))); end; :: deftheorem defines :::"id"::: NATTRA_1:def 4 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "b4")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_nattra_1 :::"id"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" )))) ")" )))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; let "t" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); let "a" be ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")); func "t" :::"."::: "a" -> ($#m1_cat_1 :::"Morphism"::: ) "of" (Set "F1" ($#k8_cat_1 :::"."::: ) "a") "," (Set "F2" ($#k8_cat_1 :::"."::: ) "a") equals :: NATTRA_1:def 5 (Set "t" ($#k3_funct_2 :::"."::: ) "a"); end; :: deftheorem defines :::"."::: NATTRA_1:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")))))))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F", "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume that (Bool (Set (Const "F")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "F1"))) and (Bool (Set (Const "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; let "t1" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F")) "," (Set (Const "F1")); let "t2" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); func "t2" :::"`*`"::: "t1" -> ($#m1_nattra_1 :::"transformation"::: ) "of" "F" "," "F2" means :: NATTRA_1:def 6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Set it ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "t2" ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" "t1" ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))); end; :: deftheorem defines :::"`*`"::: NATTRA_1:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "b8")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k5_nattra_1 :::"`*`"::: ) (Set (Var "t1")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b8")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t2")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "t1")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))) ")" )))))); theorem :: NATTRA_1:19 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "t1")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "t1")) ($#r2_funct_2 :::"="::: ) (Set (Var "t2")))))) ; theorem :: NATTRA_1:20 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k3_nattra_1 :::"id"::: ) (Set (Var "F")) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" )))))) ; theorem :: NATTRA_1:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_nattra_1 :::"id"::: ) (Set (Var "F2")) ")" ) ($#k5_nattra_1 :::"`*`"::: ) (Set (Var "t"))) ($#r2_funct_2 :::"="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "t")) ($#k5_nattra_1 :::"`*`"::: ) (Set "(" ($#k3_nattra_1 :::"id"::: ) (Set (Var "F1")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "t"))) ")" )))) ; theorem :: NATTRA_1:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F3")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t3")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "holds" (Bool (Set (Set "(" (Set (Var "t3")) ($#k5_nattra_1 :::"`*`"::: ) (Set (Var "t2")) ")" ) ($#k5_nattra_1 :::"`*`"::: ) (Set (Var "t1"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "t3")) ($#k5_nattra_1 :::"`*`"::: ) (Set "(" (Set (Var "t2")) ($#k5_nattra_1 :::"`*`"::: ) (Set (Var "t1")) ")" )))))))) ; begin definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); pred "F1" :::"is_naturally_transformable_to"::: "F2" means :: NATTRA_1:def 7 (Bool "(" (Bool "F1" ($#r1_nattra_1 :::"is_transformable_to"::: ) "F2") & (Bool "ex" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" "F1" "," "F2" "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" "F1" ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "F2" ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))))) ")" ); reflexivity (Bool "for" (Set (Var "F1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F1")) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Const "A")) "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "F1")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))))) ")" )) ; end; :: deftheorem defines :::"is_naturally_transformable_to"::: NATTRA_1:def 7 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) "iff" (Bool "(" (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "F1")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F2")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))))) ")" ) ")" ))); theorem :: NATTRA_1:23 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "F")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "F2"))) ; mode :::"natural_transformation"::: "of" "F1" "," "F2" -> ($#m1_nattra_1 :::"transformation"::: ) "of" "F1" "," "F2" means :: NATTRA_1:def 8 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" it ($#k4_nattra_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" "F1" ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "F2" ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" it ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ))))); end; :: deftheorem defines :::"natural_transformation"::: NATTRA_1:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "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 "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "b5")) ($#k4_nattra_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "F1")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F2")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "b5")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ))))) ")" )))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"id"::: redefine func :::"id"::: "F" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" "F" "," "F"; end; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F", "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume that (Bool (Set (Const "F")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "F1"))) and (Bool (Set (Const "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "F2"))) ; let "t1" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F")) "," (Set (Const "F1")); let "t2" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); func "t2" :::"`*`"::: "t1" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" "F" "," "F2" equals :: NATTRA_1:def 9 (Set "t2" ($#k5_nattra_1 :::"`*`"::: ) "t1"); end; :: deftheorem defines :::"`*`"::: NATTRA_1:def 9 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool (Set (Set (Var "t2")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k5_nattra_1 :::"`*`"::: ) (Set (Var "t1")))))))); theorem :: NATTRA_1:24 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "F2")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t"))) ($#r2_funct_2 :::"="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "t")) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "F1")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "t"))) ")" )))) ; theorem :: NATTRA_1:25 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "t2")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t1")) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t2")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k5_cat_1 :::"*"::: ) (Set "(" (Set (Var "t1")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))))))) ; theorem :: NATTRA_1:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F3")))) "holds" (Bool "for" (Set (Var "t3")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "holds" (Bool (Set (Set "(" (Set (Var "t3")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t1")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "t3")) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" (Set (Var "t1")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t")) ")" )))))))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "IT" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); attr "IT" is :::"invertible"::: means :: NATTRA_1:def 10 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Set "IT" ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) "is" ($#v9_cat_1 :::"invertible"::: ) )); end; :: deftheorem defines :::"invertible"::: NATTRA_1:def 10 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "IT")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_nattra_1 :::"invertible"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "IT")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) "is" ($#v9_cat_1 :::"invertible"::: ) )) ")" )))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); pred "F1" "," "F2" :::"are_naturally_equivalent"::: means :: NATTRA_1:def 11 (Bool "(" (Bool "F1" ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) "F2") & (Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" "F1" "," "F2" "st" (Bool (Set (Var "t")) "is" ($#v1_nattra_1 :::"invertible"::: ) )) ")" ); reflexivity (Bool "for" (Set (Var "F1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F1")) "st" (Bool (Set (Var "t")) "is" ($#v1_nattra_1 :::"invertible"::: ) )) ")" )) ; end; :: deftheorem defines :::"are_naturally_equivalent"::: NATTRA_1:def 11 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r3_nattra_1 :::"are_naturally_equivalent"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Set (Var "t")) "is" ($#v1_nattra_1 :::"invertible"::: ) )) ")" ) ")" ))); notationlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); synonym "F1" :::"~="::: "F2" for "F1" "," "F2" :::"are_naturally_equivalent"::: ; end; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; let "t1" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); assume (Bool (Set (Const "t1")) "is" ($#v1_nattra_1 :::"invertible"::: ) ) ; func "t1" :::"""::: -> ($#m1_nattra_1 :::"transformation"::: ) "of" "F2" "," "F1" means :: NATTRA_1:def 12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "A" "holds" (Bool (Set it ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "t1" ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_cat_1 :::"""::: ) ))); end; :: deftheorem defines :::"""::: NATTRA_1:def 12 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "t1")) "is" ($#v1_nattra_1 :::"invertible"::: ) )) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F1")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t1")) ($#k8_nattra_1 :::"""::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b6")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t1")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_cat_1 :::"""::: ) ))) ")" ))))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "t1" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); assume that (Bool (Set (Const "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "F2"))) and (Bool (Set (Const "t1")) "is" ($#v1_nattra_1 :::"invertible"::: ) ) ; func "t1" :::"""::: -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" "F2" "," "F1" equals :: NATTRA_1:def 13 (Set "t1" ($#k8_nattra_1 :::"""::: ) ); end; :: deftheorem defines :::"""::: NATTRA_1:def 13 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "t1")) "is" ($#v1_nattra_1 :::"invertible"::: ) )) "holds" (Bool (Set (Set (Var "t1")) ($#k9_nattra_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "t1")) ($#k8_nattra_1 :::"""::: ) ))))); theorem :: NATTRA_1:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "t1")) "is" ($#v1_nattra_1 :::"invertible"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "t1")) ($#k9_nattra_1 :::"""::: ) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t1")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k6_cat_1 :::"""::: ) )))))) ; theorem :: NATTRA_1:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "F2")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F1"))))) ; theorem :: NATTRA_1:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F3")))) "holds" (Bool (Set (Var "F1")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F3"))))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) "," (Set (Const "F2")) ($#r3_nattra_1 :::"are_naturally_equivalent"::: ) ) ; mode :::"natural_equivalence"::: "of" "F1" "," "F2" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" "F1" "," "F2" means :: NATTRA_1:def 14 (Bool it "is" ($#v1_nattra_1 :::"invertible"::: ) ); end; :: deftheorem defines :::"natural_equivalence"::: NATTRA_1:def 14 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r3_nattra_1 :::"are_naturally_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m3_nattra_1 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2"))) "iff" (Bool (Set (Var "b5")) "is" ($#v1_nattra_1 :::"invertible"::: ) ) ")" )))); theorem :: NATTRA_1:30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set ($#k6_nattra_1 :::"id"::: ) (Set (Var "F"))) "is" ($#m3_nattra_1 :::"natural_equivalence"::: ) "of" (Set (Var "F")) "," (Set (Var "F"))))) ; theorem :: NATTRA_1:31 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F3")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m3_nattra_1 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t9")) "being" ($#m3_nattra_1 :::"natural_equivalence"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "holds" (Bool (Set (Set (Var "t9")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t"))) "is" ($#m3_nattra_1 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F3"))))))) ; begin definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); mode :::"NatTrans-DOMAIN"::: "of" "A" "," "B" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: NATTRA_1:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool "ex" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B"(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) ")" )))); end; :: deftheorem defines :::"NatTrans-DOMAIN"::: NATTRA_1:def 15 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m4_nattra_1 :::"NatTrans-DOMAIN"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3")))) "holds" (Bool "ex" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) ")" )))) ")" ))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); func :::"NatTrans"::: "(" "A" "," "B" ")" -> ($#m4_nattra_1 :::"NatTrans-DOMAIN"::: ) "of" "A" "," "B" means :: NATTRA_1:def 16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B"(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) ")" ))) ")" )); end; :: deftheorem defines :::"NatTrans"::: NATTRA_1:def 16 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b3")) "being" ($#m4_nattra_1 :::"NatTrans-DOMAIN"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_nattra_1 :::"NatTrans"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) ")" ))) ")" )) ")" ))); theorem :: NATTRA_1:32 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t1")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_nattra_1 :::"NatTrans"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) ")" )))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); func :::"Functors"::: "(" "A" "," "B" ")" -> ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"Category":::) means :: NATTRA_1:def 17 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_2 :::"Funct"::: ) "(" "A" "," "B" ")" )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k10_nattra_1 :::"NatTrans"::: ) "(" "A" "," "B" ")" )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" it "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" it "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k10_cat_2 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" it))) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" it "st" (Bool (Bool (Set ($#k10_cat_2 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" it)))) "holds" (Bool "ex" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B"(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1"))(Bool "ex" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F1")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" it) ($#k1_funct_1 :::"."::: ) (Set ($#k10_cat_2 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "t1")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" it (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B" "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "F")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ); end; :: deftheorem defines :::"Functors"::: NATTRA_1:def 17 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b3")) "being" ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_2 :::"Funct"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k10_nattra_1 :::"NatTrans"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3")) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) )) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_xtuple_0 :::"`2"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k10_cat_2 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "b3"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b3")) "st" (Bool (Bool (Set ($#k10_cat_2 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "b3")))))) "holds" (Bool "ex" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1"))(Bool "ex" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F1")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t1")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set (Var "b3"))) ($#k1_funct_1 :::"."::: ) (Set ($#k10_cat_2 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "t1")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) )) ")" )))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "b3")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Var "a")))) "holds" (Bool (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "F")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" ) ")" ) ")" ))); theorem :: NATTRA_1:33 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F1")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) ")" ))))) ; theorem :: NATTRA_1:34 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) (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 "ex" (Set (Var "F")) "," (Set (Var "F1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))(Bool "ex" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) "st" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "F"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "F1"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F1")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) ")" )))))) ; theorem :: NATTRA_1:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F2")) "," (Set (Var "F3")) "," (Set (Var "F")) "," (Set (Var "F1")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t9")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F1")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F2")) "," (Set (Var "F3")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t9")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k10_cat_2 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k10_cat_2 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" )))) "iff" (Bool (Set (Var "F1")) ($#r2_funct_2 :::"="::: ) (Set (Var "F2"))) ")" )))))) ; theorem :: NATTRA_1:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t1")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F1")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F1")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set (Var "t1")) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "F")) "," (Set (Var "F2")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set (Var "t1")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t")) ")" ) ($#k4_tarski :::"]"::: ) ))))))) ; begin definitionlet "C" be ($#l1_cat_1 :::"Category":::); attr "C" is :::"discrete"::: means :: NATTRA_1:def 18 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "st" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))))); end; :: deftheorem defines :::"discrete"::: NATTRA_1:def 18 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "C")) "is" ($#v2_nattra_1 :::"discrete"::: ) ) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "a")))))) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) bbbadV14_STRUCT_0() ($#v2_cat_1 :::"Category-like"::: ) ($#v3_cat_1 :::"transitive"::: ) ($#v4_cat_1 :::"associative"::: ) ($#v5_cat_1 :::"reflexive"::: ) ($#v6_cat_1 :::"with_identities"::: ) ($#v2_nattra_1 :::"discrete"::: ) for ($#l1_cat_1 :::"CatStr"::: ) ; end; theorem :: NATTRA_1:37 (Bool "for" (Set (Var "A")) "being" ($#v2_nattra_1 :::"discrete"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: NATTRA_1:38 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "A")) "is" ($#v2_nattra_1 :::"discrete"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "ex" (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" )) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" )) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ) ")" )) ; theorem :: NATTRA_1:39 (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")) ")" ) "is" ($#v2_nattra_1 :::"discrete"::: ) )) ; theorem :: NATTRA_1:40 (Bool "for" (Set (Var "A")) "being" ($#v2_nattra_1 :::"discrete"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "C")) "being" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Var "C")) "is" ($#v2_nattra_1 :::"discrete"::: ) ))) ; theorem :: NATTRA_1:41 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_nattra_1 :::"discrete"::: ) ) & (Bool (Set (Var "B")) "is" ($#v2_nattra_1 :::"discrete"::: ) )) "holds" (Bool (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "is" ($#v2_nattra_1 :::"discrete"::: ) )) ; theorem :: NATTRA_1:42 (Bool "for" (Set (Var "A")) "being" ($#v2_nattra_1 :::"discrete"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "F1")) ($#r2_funct_2 :::"="::: ) (Set (Var "F2")))))) ; theorem :: NATTRA_1:43 (Bool "for" (Set (Var "A")) "being" ($#v2_nattra_1 :::"discrete"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F")) "holds" (Bool (Set (Var "t")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_nattra_1 :::"id"::: ) (Set (Var "F")))))))) ; theorem :: NATTRA_1:44 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) "is" ($#v2_nattra_1 :::"discrete"::: ) )) "holds" (Bool (Set ($#k11_nattra_1 :::"Functors"::: ) "(" (Set (Var "B")) "," (Set (Var "A")) ")" ) "is" ($#v2_nattra_1 :::"discrete"::: ) )) ; registrationlet "C" be ($#l1_cat_1 :::"Category":::); 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"::: ) ($#v2_nattra_1 :::"discrete"::: ) for ($#m3_cat_2 :::"Subcategory"::: ) "of" "C"; end; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"IdCat"::: "C" -> ($#v1_cat_1 :::"strict"::: ) ($#v2_nattra_1 :::"discrete"::: ) ($#m3_cat_2 :::"Subcategory"::: ) "of" "C" means :: NATTRA_1:def 19 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C")) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Object":::) "of" "C" : (Bool verum) "}" ) ")" ); end; :: deftheorem defines :::"IdCat"::: NATTRA_1:def 19 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_cat_1 :::"strict"::: ) ($#v2_nattra_1 :::"discrete"::: ) ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_nattra_1 :::"IdCat"::: ) (Set (Var "C")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C")))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" ) where a "is" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) : (Bool verum) "}" ) ")" ) ")" ))); theorem :: NATTRA_1:45 (Bool "for" (Set (Var "C")) "being" ($#v1_cat_1 :::"strict"::: ) ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "C")) "is" ($#v2_nattra_1 :::"discrete"::: ) )) "holds" (Bool (Set ($#k12_nattra_1 :::"IdCat"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "C")))) ; theorem :: NATTRA_1:46 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k12_nattra_1 :::"IdCat"::: ) (Set "(" ($#k12_nattra_1 :::"IdCat"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_nattra_1 :::"IdCat"::: ) (Set (Var "C"))))) ; theorem :: NATTRA_1:47 (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_nattra_1 :::"IdCat"::: ) (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ))) ; theorem :: NATTRA_1:48 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k12_nattra_1 :::"IdCat"::: ) (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_cat_2 :::"[:"::: ) (Set "(" ($#k12_nattra_1 :::"IdCat"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k12_nattra_1 :::"IdCat"::: ) (Set (Var "B")) ")" ) ($#k8_cat_2 :::":]"::: ) ))) ;