:: FUNCTOR0 semantic presentation begin scheme :: FUNCTOR0:sch 1 ValOnPair{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"Function":::), F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool (Set (Set F2 "(" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) ")" )) provided (Bool (Set F2 "(" ")" ) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "o9")) ($#k4_tarski :::"]"::: ) ) "," (Set F5 "(" (Set (Var "o")) "," (Set (Var "o9")) ")" ) ($#k4_tarski :::"]"::: ) ) where o, o9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "o")) "," (Set (Var "o9"))]) "}" ) and (Bool P1[(Set F3 "(" ")" ) "," (Set F4 "(" ")" )]) proof end; theorem :: FUNCTOR0:1 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FUNCTOR0:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "M")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "M"))))) ; registrationlet "f" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k2_funct_4 :::"~"::: ) "f") -> ($#v1_xboole_0 :::"empty"::: ) ; let "g" be ($#m1_hidden :::"Function":::); cluster (Set ($#k15_funct_3 :::"[:"::: ) "f" "," "g" ($#k15_funct_3 :::":]"::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set ($#k15_funct_3 :::"[:"::: ) "g" "," "f" ($#k15_funct_3 :::":]"::: ) ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: FUNCTOR0:3 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ))))) ; theorem :: FUNCTOR0:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) "iff" (Bool (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "f")) ($#k16_funct_3 :::":]"::: ) ) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ))) ; registrationlet "f" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k2_funct_4 :::"~"::: ) "f") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; theorem :: FUNCTOR0:5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))))) ; theorem :: FUNCTOR0:6 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k15_funct_3 :::":]"::: ) ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k15_funct_3 :::"[:"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) "," (Set "(" (Set (Var "g")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k15_funct_3 :::":]"::: ) ))) ; theorem :: FUNCTOR0:7 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "f")) ($#k15_funct_3 :::":]"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; theorem :: FUNCTOR0:8 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "f"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; theorem :: FUNCTOR0:9 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k15_funct_3 :::":]"::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k15_funct_3 :::":]"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; theorem :: FUNCTOR0:10 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set "(" ($#k2_funct_4 :::"~"::: ) (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k15_funct_3 :::":]"::: ) ) ")" ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_4 :::"~"::: ) (Set "(" (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k15_funct_3 :::":]"::: ) ) ($#k2_funct_1 :::"""::: ) ")" )))) ; theorem :: FUNCTOR0:11 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "B"))) ($#r1_relset_1 :::"c="::: ) (Set (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "f")) ($#k16_funct_3 :::":]"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" ))))) ; theorem :: FUNCTOR0:12 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k8_pboole :::"**"::: ) (Set "(" (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ))))) ; definitionlet "A", "B", "C" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "A")) "," (Set (Const "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "C")); :: original: :::"~"::: redefine func :::"~"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) "," "C"; end; theorem :: FUNCTOR0:13 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "C")) "st" (Bool (Bool (Set ($#k1_functor0 :::"~"::: ) (Set (Var "f"))) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ))) ; theorem :: FUNCTOR0:14 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "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 "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "f")) ($#k16_funct_3 :::":]"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "A")) ")" )) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "B"))))))) ; begin definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; mode bifunction of "A" "," "B" is ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ); end; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"bifunction":::) "of" (Set (Const "A")) "," (Set (Const "B")); attr "f" is :::"Covariant"::: means :: FUNCTOR0:def 1 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "A" "," "B" "st" (Bool "f" ($#r8_binop_1 :::"="::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "g")) "," (Set (Var "g")) ($#k16_funct_3 :::":]"::: ) ))); attr "f" is :::"Contravariant"::: means :: FUNCTOR0:def 2 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" "A" "," "B" "st" (Bool "f" ($#r8_binop_1 :::"="::: ) (Set ($#k1_functor0 :::"~"::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "g")) "," (Set (Var "g")) ($#k16_funct_3 :::":]"::: ) )))); end; :: deftheorem defines :::"Covariant"::: FUNCTOR0:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bifunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_functor0 :::"Covariant"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Set (Var "f")) ($#r8_binop_1 :::"="::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "g")) "," (Set (Var "g")) ($#k16_funct_3 :::":]"::: ) ))) ")" ))); :: deftheorem defines :::"Contravariant"::: FUNCTOR0:def 2 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bifunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_functor0 :::"Contravariant"::: ) ) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Set (Var "f")) ($#r8_binop_1 :::"="::: ) (Set ($#k1_functor0 :::"~"::: ) (Set ($#k16_funct_3 :::"[:"::: ) (Set (Var "g")) "," (Set (Var "g")) ($#k16_funct_3 :::":]"::: ) )))) ")" ))); theorem :: FUNCTOR0:15 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"bifunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "f")) ($#r6_pboole :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_functor0 :::"Covariant"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_functor0 :::"Contravariant"::: ) ) ")" ))))) ; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_functor0 :::"Covariant"::: ) ($#v2_functor0 :::"Contravariant"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: FUNCTOR0:16 (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")) "being" ($#v1_functor0 :::"Covariant"::: ) ($#v2_functor0 :::"Contravariant"::: ) ($#m1_subset_1 :::"bifunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "st" (Bool (Set (Var "f")) ($#r8_pboole :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "A")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "b")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )))))) ; begin definitionlet "I1", "I2" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I1")) "," (Set (Const "I2")); let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I1")); let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I2")); mode :::"MSUnTrans"::: "of" "f" "," "A" "," "B" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I1" means :: FUNCTOR0:def 3 (Bool "ex" (Set (Var "I29")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "B9")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I29"))(Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" "I1" "," (Set (Var "I29")) "st" (Bool "(" (Bool "f" ($#r1_hidden :::"="::: ) (Set (Var "f9"))) & (Bool "B" ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool it "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," (Set (Set (Var "B9")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f9")))) ")" )))) if (Bool "I2" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Bool it ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) "I1")); end; :: deftheorem defines :::"MSUnTrans"::: FUNCTOR0:def 3 : (Bool "for" (Set (Var "I1")) "," (Set (Var "I2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I1")) "," (Set (Var "I2")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I1")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I2")) (Bool "for" (Set (Var "b6")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I1")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "I2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Var "f")) "," (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "I29")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "B9")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I29"))(Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I1")) "," (Set (Var "I29")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "f9"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "B9"))) & (Bool (Set (Var "b6")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Set (Var "B9")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f9")))) ")" )))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "I2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Var "f")) "," (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool (Set (Var "b6")) ($#r6_pboole :::"="::: ) (Set ($#k1_pboole :::"[[0]]"::: ) (Set (Var "I1")))) ")" ) ")" ")" )))))); definitionlet "I1" be ($#m1_hidden :::"set"::: ) ; let "I2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I1")) "," (Set (Const "I2")); let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I1")); let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I2")); redefine mode :::"MSUnTrans"::: "of" "f" "," "A" "," "B" means :: FUNCTOR0:def 4 (Bool it "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," (Set "B" ($#k3_relat_1 :::"*"::: ) "f")); end; :: deftheorem defines :::"MSUnTrans"::: FUNCTOR0:def 4 : (Bool "for" (Set (Var "I1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I2")) "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 "I1")) "," (Set (Var "I2")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I1")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I2")) (Bool "for" (Set (Var "b6")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I1")) "holds" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Var "f")) "," (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool (Set (Var "b6")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Set (Var "B")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) ")" ))))))); registrationlet "I1", "I2" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I1")) "," (Set (Const "I2")); let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I1")); let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I2")); cluster -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_functor0 :::"MSUnTrans"::: ) "of" "f" "," "A" "," "B"; end; theorem :: FUNCTOR0:17 (Bool "for" (Set (Var "I1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I2")) "," (Set (Var "I3")) "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 "I1")) "," (Set (Var "I2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I2")) "," (Set (Var "I3")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I2")) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I3")) (Bool "for" (Set (Var "G")) "being" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Var "g")) "," (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "," (Set (Set (Var "B")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "," (Set (Var "C")))))))))) ; definitionlet "I1" be ($#m1_hidden :::"set"::: ) ; let "I2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "I1")) "," (Set (Const "I2")); let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "I1")) "," (Set (Const "I1")) ($#k2_zfmisc_1 :::":]"::: ) ); let "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "I2")) "," (Set (Const "I2")) ($#k2_zfmisc_1 :::":]"::: ) ); let "F" be ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set ($#k16_funct_3 :::"[:"::: ) (Set (Const "f")) "," (Set (Const "f")) ($#k16_funct_3 :::":]"::: ) ) "," (Set (Const "A")) "," (Set (Const "B")); :: original: :::"~"::: redefine func :::"~"::: "F" -> ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set ($#k16_funct_3 :::"[:"::: ) "f" "," "f" ($#k16_funct_3 :::":]"::: ) ) "," (Set ($#k2_funct_4 :::"~"::: ) "A") "," (Set ($#k2_funct_4 :::"~"::: ) "B"); end; theorem :: FUNCTOR0:18 (Bool "for" (Set (Var "I1")) "," (Set (Var "I2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I1")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I2")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I2")) "st" (Bool (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I1")) "," (Set (Var "I2")) "st" (Bool (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "I1")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "o"))))) "holds" (Bool "{" (Set ($#k4_tarski :::"["::: ) (Set (Var "o9")) "," (Set "(" (Set "(" (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "o9")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) ) where o9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I1")) : (Bool verum) "}" "is" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Var "f")) "," (Set (Var "A")) "," (Set (Var "B"))))))))) ; theorem :: FUNCTOR0:19 (Bool "for" (Set (Var "I1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I2")) "," (Set (Var "I3")) "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 "I1")) "," (Set (Var "I2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "I2")) "," (Set (Var "I3")) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I1")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I2")) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I3")) (Bool "for" (Set (Var "F")) "being" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Var "f")) "," (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "," (Set (Set (Var "B")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "," (Set (Var "C")) "st" (Bool (Bool "(" "for" (Set (Var "ii")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "ii")) ($#r2_hidden :::"in"::: ) (Set (Var "I1"))) & (Bool (Set (Set "(" (Set (Var "B")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "ii"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "ii"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "C")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "ii"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "G")) ($#k8_pboole :::"**"::: ) (Set (Var "F"))) "is" ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "," (Set (Var "A")) "," (Set (Var "C")))))))))))) ; begin definitionlet "C1", "C2" be ($#l1_struct_0 :::"1-sorted"::: ) ; attr "c3" is :::"strict"::: ; struct :::"BimapStr"::: "over" "C1" "," "C2" -> ; aggr :::"BimapStr":::(# :::"ObjectMap"::: #) -> ($#l1_functor0 :::"BimapStr"::: ) "over" "C1" "," "C2"; sel :::"ObjectMap"::: "c3" -> ($#m1_subset_1 :::"bifunction":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C2"); end; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C1")); func "F" :::"."::: "o" -> ($#m1_subset_1 :::"object":::) "of" "C2" equals :: FUNCTOR0:def 5 (Set (Set "(" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ($#k2_binop_1 :::"."::: ) "(" "o" "," "o" ")" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ); end; :: deftheorem defines :::"."::: FUNCTOR0:def 5 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "o")) "," (Set (Var "o")) ")" ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))))); definitionlet "A", "B" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "F" be ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); attr "F" is :::"one-to-one"::: means :: FUNCTOR0:def 6 (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") "is" ($#v2_funct_1 :::"one-to-one"::: ) ); attr "F" is :::"onto"::: means :: FUNCTOR0:def 7 (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") "is" ($#v2_funct_2 :::"onto"::: ) ); attr "F" is :::"reflexive"::: means :: FUNCTOR0:def 8 (Bool (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") ")" )) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B"))); attr "F" is :::"coreflexive"::: means :: FUNCTOR0:def 9 (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B")) ($#r1_relset_1 :::"c="::: ) (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") ")" ))); end; :: deftheorem defines :::"one-to-one"::: FUNCTOR0:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_functor0 :::"one-to-one"::: ) ) "iff" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" ))); :: deftheorem defines :::"onto"::: FUNCTOR0:def 7 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v5_functor0 :::"onto"::: ) ) "iff" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ))); :: deftheorem defines :::"reflexive"::: FUNCTOR0:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_functor0 :::"reflexive"::: ) ) "iff" (Bool (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ")" )) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))))) ")" ))); :: deftheorem defines :::"coreflexive"::: FUNCTOR0:def 9 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) ) "iff" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B")))) ($#r1_relset_1 :::"c="::: ) (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ")" ))) ")" ))); definitionlet "A", "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); redefine attr "F" is :::"reflexive"::: means :: FUNCTOR0:def 10 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "o")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" ) ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"reflexive"::: FUNCTOR0:def 10 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v6_functor0 :::"reflexive"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "o")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" ) ($#k4_tarski :::"]"::: ) ))) ")" ))); theorem :: FUNCTOR0:20 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) )) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) (Bool "ex" (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Set (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o9"))) ($#r1_hidden :::"="::: ) (Set (Var "o"))))))) ; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); attr "F" is :::"feasible"::: means :: FUNCTOR0:def 11 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "C2") ($#k1_funct_1 :::"."::: ) (Set "(" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ($#k2_binop_1 :::"."::: ) "(" (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); end; :: deftheorem defines :::"feasible"::: FUNCTOR0:def 11 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v8_functor0 :::"feasible"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "C2"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))); definitionlet "C1", "C2" be ($#l1_altcat_1 :::"AltGraph"::: ) ; attr "c3" is :::"strict"::: ; struct :::"FunctorStr"::: "over" "C1" "," "C2" -> ($#l1_functor0 :::"BimapStr"::: ) "over" "C1" "," "C2"; aggr :::"FunctorStr":::(# :::"ObjectMap":::, :::"MorphMap"::: #) -> ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2"; sel :::"MorphMap"::: "c3" -> ($#m1_functor0 :::"MSUnTrans"::: ) "of" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "c3") "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "C1") "," (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "C2"); end; definitionlet "C1", "C2" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "IT" be ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); attr "IT" is :::"Covariant"::: means :: FUNCTOR0:def 12 (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "IT") "is" ($#v1_functor0 :::"Covariant"::: ) ); attr "IT" is :::"Contravariant"::: means :: FUNCTOR0:def 13 (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "IT") "is" ($#v2_functor0 :::"Contravariant"::: ) ); end; :: deftheorem defines :::"Covariant"::: FUNCTOR0:def 12 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v10_functor0 :::"Covariant"::: ) ) "iff" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "IT"))) "is" ($#v1_functor0 :::"Covariant"::: ) ) ")" ))); :: deftheorem defines :::"Contravariant"::: FUNCTOR0:def 13 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v11_functor0 :::"Contravariant"::: ) ) "iff" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "IT"))) "is" ($#v2_functor0 :::"Contravariant"::: ) ) ")" ))); registrationlet "C1", "C2" be ($#l1_altcat_1 :::"AltGraph"::: ) ; cluster ($#v10_functor0 :::"Covariant"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2"; cluster ($#v11_functor0 :::"Contravariant"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2"; end; definitionlet "C1", "C2" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C1")); func :::"Morph-Map"::: "(" "F" "," "o1" "," "o2" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCTOR0:def 14 (Set (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "F") ($#k1_binop_1 :::"."::: ) "(" "o1" "," "o2" ")" ); end; :: deftheorem defines :::"Morph-Map"::: FUNCTOR0:def 14 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "o1")) "," (Set (Var "o2")) ")" ))))); registrationlet "C1", "C2" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C1")); cluster (Set ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," "o1" "," "o2" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C1")); :: original: :::"Morph-Map"::: redefine func :::"Morph-Map"::: "(" "F" "," "o1" "," "o2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_altcat_1 :::"<^"::: ) "o1" "," "o2" ($#k1_altcat_1 :::"^>"::: ) ) "," (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) "o1" ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) "o2" ")" ) ($#k1_altcat_1 :::"^>"::: ) ); end; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C1")); assume that (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Const "o1")) "," (Set (Const "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) and (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Const "F")) ($#k3_functor0 :::"."::: ) (Set (Const "o1")) ")" ) "," (Set "(" (Set (Const "F")) ($#k3_functor0 :::"."::: ) (Set (Const "o2")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "m" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); func "F" :::"."::: "m" -> ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F" ($#k3_functor0 :::"."::: ) "o1" ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) "o2" ")" ) equals :: FUNCTOR0:def 15 (Set (Set "(" ($#k5_functor0 :::"Morph-Map"::: ) "(" "F" "," "o1" "," "o2" ")" ")" ) ($#k1_funct_1 :::"."::: ) "m"); end; :: deftheorem defines :::"."::: FUNCTOR0:def 15 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))))); definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C1")); :: original: :::"Morph-Map"::: redefine func :::"Morph-Map"::: "(" "F" "," "o1" "," "o2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_altcat_1 :::"<^"::: ) "o1" "," "o2" ($#k1_altcat_1 :::"^>"::: ) ) "," (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) "o2" ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) "o1" ")" ) ($#k1_altcat_1 :::"^>"::: ) ); end; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "o1", "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C1")); assume that (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Const "o1")) "," (Set (Const "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) and (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Const "F")) ($#k3_functor0 :::"."::: ) (Set (Const "o2")) ")" ) "," (Set "(" (Set (Const "F")) ($#k3_functor0 :::"."::: ) (Set (Const "o1")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "m" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o1")) "," (Set (Const "o2")); func "F" :::"."::: "m" -> ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F" ($#k3_functor0 :::"."::: ) "o2" ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) "o1" ")" ) equals :: FUNCTOR0:def 16 (Set (Set "(" ($#k7_functor0 :::"Morph-Map"::: ) "(" "F" "," "o1" "," "o2" ")" ")" ) ($#k1_funct_1 :::"."::: ) "m"); end; :: deftheorem defines :::"."::: FUNCTOR0:def 16 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))))))); definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C2")); assume (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Const "o")) "," (Set (Const "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; let "m" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o")) "," (Set (Const "o")); func "C1" :::"-->"::: "m" -> ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2" means :: FUNCTOR0:def 17 (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" it) ($#r8_pboole :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C1") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C1") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) "o" "," "o" ($#k4_tarski :::"]"::: ) ))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" it) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#k7_funcop_1 :::"-->"::: ) "m" ")" ) ($#k4_tarski :::"]"::: ) ) where o1, o2 "is" ($#m1_subset_1 :::"object":::) "of" "C1" : (Bool verum) "}" ) ")" ); end; :: deftheorem defines :::"-->"::: FUNCTOR0:def 17 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o")) (Bool "for" (Set (Var "b5")) "being" ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k9_functor0 :::"-->"::: ) (Set (Var "m")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "b5"))) ($#r8_pboole :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C1"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set (Var "o")) ($#k4_tarski :::"]"::: ) ))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "b5"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k4_tarski :::"]"::: ) ) "," (Set "(" (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) ) where o1, o2 "is" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) : (Bool verum) "}" ) ")" ) ")" ))))); theorem :: FUNCTOR0:21 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o2")) (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "(" (Set (Var "C1")) ($#k9_functor0 :::"-->"::: ) (Set (Var "m")) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o1"))) ($#r1_hidden :::"="::: ) (Set (Var "o2"))))))) ; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C2")); let "m" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o")) "," (Set (Const "o")); cluster (Set "C1" ($#k9_functor0 :::"-->"::: ) "m") -> ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v11_functor0 :::"Contravariant"::: ) ; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; cluster ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v11_functor0 :::"Contravariant"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2"; end; theorem :: FUNCTOR0:22 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "o1")) "," (Set (Var "o2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) ($#k4_tarski :::"]"::: ) ))))) ; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); redefine attr "F" is :::"feasible"::: means :: FUNCTOR0:def 18 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); end; :: deftheorem defines :::"feasible"::: FUNCTOR0:def 18 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v8_functor0 :::"feasible"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))); theorem :: FUNCTOR0:23 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "o1")) "," (Set (Var "o2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) ($#k4_tarski :::"]"::: ) ))))) ; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); redefine attr "F" is :::"feasible"::: means :: FUNCTOR0:def 19 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); end; :: deftheorem defines :::"feasible"::: FUNCTOR0:def 19 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v8_functor0 :::"feasible"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))); registrationlet "C1", "C2" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); cluster (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "F") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); attr "F" is :::"id-preserving"::: means :: FUNCTOR0:def 20 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "holds" (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "o")) "," (Set (Var "o")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" )))); end; :: deftheorem defines :::"id-preserving"::: FUNCTOR0:def 20 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v12_functor0 :::"id-preserving"::: ) ) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o")) "," (Set (Var "o")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" )))) ")" ))); theorem :: FUNCTOR0:24 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o2")) (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o9")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set "(" (Set (Var "C1")) ($#k9_functor0 :::"-->"::: ) (Set (Var "m")) ")" ) "," (Set (Var "o")) "," (Set (Var "o9")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "m")))))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; registrationlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C2")); cluster (Set "C1" ($#k9_functor0 :::"-->"::: ) (Set "(" ($#k8_altcat_1 :::"idm"::: ) "o2" ")" )) -> ($#v9_functor0 :::"strict"::: ) ($#v12_functor0 :::"id-preserving"::: ) ; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "o2" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C2")); let "m" be ($#m1_subset_1 :::"Morphism":::) "of" (Set (Const "o2")) "," (Set (Const "o2")); cluster (Set "C1" ($#k9_functor0 :::"-->"::: ) "m") -> ($#v6_functor0 :::"reflexive"::: ) ($#v9_functor0 :::"strict"::: ) ; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; cluster ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2"; end; registrationlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ($#v12_functor0 :::"id-preserving"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2"; end; definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); attr "F" is :::"comp-preserving"::: means :: FUNCTOR0:def 21 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" )(Bool "ex" (Set (Var "g9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o3")) ")" ) "st" (Bool "(" (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")))) & (Bool (Set (Var "g9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "o2")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "o1")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g9")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f9")))) ")" )))))); end; :: deftheorem defines :::"comp-preserving"::: FUNCTOR0:def 21 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v13_functor0 :::"comp-preserving"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" )(Bool "ex" (Set (Var "g9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o3")) ")" ) "st" (Bool "(" (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")))) & (Bool (Set (Var "g9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o2")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g9")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f9")))) ")" )))))) ")" ))); definitionlet "C1", "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); attr "F" is :::"comp-reversing"::: means :: FUNCTOR0:def 22 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" )(Bool "ex" (Set (Var "g9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o3")) ")" ) "," (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "st" (Bool "(" (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")))) & (Bool (Set (Var "g9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "o2")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" "F" "," (Set (Var "o1")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f9")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "g9")))) ")" )))))); end; :: deftheorem defines :::"comp-reversing"::: FUNCTOR0:def 22 : (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v14_functor0 :::"comp-reversing"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "ex" (Set (Var "f9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" )(Bool "ex" (Set (Var "g9")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o3")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "st" (Bool "(" (Bool (Set (Var "f9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f")))) & (Bool (Set (Var "g9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o2")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")))) & (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o1")) "," (Set (Var "o3")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f9")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "g9")))) ")" )))))) ")" ))); definitionlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); redefine attr "F" is :::"comp-preserving"::: means :: FUNCTOR0:def 23 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "holds" (Bool (Set "F" ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k6_functor0 :::"."::: ) (Set (Var "g")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" "F" ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )))))); end; :: deftheorem defines :::"comp-preserving"::: FUNCTOR0:def 23 : (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v13_functor0 :::"comp-preserving"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "holds" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "g")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )))))) ")" )))); definitionlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); redefine attr "F" is :::"comp-reversing"::: means :: FUNCTOR0:def 24 (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" "C1" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "holds" (Bool (Set "F" ($#k8_functor0 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "F" ($#k8_functor0 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" "F" ($#k8_functor0 :::"."::: ) (Set (Var "g")) ")" )))))); end; :: deftheorem defines :::"comp-reversing"::: FUNCTOR0:def 24 : (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v14_functor0 :::"comp-reversing"::: ) ) "iff" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o2")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) "holds" (Bool (Set (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set "(" (Set (Var "g")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k8_functor0 :::"."::: ) (Set (Var "g")) ")" )))))) ")" )))); theorem :: FUNCTOR0:25 (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o2")) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C1")) ($#k9_functor0 :::"-->"::: ) (Set (Var "m"))))) "holds" (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o9")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "m")))))))))) ; theorem :: FUNCTOR0:26 (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o2")) (Bool "for" (Set (Var "o")) "," (Set (Var "o9")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o")) "," (Set (Var "o9")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o")) "," (Set (Var "o9")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "C1")) ($#k9_functor0 :::"-->"::: ) (Set (Var "m")) ")" ) ($#k8_functor0 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))))))))) ; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "o" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "C2")); cluster (Set "C1" ($#k9_functor0 :::"-->"::: ) (Set "(" ($#k8_altcat_1 :::"idm"::: ) "o" ")" )) -> ($#v9_functor0 :::"strict"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ($#v14_functor0 :::"comp-reversing"::: ) ; end; definitionlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; mode :::"Functor"::: "of" "C1" "," "C2" -> ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C2" means :: FUNCTOR0:def 25 (Bool "(" (Bool it "is" ($#v8_functor0 :::"feasible"::: ) ) & (Bool it "is" ($#v12_functor0 :::"id-preserving"::: ) ) & (Bool "(" (Bool "(" (Bool it "is" ($#v10_functor0 :::"Covariant"::: ) ) & (Bool it "is" ($#v13_functor0 :::"comp-preserving"::: ) ) ")" ) "or" (Bool "(" (Bool it "is" ($#v11_functor0 :::"Contravariant"::: ) ) & (Bool it "is" ($#v14_functor0 :::"comp-reversing"::: ) ) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"Functor"::: FUNCTOR0:def 25 : (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2"))) "iff" (Bool "(" (Bool (Set (Var "b3")) "is" ($#v8_functor0 :::"feasible"::: ) ) & (Bool (Set (Var "b3")) "is" ($#v12_functor0 :::"id-preserving"::: ) ) & (Bool "(" (Bool "(" (Bool (Set (Var "b3")) "is" ($#v10_functor0 :::"Covariant"::: ) ) & (Bool (Set (Var "b3")) "is" ($#v13_functor0 :::"comp-preserving"::: ) ) ")" ) "or" (Bool "(" (Bool (Set (Var "b3")) "is" ($#v11_functor0 :::"Contravariant"::: ) ) & (Bool (Set (Var "b3")) "is" ($#v14_functor0 :::"comp-reversing"::: ) ) ")" ) ")" ) ")" ) ")" )))); definitionlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "C1")) "," (Set (Const "C2")); attr "F" is :::"covariant"::: means :: FUNCTOR0:def 26 (Bool "(" (Bool "F" "is" ($#v10_functor0 :::"Covariant"::: ) ) & (Bool "F" "is" ($#v13_functor0 :::"comp-preserving"::: ) ) ")" ); attr "F" is :::"contravariant"::: means :: FUNCTOR0:def 27 (Bool "(" (Bool "F" "is" ($#v11_functor0 :::"Contravariant"::: ) ) & (Bool "F" "is" ($#v14_functor0 :::"comp-reversing"::: ) ) ")" ); end; :: deftheorem defines :::"covariant"::: FUNCTOR0:def 26 : (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v15_functor0 :::"covariant"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v10_functor0 :::"Covariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v13_functor0 :::"comp-preserving"::: ) ) ")" ) ")" )))); :: deftheorem defines :::"contravariant"::: FUNCTOR0:def 27 : (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v16_functor0 :::"contravariant"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v11_functor0 :::"Contravariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v14_functor0 :::"comp-reversing"::: ) ) ")" ) ")" )))); definitionlet "A" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Const "A")); func :::"incl"::: "B" -> ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" "B" "," "A" means :: FUNCTOR0:def 28 (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "B") ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" it) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "B"))) ")" ); end; :: deftheorem defines :::"incl"::: FUNCTOR0:def 28 : (Bool "for" (Set (Var "A")) "being" ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_functor0 :::"incl"::: ) (Set (Var "B")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "B"))) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "b3"))) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "B"))))) ")" ) ")" )))); definitionlet "A" be ($#l1_altcat_1 :::"AltGraph"::: ) ; func :::"id"::: "A" -> ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" "A" "," "A" means :: FUNCTOR0:def 29 (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" it) ($#r8_binop_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" it) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "A"))) ")" ); end; :: deftheorem defines :::"id"::: FUNCTOR0:def 29 : (Bool "for" (Set (Var "A")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "b2")) "being" ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_functor0 :::"id"::: ) (Set (Var "A")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "b2"))) ($#r8_binop_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "b2"))) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_3 :::"id"::: ) (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "A"))))) ")" ) ")" ))); registrationlet "A" be ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Const "A")); cluster (Set ($#k10_functor0 :::"incl"::: ) "B") -> ($#v9_functor0 :::"strict"::: ) ($#v10_functor0 :::"Covariant"::: ) ; end; theorem :: FUNCTOR0:27 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k10_functor0 :::"incl"::: ) (Set (Var "B")) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "o")))))) ; theorem :: FUNCTOR0:28 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set "(" ($#k10_functor0 :::"incl"::: ) (Set (Var "B")) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" (Set "(" ($#k10_functor0 :::"incl"::: ) (Set (Var "B")) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ))))) ; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Const "A")); cluster (Set ($#k10_functor0 :::"incl"::: ) "B") -> ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ; end; definitionlet "A", "B" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); attr "F" is :::"faithful"::: means :: FUNCTOR0:def 30 (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "F") "is" ($#v1_msualg_3 :::""1-1""::: ) ); end; :: deftheorem defines :::"faithful"::: FUNCTOR0:def 30 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v17_functor0 :::"faithful"::: ) ) "iff" (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F"))) "is" ($#v1_msualg_3 :::""1-1""::: ) ) ")" ))); definitionlet "A", "B" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); attr "F" is :::"full"::: means :: FUNCTOR0:def 31 (Bool "ex" (Set (Var "B9")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "A") "," (Set (Var "B9")) "st" (Bool "(" (Bool (Set (Var "B9")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "B") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F"))) & (Bool (Set (Var "f")) ($#r6_pboole :::"="::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "F")) & (Bool (Set (Var "f")) "is" ($#v2_msualg_3 :::""onto""::: ) ) ")" ))); end; :: deftheorem defines :::"full"::: FUNCTOR0:def 31 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v18_functor0 :::"full"::: ) ) "iff" (Bool "ex" (Set (Var "B9")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) ($#k2_zfmisc_1 :::":]"::: ) )(Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "A"))) "," (Set (Var "B9")) "st" (Bool "(" (Bool (Set (Var "B9")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "B"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))))) & (Bool (Set (Var "f")) ($#r6_pboole :::"="::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F")))) & (Bool (Set (Var "f")) "is" ($#v2_msualg_3 :::""onto""::: ) ) ")" ))) ")" ))); definitionlet "A" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); redefine attr "F" is :::"full"::: means :: FUNCTOR0:def 32 (Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "A") "," (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "B") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r6_pboole :::"="::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "F")) & (Bool (Set (Var "f")) "is" ($#v2_msualg_3 :::""onto""::: ) ) ")" )); end; :: deftheorem defines :::"full"::: FUNCTOR0:def 32 : (Bool "for" (Set (Var "A")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v18_functor0 :::"full"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "A"))) "," (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "B"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F")))) "st" (Bool "(" (Bool (Set (Var "f")) ($#r6_pboole :::"="::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F")))) & (Bool (Set (Var "f")) "is" ($#v2_msualg_3 :::""onto""::: ) ) ")" )) ")" )))); definitionlet "A", "B" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); attr "F" is :::"injective"::: means :: FUNCTOR0:def 33 (Bool "(" (Bool "F" "is" ($#v4_functor0 :::"one-to-one"::: ) ) & (Bool "F" "is" ($#v17_functor0 :::"faithful"::: ) ) ")" ); attr "F" is :::"surjective"::: means :: FUNCTOR0:def 34 (Bool "(" (Bool "F" "is" ($#v18_functor0 :::"full"::: ) ) & (Bool "F" "is" ($#v5_functor0 :::"onto"::: ) ) ")" ); end; :: deftheorem defines :::"injective"::: FUNCTOR0:def 33 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v19_functor0 :::"injective"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v4_functor0 :::"one-to-one"::: ) ) & (Bool (Set (Var "F")) "is" ($#v17_functor0 :::"faithful"::: ) ) ")" ) ")" ))); :: deftheorem defines :::"surjective"::: FUNCTOR0:def 34 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v20_functor0 :::"surjective"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v18_functor0 :::"full"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_functor0 :::"onto"::: ) ) ")" ) ")" ))); definitionlet "A", "B" be ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); attr "F" is :::"bijective"::: means :: FUNCTOR0:def 35 (Bool "(" (Bool "F" "is" ($#v19_functor0 :::"injective"::: ) ) & (Bool "F" "is" ($#v20_functor0 :::"surjective"::: ) ) ")" ); end; :: deftheorem defines :::"bijective"::: FUNCTOR0:def 35 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v19_functor0 :::"injective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v20_functor0 :::"surjective"::: ) ) ")" ) ")" ))); registrationlet "A", "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#v16_functor0 :::"contravariant"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B"; end; theorem :: FUNCTOR0:29 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k11_functor0 :::"id"::: ) (Set (Var "A")) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "o"))))) ; theorem :: FUNCTOR0:30 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set "(" ($#k11_functor0 :::"id"::: ) (Set (Var "A")) ")" ) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "m")))))) ; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; cluster (Set ($#k11_functor0 :::"id"::: ) "A") -> ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ($#v10_functor0 :::"Covariant"::: ) ; end; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; cluster ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "A" "," "A"; end; theorem :: FUNCTOR0:31 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k11_functor0 :::"id"::: ) (Set (Var "A"))))) "holds" (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "holds" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))))))) ; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster (Set ($#k11_functor0 :::"id"::: ) "A") -> ($#v9_functor0 :::"strict"::: ) ($#v12_functor0 :::"id-preserving"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ; end; definitionlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; :: original: :::"id"::: redefine func :::"id"::: "A" -> ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "A"; end; registrationlet "A" be ($#l1_altcat_1 :::"AltGraph"::: ) ; cluster (Set ($#k11_functor0 :::"id"::: ) "A") -> ($#v9_functor0 :::"strict"::: ) ($#v21_functor0 :::"bijective"::: ) ; end; begin definitionlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2", "C3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "G" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C2")) "," (Set (Const "C3")); func "G" :::"*"::: "F" -> ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" "C1" "," "C3" means :: FUNCTOR0:def 36 (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" it) ($#r8_binop_1 :::"="::: ) (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "G") ($#k1_partfun1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F"))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" it) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "G") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ")" ) ($#k8_pboole :::"**"::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "F"))) ")" ); end; :: deftheorem defines :::"*"::: FUNCTOR0:def 36 : (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "G")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C2")) "," (Set (Var "C3")) (Bool "for" (Set (Var "b6")) "being" ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C3")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "b6"))) ($#r8_binop_1 :::"="::: ) (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "G"))) ($#k1_partfun1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "b6"))) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "G"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ")" ) ($#k8_pboole :::"**"::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F"))))) ")" ) ")" )))))); registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2", "C3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "G" be ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C2")) "," (Set (Const "C3")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v9_functor0 :::"strict"::: ) ($#v10_functor0 :::"Covariant"::: ) ; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2", "C3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "G" be ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C2")) "," (Set (Const "C3")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v9_functor0 :::"strict"::: ) ($#v11_functor0 :::"Contravariant"::: ) ; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2", "C3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "G" be ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C2")) "," (Set (Const "C3")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v9_functor0 :::"strict"::: ) ($#v11_functor0 :::"Contravariant"::: ) ; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2", "C3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "G" be ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C2")) "," (Set (Const "C3")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v9_functor0 :::"strict"::: ) ($#v10_functor0 :::"Covariant"::: ) ; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "C2", "C3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "G" be ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C2")) "," (Set (Const "C3")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ; end; theorem :: FUNCTOR0:32 (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "C2")) "," (Set (Var "C3")) "," (Set (Var "C4")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "G")) "being" ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C2")) "," (Set (Var "C3")) (Bool "for" (Set (Var "H")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C3")) "," (Set (Var "C4")) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k13_functor0 :::"*"::: ) (Set (Var "G")) ")" ) ($#k13_functor0 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k13_functor0 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: FUNCTOR0:33 (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "G")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C2")) "," (Set (Var "C3")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_functor0 :::"."::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" )))))))) ; theorem :: FUNCTOR0:34 (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "C2")) "," (Set (Var "C3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) (Bool "for" (Set (Var "G")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "C2")) "," (Set (Var "C3")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C1")) "holds" (Bool (Set ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set "(" (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")) ")" ) "," (Set (Var "o")) "," (Set (Var "o")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" ) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o")) "," (Set (Var "o")) ")" ")" )))))))) ; registrationlet "C1", "C2", "C3" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#v12_functor0 :::"id-preserving"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C1")) "," (Set (Const "C2")); let "G" be ($#v12_functor0 :::"id-preserving"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "C2")) "," (Set (Const "C3")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v9_functor0 :::"strict"::: ) ($#v12_functor0 :::"id-preserving"::: ) ; end; definitionlet "A", "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Const "A")); let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "C")); func "F" :::"|"::: "B" -> ($#l2_functor0 :::"FunctorStr"::: ) "over" "B" "," "C" equals :: FUNCTOR0:def 37 (Set "F" ($#k13_functor0 :::"*"::: ) (Set "(" ($#k10_functor0 :::"incl"::: ) "B" ")" )); end; :: deftheorem defines :::"|"::: FUNCTOR0:def 37 : (Bool "for" (Set (Var "A")) "," (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_altcat_2 :::"SubCatStr"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "F")) ($#k14_functor0 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k13_functor0 :::"*"::: ) (Set "(" ($#k10_functor0 :::"incl"::: ) (Set (Var "B")) ")" )))))); begin definitionlet "A", "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) ; let "F" be ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) ; func "F" :::"""::: -> ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" "B" "," "A" means :: FUNCTOR0:def 38 (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ($#k2_funct_1 :::"""::: ) )) & (Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "A") "," (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" "B") ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r8_pboole :::"="::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" "F")) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k4_msualg_3 :::""""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" "F") ($#k2_funct_1 :::"""::: ) ")" ))) ")" )) ")" ); end; :: deftheorem defines :::"""::: FUNCTOR0:def 38 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_altcat_1 :::"AltGraph"::: ) (Bool "for" (Set (Var "F")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#v9_functor0 :::"strict"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k2_funct_1 :::"""::: ) )) & (Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "A"))) "," (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "B"))) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F")))) "st" (Bool "(" (Bool (Set (Var "f")) ($#r8_pboole :::"="::: ) (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F")))) & (Bool (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k4_msualg_3 :::""""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) ($#k2_funct_1 :::"""::: ) ")" ))) ")" )) ")" ) ")" )))); theorem :: FUNCTOR0:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v8_functor0 :::"feasible"::: ) ) ")" ))) ; theorem :: FUNCTOR0:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v6_functor0 :::"reflexive"::: ) ))) ; theorem :: FUNCTOR0:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#v12_functor0 :::"id-preserving"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v12_functor0 :::"id-preserving"::: ) ))) ; theorem :: FUNCTOR0:38 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v10_functor0 :::"Covariant"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v10_functor0 :::"Covariant"::: ) ))) ; theorem :: FUNCTOR0:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v11_functor0 :::"Contravariant"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v11_functor0 :::"Contravariant"::: ) ))) ; theorem :: FUNCTOR0:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v10_functor0 :::"Covariant"::: ) )) "holds" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" (Set (Var "F")) ($#k15_functor0 :::"""::: ) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" (Set "(" (Set (Var "F")) ($#k15_functor0 :::"""::: ) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_functor0 :::"""::: ) ")" ) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m"))))))) ; theorem :: FUNCTOR0:41 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) ) & (Bool (Set (Var "F")) "is" ($#v11_functor0 :::"Contravariant"::: ) )) "holds" (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "B")) (Bool "for" (Set (Var "m")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o1")) "," (Set (Var "o2")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set "(" (Set "(" (Set (Var "F")) ($#k15_functor0 :::"""::: ) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o2")) ")" ) "," (Set "(" (Set "(" (Set (Var "F")) ($#k15_functor0 :::"""::: ) ")" ) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_functor0 :::"""::: ) ")" ) "," (Set (Var "o1")) "," (Set (Var "o2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "m"))))))) ; theorem :: FUNCTOR0:42 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v13_functor0 :::"comp-preserving"::: ) ) & (Bool (Set (Var "F")) "is" ($#v10_functor0 :::"Covariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v13_functor0 :::"comp-preserving"::: ) ))) ; theorem :: FUNCTOR0:43 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v6_functor0 :::"reflexive"::: ) ($#v8_functor0 :::"feasible"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v14_functor0 :::"comp-reversing"::: ) ) & (Bool (Set (Var "F")) "is" ($#v11_functor0 :::"Contravariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) ) "is" ($#v14_functor0 :::"comp-reversing"::: ) ))) ; registrationlet "C1" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v10_functor0 :::"Covariant"::: ) -> ($#v6_functor0 :::"reflexive"::: ) for ($#l1_functor0 :::"BimapStr"::: ) "over" "C1" "," "C2"; end; registrationlet "C1" be ($#l1_struct_0 :::"1-sorted"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) ; cluster ($#v11_functor0 :::"Contravariant"::: ) -> ($#v6_functor0 :::"reflexive"::: ) for ($#l1_functor0 :::"BimapStr"::: ) "over" "C1" "," "C2"; end; theorem :: FUNCTOR0:44 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "M")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v10_functor0 :::"Covariant"::: ) ) & (Bool (Set (Var "M")) "is" ($#v5_functor0 :::"onto"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v7_functor0 :::"coreflexive"::: ) ))) ; theorem :: FUNCTOR0:45 (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "M")) "being" ($#l1_functor0 :::"BimapStr"::: ) "over" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set (Var "M")) "is" ($#v11_functor0 :::"Contravariant"::: ) ) & (Bool (Set (Var "M")) "is" ($#v5_functor0 :::"onto"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#v7_functor0 :::"coreflexive"::: ) ))) ; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#v15_functor0 :::"covariant"::: ) -> ($#v6_functor0 :::"reflexive"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "C1" "," "C2"; end; registrationlet "C1" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#v16_functor0 :::"contravariant"::: ) -> ($#v6_functor0 :::"reflexive"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "C1" "," "C2"; end; theorem :: FUNCTOR0:46 (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v15_functor0 :::"covariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_functor0 :::"onto"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) )))) ; theorem :: FUNCTOR0:47 (Bool "for" (Set (Var "C1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C1")) "," (Set (Var "C2")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v16_functor0 :::"contravariant"::: ) ) & (Bool (Set (Var "F")) "is" ($#v5_functor0 :::"onto"::: ) )) "holds" (Bool (Set (Var "F")) "is" ($#v7_functor0 :::"coreflexive"::: ) )))) ; theorem :: FUNCTOR0:48 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) )) & (Bool (Set (Var "G")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "G")) "is" ($#v15_functor0 :::"covariant"::: ) ) ")" )))) ; theorem :: FUNCTOR0:49 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) )) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k15_functor0 :::"""::: ) )) & (Bool (Set (Var "G")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "G")) "is" ($#v16_functor0 :::"contravariant"::: ) ) ")" )))) ; definitionlet "A", "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; pred "A" "," "B" :::"are_isomorphic"::: means :: FUNCTOR0:def 39 (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B" "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v15_functor0 :::"covariant"::: ) ) ")" )); reflexivity (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v15_functor0 :::"covariant"::: ) ) ")" ))) ; symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v15_functor0 :::"covariant"::: ) ) ")" ))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v15_functor0 :::"covariant"::: ) ) ")" ))) ; pred "A" "," "B" :::"are_anti-isomorphic"::: means :: FUNCTOR0:def 40 (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B" "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v16_functor0 :::"contravariant"::: ) ) ")" )); symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v16_functor0 :::"contravariant"::: ) ) ")" ))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v16_functor0 :::"contravariant"::: ) ) ")" ))) ; end; :: deftheorem defines :::"are_isomorphic"::: FUNCTOR0:def 39 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_functor0 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v15_functor0 :::"covariant"::: ) ) ")" )) ")" )); :: deftheorem defines :::"are_anti-isomorphic"::: FUNCTOR0:def 40 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_functor0 :::"are_anti-isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "F")) "is" ($#v21_functor0 :::"bijective"::: ) ) & (Bool (Set (Var "F")) "is" ($#v16_functor0 :::"contravariant"::: ) ) ")" )) ")" ));