:: FUNCTOR2 semantic presentation begin registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster -> ($#v8_functor0 :::"feasible"::: ) ($#v12_functor0 :::"id-preserving"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B"; end; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; cluster ($#v15_functor0 :::"covariant"::: ) -> ($#v10_functor0 :::"Covariant"::: ) ($#v13_functor0 :::"comp-preserving"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B"; cluster ($#v10_functor0 :::"Covariant"::: ) ($#v13_functor0 :::"comp-preserving"::: ) -> ($#v15_functor0 :::"covariant"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B"; cluster ($#v16_functor0 :::"contravariant"::: ) -> ($#v11_functor0 :::"Contravariant"::: ) ($#v14_functor0 :::"comp-reversing"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B"; cluster ($#v11_functor0 :::"Contravariant"::: ) ($#v14_functor0 :::"comp-reversing"::: ) -> ($#v16_functor0 :::"contravariant"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B"; end; theorem :: FUNCTOR2:1 (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")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set "(" ($#k8_altcat_1 :::"idm"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" )))))) ; begin 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"::: ) ; let "F1", "F2" be ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); pred "F1" :::"is_transformable_to"::: "F2" means :: FUNCTOR2:def 1 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" "F1" ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" "F2" ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); reflexivity (Bool "for" (Set (Var "F1")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Var "F1")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F1")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; end; :: deftheorem defines :::"is_transformable_to"::: FUNCTOR2:def 1 : (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 "F1")) "," (Set (Var "F2")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set "(" (Set (Var "F1")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F2")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))); theorem :: FUNCTOR2:2 (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")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "F")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))))) ; 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"::: ) ; let "F1", "F2" be ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; mode :::"transformation"::: "of" "F1" "," "F2" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "A") means :: FUNCTOR2:def 2 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F1" ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" "F2" ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ))); end; :: deftheorem defines :::"transformation"::: FUNCTOR2:def 2 : (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 "F1")) "," (Set (Var "F2")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) "is" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F1")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F2")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ))) ")" )))); 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"::: ) ; let "F" be ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); func :::"idt"::: "F" -> ($#m1_functor2 :::"transformation"::: ) "of" "F" "," "F" means :: FUNCTOR2:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" )))); end; :: deftheorem defines :::"idt"::: FUNCTOR2:def 3 : (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" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "b4")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_functor2 :::"idt"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" )))) ")" )))); 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"::: ) ; let "F1", "F2" be ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; let "t" be ($#m1_functor2 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); let "a" be ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")); func "t" :::"!"::: "a" -> ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" "F1" ($#k3_functor0 :::"."::: ) "a" ")" ) "," (Set "(" "F2" ($#k3_functor0 :::"."::: ) "a" ")" ) means :: FUNCTOR2:def 4 (Bool it ($#r1_hidden :::"="::: ) (Set "t" ($#k1_funct_1 :::"."::: ) "a")); end; :: deftheorem defines :::"!"::: FUNCTOR2:def 4 : (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 "F1")) "," (Set (Var "F2")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set "(" (Set (Var "F1")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F2")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")))) "iff" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" )))))); 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"::: ) ; let "F", "F1", "F2" be ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool "(" (Bool (Set (Const "F")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Const "F1"))) & (Bool (Set (Const "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Const "F2"))) ")" ) ; let "t1" be ($#m1_functor2 :::"transformation"::: ) "of" (Set (Const "F")) "," (Set (Const "F1")); let "t2" be ($#m1_functor2 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); func "t2" :::"`*`"::: "t1" -> ($#m1_functor2 :::"transformation"::: ) "of" "F" "," "F2" means :: FUNCTOR2:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set it ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "t2" ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" "t1" ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" )))); end; :: deftheorem defines :::"`*`"::: FUNCTOR2:def 5 : (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")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "b8")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t1")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b8")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t2")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "t1")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" )))) ")" )))))); theorem :: FUNCTOR2:3 (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 "F1")) "," (Set (Var "F2")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "t1")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "t1")) ($#r8_pboole :::"="::: ) (Set (Var "t2")))))) ; theorem :: FUNCTOR2:4 (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" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" ($#k1_functor2 :::"idt"::: ) (Set (Var "F")) ")" ) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "a")) ")" )))))) ; theorem :: FUNCTOR2:5 (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 "F1")) "," (Set (Var "F2")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k1_functor2 :::"idt"::: ) (Set (Var "F2")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t"))) ($#r8_pboole :::"="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "t")) ($#k3_functor2 :::"`*`"::: ) (Set "(" ($#k1_functor2 :::"idt"::: ) (Set (Var "F1")) ")" )) ($#r8_pboole :::"="::: ) (Set (Var "t"))) ")" )))) ; theorem :: FUNCTOR2:6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F3")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t3")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "holds" (Bool (Set (Set "(" (Set (Var "t3")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t2")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t1"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "t3")) ($#k3_functor2 :::"`*`"::: ) (Set "(" (Set (Var "t2")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t1")) ")" )))))))) ; begin 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"::: ) ; let "F1", "F2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); pred "F1" :::"is_naturally_transformable_to"::: "F2" means :: FUNCTOR2:def 6 (Bool "(" (Bool "F1" ($#r1_functor2 :::"is_transformable_to"::: ) "F2") & (Bool "ex" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" "F1" "," "F2" "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "b")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" "F1" ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "F2" ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" )))))) ")" ); reflexivity (Bool "for" (Set (Var "F1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F1")) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "b")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "F1")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F1")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" )))))) ")" )) ; end; :: deftheorem defines :::"is_naturally_transformable_to"::: FUNCTOR2:def 6 : (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 "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) "iff" (Bool "(" (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "b")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "F1")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F2")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" )))))) ")" ) ")" ))); theorem :: FUNCTOR2:7 (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")) "holds" (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F"))))) ; theorem :: FUNCTOR2:8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))))) ; 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"::: ) ; let "F1", "F2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Const "F2"))) ; mode :::"natural_transformation"::: "of" "F1" "," "F2" -> ($#m1_functor2 :::"transformation"::: ) "of" "F1" "," "F2" means :: FUNCTOR2:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" it ($#k2_functor2 :::"!"::: ) (Set (Var "b")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" "F1" ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "F2" ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" it ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ))))); end; :: deftheorem defines :::"natural_transformation"::: FUNCTOR2:def 7 : (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 "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Set "(" (Set (Var "b5")) ($#k2_functor2 :::"!"::: ) (Set (Var "b")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "F1")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F2")) ($#k6_functor0 :::"."::: ) (Set (Var "f")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "b5")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ))))) ")" )))); 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"::: ) ; let "F" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"idt"::: redefine func :::"idt"::: "F" -> ($#m2_functor2 :::"natural_transformation"::: ) "of" "F" "," "F"; end; definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "F", "F1", "F2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool "(" (Bool (Set (Const "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Const "F1"))) & (Bool (Set (Const "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Const "F2"))) ")" ) ; let "t1" be ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Const "F")) "," (Set (Const "F1")); let "t2" be ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); func "t2" :::"`*`"::: "t1" -> ($#m2_functor2 :::"natural_transformation"::: ) "of" "F" "," "F2" means :: FUNCTOR2:def 8 (Bool it ($#r8_pboole :::"="::: ) (Set "t2" ($#k3_functor2 :::"`*`"::: ) "t1")); end; :: deftheorem defines :::"`*`"::: FUNCTOR2:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "b8")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "t1")))) "iff" (Bool (Set (Var "b8")) ($#r8_pboole :::"="::: ) (Set (Set (Var "t2")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t1")))) ")" )))))); theorem :: FUNCTOR2:9 (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 "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_functor2 :::"idt"::: ) (Set (Var "F2")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t"))) ($#r8_pboole :::"="::: ) (Set (Var "t"))) & (Bool (Set (Set (Var "t")) ($#k3_functor2 :::"`*`"::: ) (Set "(" ($#k4_functor2 :::"idt"::: ) (Set (Var "F1")) ")" )) ($#r8_pboole :::"="::: ) (Set (Var "t"))) ")" )))) ; theorem :: FUNCTOR2:10 (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")) "," (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t2")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "t2")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t1")) ")" ) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t2")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "t1")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" )))))))) ; theorem :: FUNCTOR2:11 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F")) "," (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "F1")) (Bool "for" (Set (Var "t1")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F3")))) "holds" (Bool "for" (Set (Var "t3")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "holds" (Bool (Set (Set "(" (Set (Var "t3")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "t1")) ")" ) ($#k5_functor2 :::"`*`"::: ) (Set (Var "t"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "t3")) ($#k5_functor2 :::"`*`"::: ) (Set "(" (Set (Var "t1")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "t")) ")" )))))))) ; begin definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); func :::"Funcs"::: "(" "A" "," "B" ")" -> ($#m1_hidden :::"set"::: ) means :: FUNCTOR2:def 9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," "B") ")" )) if (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I") & (Bool (Set "B" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set "A" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"Funcs"::: FUNCTOR2:def 9 : (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_functor2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool (Set (Var "x")) "is" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" )) ")" ) ")" & "(" (Bool (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I"))) & (Bool (Set (Set (Var "B")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Bool "not" (Set (Set (Var "A")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_functor2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" )))); 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"::: ) ; func :::"Funct"::: "(" "A" "," "B" ")" -> ($#m1_hidden :::"set"::: ) means :: FUNCTOR2:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B") ")" )); end; :: deftheorem defines :::"Funct"::: FUNCTOR2:def 10 : (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 "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_functor2 :::"Funct"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Var "x")) "is" ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) ")" )) ")" ))); definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); func :::"Functors"::: "(" "A" "," "B" ")" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) means :: FUNCTOR2:def 11 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k7_functor2 :::"Funct"::: ) "(" "A" "," "B" ")" )) & (Bool "(" "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" it) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" )) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) "is" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "G"))) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B" "st" (Bool (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "H")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "G")) (Bool "for" (Set (Var "t2")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" it) ($#k1_multop_1 :::"."::: ) "(" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) ")" )) & (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "t2")) "," (Set (Var "t1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "t1")))) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"Functors"::: FUNCTOR2:def 11 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "b3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_functor2 :::"Functors"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k7_functor2 :::"Funct"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) & (Bool "(" "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u1_altcat_1 :::"Arrows"::: ) "of" (Set (Var "b3"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "F")) "," (Set (Var "G")) ")" )) "iff" (Bool "(" (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G"))) & (Bool (Set (Var "x")) "is" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "G"))) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) "being" ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G"))) & (Bool (Set (Var "G")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "H")))) "holds" (Bool "for" (Set (Var "t1")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F")) "," (Set (Var "G")) (Bool "for" (Set (Var "t2")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "G")) "," (Set (Var "H")) (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_altcat_1 :::"Comp"::: ) "of" (Set (Var "b3"))) ($#k1_multop_1 :::"."::: ) "(" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "H")) ")" )) & (Bool (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "t2")) "," (Set (Var "t1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "t1")))) ")" )))) ")" ) ")" ) ")" )));