:: INDEX_1 semantic presentation begin registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) bbbadV3_RELAT_1() "A" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "C" be ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::); let "f" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); :: original: :::"`2"::: redefine func "f" :::"`2"::: -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set "f" ($#k5_cat_5 :::"`11"::: ) ) "," (Set "f" ($#k6_cat_5 :::"`12"::: ) ); end; theorem :: INDEX_1:1 (Bool "for" (Set (Var "C")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k9_cat_2 :::"["::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "g")) ")" ) ($#k9_cat_2 :::"]"::: ) ) "," (Set "(" (Set "(" (Set (Var "g")) ($#k1_index_1 :::"`2"::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k1_index_1 :::"`2"::: ) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))) ; theorem :: INDEX_1:2 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_2 :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F"))) ($#r1_funct_2 :::"="::: ) (Set ($#k7_cat_1 :::"Obj"::: ) (Set (Var "G")))))))) ; definitionlet "IT" be ($#m1_hidden :::"Function":::); attr "IT" is :::"Category-yielding"::: means :: INDEX_1:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l1_cat_1 :::"Category":::))); end; :: deftheorem defines :::"Category-yielding"::: INDEX_1:def 1 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_index_1 :::"Category-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#l1_cat_1 :::"Category":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_index_1 :::"Category-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_index_1 :::"Category-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; mode ManySortedCategory of "A" is ($#v1_index_1 :::"Category-yielding"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "A"; end; definitionlet "C" be ($#l1_cat_1 :::"Category":::); mode ManySortedCategory of "C" is ($#m1_hidden :::"ManySortedCategory":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C"); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "x" be ($#l1_cat_1 :::"Category":::); cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "x") -> ($#v1_index_1 :::"Category-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v1_index_1 :::"Category-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) "f") -> ($#v2_cat_5 :::"categorial"::: ) ; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedCategory":::) "of" (Set (Const "X")); let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#l1_cat_1 :::"Category":::); end; registrationlet "f" be ($#m1_hidden :::"Function":::); let "g" be ($#v1_index_1 :::"Category-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v1_index_1 :::"Category-yielding"::: ) ; end; definitionlet "F" be ($#v1_index_1 :::"Category-yielding"::: ) ($#m1_hidden :::"Function":::); func :::"Objs"::: "F" -> ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::) means :: INDEX_1:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))))) ")" ) ")" ); func :::"Mphs"::: "F" -> ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::) means :: INDEX_1:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F"))) "holds" (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) ")" ) ")" ); end; :: deftheorem defines :::"Objs"::: INDEX_1:def 2 : (Bool "for" (Set (Var "F")) "being" ($#v1_index_1 :::"Category-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_index_1 :::"Objs"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"Mphs"::: INDEX_1:def 3 : (Bool "for" (Set (Var "F")) "being" ($#v1_index_1 :::"Category-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_index_1 :::"Mphs"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) ")" ) ")" ) ")" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"ManySortedCategory":::) "of" (Set (Const "A")); cluster (Set ($#k3_index_1 :::"Objs"::: ) "F") -> ($#v2_relat_1 :::"non-empty"::: ) "A" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set ($#k4_index_1 :::"Mphs"::: ) "F") -> ($#v2_relat_1 :::"non-empty"::: ) "A" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_hidden :::"ManySortedCategory":::) "of" (Set (Const "A")); cluster (Set ($#k3_index_1 :::"Objs"::: ) "F") -> ($#v2_relat_1 :::"non-empty"::: ) ($#v1_partfun1 :::"total"::: ) ; cluster (Set ($#k4_index_1 :::"Mphs"::: ) "F") -> ($#v2_relat_1 :::"non-empty"::: ) ($#v1_partfun1 :::"total"::: ) ; end; theorem :: INDEX_1:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set ($#k3_index_1 :::"Objs"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))))) & (Bool (Set ($#k4_index_1 :::"Mphs"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "C")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))))) ")" ))) ; begin definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; mode :::"ManySortedSet"::: "of" "A" "," "B" -> ($#m1_hidden :::"set"::: ) means :: INDEX_1:def 4 (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "A"(Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" "B" "st" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) )))); end; :: deftheorem defines :::"ManySortedSet"::: INDEX_1:def 4 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "A"))(Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "B")) "st" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) )))) ")" ))); definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "A")); let "g" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "B")); :: original: :::"["::: redefine func :::"[":::"f" "," "g":::"]"::: -> ($#m1_index_1 :::"ManySortedSet"::: ) "of" "A" "," "B"; end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); cluster (Set "X" ($#k1_xtuple_0 :::"`1"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; cluster (Set "X" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); cluster (Set "X" ($#k1_xtuple_0 :::"`1"::: ) ) -> "A" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set "X" ($#k2_xtuple_0 :::"`2"::: ) ) -> "B" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); cluster (Set "X" ($#k1_xtuple_0 :::"`1"::: ) ) -> "A" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"A" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster (Set "X" ($#k2_xtuple_0 :::"`2"::: ) ) -> "B" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"B" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "IT" be ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); attr "IT" is :::"Category-yielding_on_first"::: means :: INDEX_1:def 5 (Bool (Set "IT" ($#k1_xtuple_0 :::"`1"::: ) ) "is" ($#v1_index_1 :::"Category-yielding"::: ) ); attr "IT" is :::"Function-yielding_on_second"::: means :: INDEX_1:def 6 (Bool (Set "IT" ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ); end; :: deftheorem defines :::"Category-yielding_on_first"::: INDEX_1:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_index_1 :::"Category-yielding_on_first"::: ) ) "iff" (Bool (Set (Set (Var "IT")) ($#k1_xtuple_0 :::"`1"::: ) ) "is" ($#v1_index_1 :::"Category-yielding"::: ) ) ")" ))); :: deftheorem defines :::"Function-yielding_on_second"::: INDEX_1:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "IT")) "being" ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_index_1 :::"Function-yielding_on_second"::: ) ) "iff" (Bool (Set (Set (Var "IT")) ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#v1_funcop_1 :::"Function-yielding"::: ) ) ")" ))); registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster ($#v2_index_1 :::"Category-yielding_on_first"::: ) ($#v3_index_1 :::"Function-yielding_on_second"::: ) for ($#m1_index_1 :::"ManySortedSet"::: ) "of" "A" "," "B"; end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#v2_index_1 :::"Category-yielding_on_first"::: ) ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); cluster (Set "X" ($#k1_xtuple_0 :::"`1"::: ) ) -> ($#v1_index_1 :::"Category-yielding"::: ) ; end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "X" be ($#v3_index_1 :::"Function-yielding_on_second"::: ) ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); cluster (Set "X" ($#k2_xtuple_0 :::"`2"::: ) ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "f" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k10_xtuple_0 :::"proj2"::: ) "f") -> ($#v4_funct_1 :::"functional"::: ) ; end; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedCategory":::) "of" (Set (Const "A")); let "g" be ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Const "B")); :: original: :::"["::: redefine func :::"[":::"f" "," "g":::"]"::: -> ($#v2_index_1 :::"Category-yielding_on_first"::: ) ($#v3_index_1 :::"Function-yielding_on_second"::: ) ($#m1_index_1 :::"ManySortedSet"::: ) "of" "A" "," "B"; end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_hidden :::"ManySortedCategory":::) "of" (Set (Const "A")); mode :::"ManySortedFunctor"::: "of" "F" "," "G" -> ($#m1_hidden :::"ManySortedFunction":::) "of" "A" means :: INDEX_1:def 7 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set "F" ($#k2_index_1 :::"."::: ) (Set (Var "a"))) "," (Set "G" ($#k2_index_1 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"ManySortedFunctor"::: INDEX_1:def 7 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"ManySortedCategory":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m2_index_1 :::"ManySortedFunctor"::: ) "of" (Set (Var "F")) "," (Set (Var "G"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set (Var "F")) ($#k2_index_1 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "G")) ($#k2_index_1 :::"."::: ) (Set (Var "a"))))) ")" )))); scheme :: INDEX_1:sch 1 LambdaMSFr{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"ManySortedCategory":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"ManySortedCategory":::) "of" (Set F1 "(" ")" ), F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "F")) "being" ($#m2_index_1 :::"ManySortedFunctor"::: ) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "a")) ")" )))) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F4 "(" (Set (Var "a")) ")" ) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set F2 "(" ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a"))) "," (Set (Set F3 "(" ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a"))))) proof end; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_hidden :::"ManySortedCategory":::) "of" (Set (Const "A")); let "f" be ($#m2_index_1 :::"ManySortedFunctor"::: ) "of" (Set (Const "F")) "," (Set (Const "G")); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"."::: redefine func "f" :::"."::: "a" -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set "F" ($#k2_index_1 :::"."::: ) "a") "," (Set "G" ($#k2_index_1 :::"."::: ) "a"); end; begin definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set (Const "A")); mode :::"Indexing"::: "of" "F" "," "G" -> ($#v2_index_1 :::"Category-yielding_on_first"::: ) ($#m1_index_1 :::"ManySortedSet"::: ) "of" "A" "," "B" means :: INDEX_1:def 8 (Bool (Set it ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#m2_index_1 :::"ManySortedFunctor"::: ) "of" (Set (Set "(" it ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) "F") "," (Set (Set "(" it ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) "G")); end; :: deftheorem defines :::"Indexing"::: INDEX_1:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) (Bool "for" (Set (Var "b5")) "being" ($#v2_index_1 :::"Category-yielding_on_first"::: ) ($#m1_index_1 :::"ManySortedSet"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m3_index_1 :::"Indexing"::: ) "of" (Set (Var "F")) "," (Set (Var "G"))) "iff" (Bool (Set (Set (Var "b5")) ($#k2_xtuple_0 :::"`2"::: ) ) "is" ($#m2_index_1 :::"ManySortedFunctor"::: ) "of" (Set (Set "(" (Set (Var "b5")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "F"))) "," (Set (Set "(" (Set (Var "b5")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "G")))) ")" )))); theorem :: INDEX_1:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) (Bool "for" (Set (Var "I")) "being" ($#m3_index_1 :::"Indexing"::: ) "of" (Set (Var "F")) "," (Set (Var "G")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")) ")" )) "," (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "m")) ")" ))))))) ; theorem :: INDEX_1:5 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m3_index_1 :::"Indexing"::: ) "of" (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k2_xtuple_0 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "m")) ")" )) "," (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "m")) ")" )))))) ; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set (Const "A")); let "I" be ($#m3_index_1 :::"Indexing"::: ) "of" (Set (Const "F")) "," (Set (Const "G")); :: original: :::"`2"::: redefine func "I" :::"`2"::: -> ($#m2_index_1 :::"ManySortedFunctor"::: ) "of" (Set (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) "F") "," (Set (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) "G"); end; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set (Const "A")); let "I" be ($#m3_index_1 :::"Indexing"::: ) "of" (Set (Const "F")) "," (Set (Const "G")); mode :::"TargetCat"::: "of" "I" -> ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) means :: INDEX_1:def 9 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"Object":::) "of" it) ")" ) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "B" "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" "F" ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ) "," (Set "(" (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" "G" ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" "I" ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k4_tarski :::"]"::: ) ) "is" ($#m1_subset_1 :::"Morphism":::) "of" it) ")" ) ")" ); end; :: deftheorem defines :::"TargetCat"::: INDEX_1:def 9 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) (Bool "for" (Set (Var "I")) "being" ($#m3_index_1 :::"Indexing"::: ) "of" (Set (Var "F")) "," (Set (Var "G")) (Bool "for" (Set (Var "b6")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "b6"))) ")" ) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "b")) ")" ) ($#k4_tarski :::"]"::: ) ) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "b6"))) ")" ) ")" ) ")" ))))); registrationlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set (Const "A")); let "I" be ($#m3_index_1 :::"Indexing"::: ) "of" (Set (Const "F")) "," (Set (Const "G")); 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"::: ) bbbadV3_CAT_1() bbbadV4_CAT_1() bbbadV5_CAT_1() ($#v6_cat_1 :::"with_identities"::: ) ($#v1_cat_5 :::"with_triple-like_morphisms"::: ) ($#v3_cat_5 :::"Categorial"::: ) ($#v4_cat_5 :::"full"::: ) for ($#m4_index_1 :::"TargetCat"::: ) "of" "I"; end; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F", "G" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "B")) "," (Set (Const "A")); let "c" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "B")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "B")); let "i" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); given "C" being ($#l1_cat_1 :::"Category":::) such that (Bool (Set (Const "C")) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set (Const "A")) "," (Set (Const "B")) "," (Set (Const "F")) "," (Set (Const "G")) "," (Set (Const "c")) "#)" )) ; mode :::"Indexing"::: "of" "F" "," "G" "," "c" "," "i" -> ($#m3_index_1 :::"Indexing"::: ) "of" "F" "," "G" means :: INDEX_1:def 10 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set (Set "(" it ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set "(" "i" ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set "(" (Set "(" it ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "B" "st" (Bool (Bool (Set "F" ($#k3_funct_2 :::"."::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set "G" ($#k3_funct_2 :::"."::: ) (Set (Var "m1"))))) "holds" (Bool (Set (Set "(" it ($#k8_index_1 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" "c" ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k4_tarski :::"]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" it ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" it ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m1")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Indexing"::: INDEX_1:def 10 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B")) "," (Set (Var "A")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "B")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool "ex" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#g1_cat_1 :::"CatStr"::: ) "(#" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "c")) "#)" )))) "holds" (Bool "for" (Set (Var "b7")) "being" ($#m3_index_1 :::"Indexing"::: ) "of" (Set (Var "F")) "," (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b7")) "is" ($#m5_index_1 :::"Indexing"::: ) "of" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "c")) "," (Set (Var "i"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "b7")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set "(" (Set "(" (Set (Var "b7")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "st" (Bool (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "m1"))))) "holds" (Bool (Set (Set "(" (Set (Var "b7")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "c")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "m2")) "," (Set (Var "m1")) ($#k4_tarski :::"]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b7")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b7")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m1")) ")" ))) ")" ) ")" ) ")" )))))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); mode Indexing of "C" is ($#m5_index_1 :::"Indexing"::: ) "of" (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "C") "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "C") "," (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C") "," (Set ($#k7_isocat_1 :::"IdMap"::: ) "C"); mode coIndexing of "C" is ($#m5_index_1 :::"Indexing"::: ) "of" (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" "C") "," (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" "C") "," (Set ($#k1_oppcat_1 :::"~"::: ) (Set "the" ($#u1_cat_1 :::"Comp"::: ) "of" "C")) "," (Set ($#k7_isocat_1 :::"IdMap"::: ) "C"); end; theorem :: INDEX_1:6 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m3_index_1 :::"Indexing"::: ) "of" (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set "(" (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set "(" (Set (Var "m2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m2")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m1")) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: INDEX_1:7 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m3_index_1 :::"Indexing"::: ) "of" (Set "the" ($#u2_graph_1 :::"Target"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u1_graph_1 :::"Source"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "I")) "is" ($#m5_index_1 :::"coIndexing":::) "of" (Set (Var "C"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "a")) ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set "(" (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "a")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "m1")) "," (Set (Var "m2")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "m2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "m1"))))) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set "(" (Set (Var "m2")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "m1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m1")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m2")) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: INDEX_1:8 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m5_index_1 :::"coIndexing":::) "of" (Set (Var "C"))) "iff" (Bool (Set (Var "x")) "is" ($#m5_index_1 :::"Indexing":::) "of" (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )) ")" ))) ; theorem :: INDEX_1:9 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Bool "not" (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c1")) "," (Set (Var "c2")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "c1"))) "," (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "c2")))))))) ; theorem :: INDEX_1:10 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"coIndexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "st" (Bool (Bool (Bool "not" (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set (Var "c1")) "," (Set (Var "c2")) ")" ) "is" ($#v1_xboole_0 :::"empty"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "c1")) "," (Set (Var "c2")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m"))) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "c2"))) "," (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "c1")))))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m5_index_1 :::"Indexing":::) "of" (Set (Const "C")); let "T" be ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Const "I")); func "I" :::"-functor"::: "(" "C" "," "T" ")" -> ($#m2_cat_1 :::"Functor"::: ) "of" "C" "," "T" means :: INDEX_1:def 11 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" "I" ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "f")) ")" ) ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"-functor"::: INDEX_1:def 11 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "b4")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" )) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "f")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" ))))); theorem :: INDEX_1:11 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T1")) ")" ) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T2")) ")" )) & (Bool (Set ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T1")) ")" ")" )) ($#r1_funct_2 :::"="::: ) (Set ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T2")) ")" ")" ))) ")" )))) ; theorem :: INDEX_1:12 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool (Set ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ))))) ; theorem :: INDEX_1:13 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" ")" ) ($#k8_cat_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set (Var "x")))))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m5_index_1 :::"Indexing":::) "of" (Set (Const "C")); func :::"rng"::: "I" -> ($#v1_cat_1 :::"strict"::: ) ($#m4_index_1 :::"TargetCat"::: ) "of" "I" means :: INDEX_1:def 12 (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" "I" "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_cat_5 :::"Image"::: ) (Set "(" "I" ($#k9_index_1 :::"-functor"::: ) "(" "C" "," (Set (Var "T")) ")" ")" )))); end; :: deftheorem defines :::"rng"::: INDEX_1:def 12 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "b3")) "being" ($#v1_cat_1 :::"strict"::: ) ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_index_1 :::"rng"::: ) (Set (Var "I")))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_5 :::"Image"::: ) (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" ")" )))) ")" )))); theorem :: INDEX_1:14 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set ($#k10_index_1 :::"rng"::: ) (Set (Var "I"))) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "D"))) "iff" (Bool (Set (Var "D")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I"))) ")" )))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m5_index_1 :::"Indexing":::) "of" (Set (Const "C")); let "m" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); func "I" :::"."::: "m" -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) "m" ")" )) "," (Set (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) "m" ")" )) equals :: INDEX_1:def 13 (Set (Set "(" "I" ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) "m"); end; :: deftheorem defines :::"."::: INDEX_1:def 13 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "I")) ($#k11_index_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m"))))))); definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m5_index_1 :::"coIndexing":::) "of" (Set (Const "C")); let "m" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "C")); func "I" :::"."::: "m" -> ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) "m" ")" )) "," (Set (Set "(" "I" ($#k1_xtuple_0 :::"`1"::: ) ")" ) ($#k2_index_1 :::"."::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) "m" ")" )) equals :: INDEX_1:def 14 (Set (Set "(" "I" ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) "m"); end; :: deftheorem defines :::"."::: INDEX_1:def 14 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"coIndexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "I")) ($#k12_index_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ")" ) ($#k7_index_1 :::"."::: ) (Set (Var "m"))))))); theorem :: INDEX_1:15 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set ($#k6_index_1 :::"["::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ) ($#k6_index_1 :::"]"::: ) ) "is" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C"))) & (Bool (Set ($#k6_index_1 :::"["::: ) (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "D")) ")" ) "," (Set "(" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ) ($#k6_index_1 :::"]"::: ) ) "is" ($#m5_index_1 :::"coIndexing":::) "of" (Set (Var "C"))) ")" )) ; begin registrationlet "C" be ($#l1_cat_1 :::"Category":::); let "D" be ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k7_cat_1 :::"Obj"::: ) "F") -> ($#v1_index_1 :::"Category-yielding"::: ) ; end; theorem :: INDEX_1:16 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k12_mcart_1 :::"pr2"::: ) (Set (Var "F")) ")" ) ($#k4_tarski :::"]"::: ) ) "is" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "D" be ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); func "F" :::"-indexing_of"::: "C" -> ($#m5_index_1 :::"Indexing":::) "of" "C" equals :: INDEX_1:def 15 (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k7_cat_1 :::"Obj"::: ) "F" ")" ) "," (Set "(" ($#k12_mcart_1 :::"pr2"::: ) "F" ")" ) ($#k4_tarski :::"]"::: ) ); end; :: deftheorem defines :::"-indexing_of"::: INDEX_1:def 15 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ) "," (Set "(" ($#k12_mcart_1 :::"pr2"::: ) (Set (Var "F")) ")" ) ($#k4_tarski :::"]"::: ) ))))); theorem :: INDEX_1:17 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Var "D")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Set (Var "F")) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C"))))))) ; theorem :: INDEX_1:18 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Set (Var "F")) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C"))) "holds" (Bool (Set (Var "F")) ($#r1_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C")) ")" ) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" )))))) ; theorem :: INDEX_1:19 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_2 :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C")))))))) ; theorem :: INDEX_1:20 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool (Set ($#k12_mcart_1 :::"pr2"::: ) (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k8_index_1 :::"`2"::: ) ))))) ; theorem :: INDEX_1:21 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" ")" ) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "I")))))) ; begin definitionlet "C", "D", "E" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "C")) "," (Set (Const "D")); let "I" be ($#m5_index_1 :::"Indexing":::) "of" (Set (Const "E")); assume (Bool (Set ($#k4_cat_5 :::"Image"::: ) (Set (Const "F"))) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Const "E"))) ; func "I" :::"*"::: "F" -> ($#m5_index_1 :::"Indexing":::) "of" "C" means :: INDEX_1:def 16 (Bool "for" (Set (Var "F9")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "C" "," "E" "st" (Bool (Bool (Set (Var "F9")) ($#r1_funct_2 :::"="::: ) "F")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "I" ($#k9_index_1 :::"-functor"::: ) "(" "E" "," (Set "(" ($#k10_index_1 :::"rng"::: ) "I" ")" ) ")" ")" ) ($#k9_cat_1 :::"*"::: ) (Set (Var "F9")) ")" ) ($#k13_index_1 :::"-indexing_of"::: ) "C"))); end; :: deftheorem defines :::"*"::: INDEX_1:def 16 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "E")) "st" (Bool (Bool (Set ($#k4_cat_5 :::"Image"::: ) (Set (Var "F"))) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "E")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "F9")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "F9")) ($#r1_funct_2 :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "E")) "," (Set "(" ($#k10_index_1 :::"rng"::: ) (Set (Var "I")) ")" ) ")" ")" ) ($#k9_cat_1 :::"*"::: ) (Set (Var "F9")) ")" ) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C"))))) ")" ))))); theorem :: INDEX_1:22 (Bool "for" (Set (Var "C")) "," (Set (Var "D1")) "," (Set (Var "D2")) "," (Set (Var "E")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D1")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D2")) "st" (Bool (Bool (Set ($#k4_cat_5 :::"Image"::: ) (Set (Var "F"))) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "E"))) & (Bool (Set ($#k4_cat_5 :::"Image"::: ) (Set (Var "G"))) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "E"))) & (Bool (Set (Var "F")) ($#r1_funct_2 :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "G")))))))) ; theorem :: INDEX_1:23 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "D")) "," (Set (Var "T")) ")" ")" ) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C")))))))) ; theorem :: INDEX_1:24 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Var "T")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "F")))))))) ; theorem :: INDEX_1:25 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) "holds" (Bool (Set ($#k10_index_1 :::"rng"::: ) (Set "(" (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "F")) ")" )) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set (Var "T"))))))) ; theorem :: INDEX_1:26 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "G")) ")" ) ($#k14_index_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")) ")" ))))))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); let "I" be ($#m5_index_1 :::"Indexing":::) "of" (Set (Const "C")); let "D" be ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::); assume (Bool (Set (Const "D")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Const "I"))) ; let "E" be ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "D")) "," (Set (Const "E")); func "F" :::"*"::: "I" -> ($#m5_index_1 :::"Indexing":::) "of" "C" means :: INDEX_1:def 17 (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" "I" (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," "E" "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) "D") & (Bool (Set (Var "G")) ($#r1_funct_2 :::"="::: ) "F")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set "(" "I" ($#k9_index_1 :::"-functor"::: ) "(" "C" "," (Set (Var "T")) ")" ")" ) ")" ) ($#k13_index_1 :::"-indexing_of"::: ) "C")))); end; :: deftheorem defines :::"*"::: INDEX_1:def 17 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "D")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")))) "holds" (Bool "for" (Set (Var "E")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "b6")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "I")))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Var "G")) ($#r1_funct_2 :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" ")" ) ")" ) ($#k13_index_1 :::"-indexing_of"::: ) (Set (Var "C")))))) ")" ))))))); theorem :: INDEX_1:27 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "F")) ($#r1_funct_2 :::"="::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k15_index_1 :::"*"::: ) (Set (Var "I")))))))))) ; theorem :: INDEX_1:28 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "D")) "holds" (Bool (Set ($#k4_cat_5 :::"Image"::: ) (Set (Var "F"))) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "I"))))))))) ; theorem :: INDEX_1:29 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "D")) "holds" (Bool (Set (Var "D")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "I"))))))))) ; theorem :: INDEX_1:30 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "D")) "holds" (Bool (Set ($#k10_index_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "I")) ")" )) "is" ($#m3_cat_2 :::"Subcategory"::: ) "of" (Set ($#k4_cat_5 :::"Image"::: ) (Set (Var "F"))))))))) ; theorem :: INDEX_1:31 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "D")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "D")) "," (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k15_index_1 :::"*"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k15_index_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "I")) ")" ))))))))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); let "I1" be ($#m5_index_1 :::"Indexing":::) "of" (Set (Const "C")); let "I2" be ($#m5_index_1 :::"Indexing":::) "of" (Set (Const "D")); func "I2" :::"*"::: "I1" -> ($#m5_index_1 :::"Indexing":::) "of" "C" equals :: INDEX_1:def 18 (Set "I2" ($#k14_index_1 :::"*"::: ) (Set "(" "I1" ($#k9_index_1 :::"-functor"::: ) "(" "C" "," (Set "(" ($#k10_index_1 :::"rng"::: ) "I1" ")" ) ")" ")" )); end; :: deftheorem defines :::"*"::: INDEX_1:def 18 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I1")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "I2")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "I2")) ($#k16_index_1 :::"*"::: ) (Set (Var "I1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I2")) ($#k14_index_1 :::"*"::: ) (Set "(" (Set (Var "I1")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set "(" ($#k10_index_1 :::"rng"::: ) (Set (Var "I1")) ")" ) ")" ")" )))))); theorem :: INDEX_1:32 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I1")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "I2")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I1")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I1")))) "holds" (Bool (Set (Set (Var "I2")) ($#k16_index_1 :::"*"::: ) (Set (Var "I1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I2")) ($#k14_index_1 :::"*"::: ) (Set "(" (Set (Var "I1")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "C")) "," (Set (Var "T")) ")" ")" )))))))) ; theorem :: INDEX_1:33 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I1")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "I2")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I2")) "st" (Bool (Bool (Set (Var "D")) "is" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I1")))) "holds" (Bool (Set (Set (Var "I2")) ($#k16_index_1 :::"*"::: ) (Set (Var "I1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I2")) ($#k9_index_1 :::"-functor"::: ) "(" (Set (Var "D")) "," (Set (Var "T")) ")" ")" ) ($#k15_index_1 :::"*"::: ) (Set (Var "I1"))))))))) ; theorem :: INDEX_1:34 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "E")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k15_index_1 :::"*"::: ) (Set (Var "I")) ")" ) ($#k14_index_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k15_index_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "F")) ")" ))))))))) ; theorem :: INDEX_1:35 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T")) "," (Set (Var "D")) (Bool "for" (Set (Var "J")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "J")) ($#k14_index_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k16_index_1 :::"*"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "J")) ($#k16_index_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "I")) ")" ))))))))) ; theorem :: INDEX_1:36 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "T1")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "J")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "T2")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "J")) (Bool "for" (Set (Var "D")) "being" ($#v3_cat_5 :::"Categorial"::: ) ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "T2")) "," (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set (Var "J")) ")" ) ($#k16_index_1 :::"*"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_index_1 :::"*"::: ) (Set "(" (Set (Var "J")) ($#k16_index_1 :::"*"::: ) (Set (Var "I")) ")" )))))))))) ; theorem :: INDEX_1:37 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "T")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "J")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" (Set (Var "J")) ($#k16_index_1 :::"*"::: ) (Set (Var "I")) ")" ) ($#k14_index_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "J")) ($#k16_index_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k14_index_1 :::"*"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: INDEX_1:38 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "I")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "D")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "J")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "E")) "being" ($#m4_index_1 :::"TargetCat"::: ) "of" (Set (Var "J")) (Bool "for" (Set (Var "K")) "being" ($#m5_index_1 :::"Indexing":::) "of" (Set (Var "E")) "holds" (Bool (Set (Set "(" (Set (Var "K")) ($#k16_index_1 :::"*"::: ) (Set (Var "J")) ")" ) ($#k16_index_1 :::"*"::: ) (Set (Var "I"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "K")) ($#k16_index_1 :::"*"::: ) (Set "(" (Set (Var "J")) ($#k16_index_1 :::"*"::: ) (Set (Var "I")) ")" ))))))))) ; theorem :: INDEX_1:39 (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k7_isocat_1 :::"IdMap"::: ) (Set (Var "C"))) ($#r1_funct_2 :::"="::: ) (Set ($#k7_isocat_1 :::"IdMap"::: ) (Set "(" (Set (Var "C")) ($#k2_oppcat_1 :::"opp"::: ) ")" )))) ;