:: FUNCTOR3 semantic presentation begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v6_altcat_1 :::"strict"::: ) ($#v11_altcat_1 :::"associative"::: ) ($#v12_altcat_1 :::"with_units"::: ) for ($#l2_altcat_1 :::"AltCatStr"::: ) ; end; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#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"::: ) ($#v9_functor0 :::"strict"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ($#v14_functor0 :::"comp-reversing"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "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 ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#v12_functor0 :::"id-preserving"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ($#v14_functor0 :::"comp-reversing"::: ) for ($#l2_functor0 :::"FunctorStr"::: ) "over" "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 ($#v8_functor0 :::"feasible"::: ) ($#v9_functor0 :::"strict"::: ) ($#v12_functor0 :::"id-preserving"::: ) ($#v15_functor0 :::"covariant"::: ) ($#v16_functor0 :::"contravariant"::: ) for ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "B"; end; theorem :: FUNCTOR3:1 (Bool "for" (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "," (Set (Var "o3")) "," (Set (Var "o4")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o2")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o2")) "," (Set (Var "o3")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o1")) "," (Set (Var "o4")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "o4")) "," (Set (Var "o3")) "st" (Bool (Bool (Set (Set (Var "b")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "d")) ($#k5_altcat_1 :::"*"::: ) (Set (Var "c")))) & (Bool (Set (Set (Var "a")) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_altcat_3 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o2")))) & (Bool (Set (Set "(" (Set (Var "d")) ($#k1_altcat_3 :::"""::: ) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k8_altcat_1 :::"idm"::: ) (Set (Var "o4")))) & (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 "o1")) ($#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 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o3")) "," (Set (Var "o4")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_altcat_1 :::"<^"::: ) (Set (Var "o4")) "," (Set (Var "o3")) ($#k1_altcat_1 :::"^>"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "c")) ($#k5_altcat_1 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k1_altcat_3 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "d")) ($#k1_altcat_3 :::"""::: ) ")" ) ($#k5_altcat_1 :::"*"::: ) (Set (Var "b")))))))))) ; theorem :: FUNCTOR3:2 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "o")) "," (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set "(" (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")) ")" ) "," (Set (Var "o")) "," (Set (Var "o1")) ")" ) ($#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 "o1")) ")" ) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k5_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o")) "," (Set (Var "o1")) ")" ")" )))))))) ; theorem :: FUNCTOR3:3 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "o")) "," (Set (Var "o1")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set "(" (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")) ")" ) "," (Set (Var "o")) "," (Set (Var "o1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_functor0 :::"Morph-Map"::: ) "(" (Set (Var "G")) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o1")) ")" ) "," (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" ) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k7_functor0 :::"Morph-Map"::: ) "(" (Set (Var "F")) "," (Set (Var "o")) "," (Set (Var "o1")) ")" ")" )))))))) ; theorem :: FUNCTOR3:4 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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")) "holds" (Bool (Set (Set "(" ($#k11_functor0 :::"id"::: ) (Set (Var "B")) ")" ) ($#k13_functor0 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F"))) "#)" ))))) ; theorem :: FUNCTOR3:5 (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 "for" (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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")) "holds" (Bool (Set (Set (Var "F")) ($#k13_functor0 :::"*"::: ) (Set "(" ($#k12_functor0 :::"id"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#g2_functor0 :::"FunctorStr"::: ) "(#" (Set "the" ($#u1_functor0 :::"ObjectMap"::: ) "of" (Set (Var "F"))) "," (Set "the" ($#u2_functor0 :::"MorphMap"::: ) "of" (Set (Var "F"))) "#)" ))))) ; theorem :: FUNCTOR3:6 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "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 "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (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 "(" (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")) ")" ) ($#k6_functor0 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "m")) ")" ))))))))) ; theorem :: FUNCTOR3:7 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "N")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (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 "(" (Set (Var "N")) ($#k13_functor0 :::"*"::: ) (Set (Var "M")) ")" ) ($#k6_functor0 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_functor0 :::"."::: ) (Set "(" (Set (Var "M")) ($#k8_functor0 :::"."::: ) (Set (Var "m")) ")" ))))))))) ; theorem :: FUNCTOR3:8 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "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 "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "N")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (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 "(" (Set (Var "N")) ($#k13_functor0 :::"*"::: ) (Set (Var "F")) ")" ) ($#k8_functor0 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "N")) ($#k8_functor0 :::"."::: ) (Set "(" (Set (Var "F")) ($#k6_functor0 :::"."::: ) (Set (Var "m")) ")" ))))))))) ; theorem :: FUNCTOR3:9 (Bool "for" (Set (Var "A")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_altcat_2 :::"reflexive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) (Bool "for" (Set (Var "G")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "M")) "being" ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "o1")) "," (Set (Var "o2")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) (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 "(" (Set (Var "G")) ($#k13_functor0 :::"*"::: ) (Set (Var "M")) ")" ) ($#k8_functor0 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "M")) ($#k8_functor0 :::"."::: ) (Set (Var "m")) ")" ))))))))) ; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "B")) "," (Set (Const "C")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v13_functor0 :::"comp-preserving"::: ) ; end; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#v14_functor0 :::"comp-reversing"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#v14_functor0 :::"comp-reversing"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "B")) "," (Set (Const "C")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v13_functor0 :::"comp-preserving"::: ) ; end; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#v14_functor0 :::"comp-reversing"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "B")) "," (Set (Const "C")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v14_functor0 :::"comp-reversing"::: ) ; end; registrationlet "A" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "B" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v8_functor0 :::"feasible"::: ) ($#v11_functor0 :::"Contravariant"::: ) ($#v14_functor0 :::"comp-reversing"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#v8_functor0 :::"feasible"::: ) ($#v10_functor0 :::"Covariant"::: ) ($#v13_functor0 :::"comp-preserving"::: ) ($#l2_functor0 :::"FunctorStr"::: ) "over" (Set (Const "B")) "," (Set (Const "C")); cluster (Set "G" ($#k13_functor0 :::"*"::: ) "F") -> ($#v14_functor0 :::"comp-reversing"::: ) ; end; 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 "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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")); let "G" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); :: original: :::"*"::: redefine func "G" :::"*"::: "F" -> ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "C"; end; 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 "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); :: original: :::"*"::: redefine func "G" :::"*"::: "F" -> ($#v9_functor0 :::"strict"::: ) ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "C"; end; 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 "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#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")); let "G" be ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); :: original: :::"*"::: redefine func "G" :::"*"::: "F" -> ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "C"; end; 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 "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "F" be ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "G" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); :: original: :::"*"::: redefine func "G" :::"*"::: "F" -> ($#v9_functor0 :::"strict"::: ) ($#v16_functor0 :::"contravariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" "A" "," "C"; end; theorem :: FUNCTOR3:10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2"))))))) ; begin definitionlet "A", "B", "C" 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")); let "t" be ($#m1_functor2 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); let "G" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); assume (Bool (Set (Const "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; func "G" :::"*"::: "t" -> ($#m1_functor2 :::"transformation"::: ) "of" (Set "G" ($#k1_functor3 :::"*"::: ) "F1") "," (Set "G" ($#k1_functor3 :::"*"::: ) "F2") means :: FUNCTOR3:def 1 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set "G" ($#k6_functor0 :::"."::: ) (Set "(" "t" ($#k2_functor2 :::"!"::: ) (Set (Var "o")) ")" )))); end; :: deftheorem defines :::"*"::: FUNCTOR3:def 1 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) (Bool "for" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "G")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "b8")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Set (Var "G")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2"))) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_functor3 :::"*"::: ) (Set (Var "t")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b8")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "o")) ")" )))) ")" )))))); theorem :: FUNCTOR3:11 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "," (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 "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "p")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set "(" (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "p")) ")" ) ($#k2_functor2 :::"!"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G1")) ($#k6_functor0 :::"."::: ) (Set "(" (Set (Var "p")) ($#k2_functor2 :::"!"::: ) (Set (Var "o")) ")" )))))))) ; definitionlet "A", "B", "C" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_altcat_1 :::"transitive"::: ) ($#v12_altcat_1 :::"with_units"::: ) ($#l2_altcat_1 :::"AltCatStr"::: ) ; let "G1", "G2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); let "F" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "s" be ($#m1_functor2 :::"transformation"::: ) "of" (Set (Const "G1")) "," (Set (Const "G2")); assume (Bool (Set (Const "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Const "G2"))) ; func "s" :::"*"::: "F" -> ($#m1_functor2 :::"transformation"::: ) "of" (Set "G1" ($#k1_functor3 :::"*"::: ) "F") "," (Set "G2" ($#k1_functor3 :::"*"::: ) "F") means :: FUNCTOR3:def 2 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set "s" ($#k2_functor2 :::"!"::: ) (Set "(" "F" ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" )))); end; :: deftheorem defines :::"*"::: FUNCTOR3:def 2 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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 "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "F")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "s")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "b8")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F"))) "," (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F"))) "holds" (Bool "(" (Bool (Set (Var "b8")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k6_functor3 :::"*"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b8")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_functor2 :::"!"::: ) (Set "(" (Set (Var "F")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" )))) ")" )))))); theorem :: FUNCTOR3:12 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (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 "for" (Set (Var "F1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "q")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set "(" (Set (Var "q")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1")) ")" ) ($#k2_functor2 :::"!"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k2_functor2 :::"!"::: ) (Set "(" (Set (Var "F1")) ($#k3_functor0 :::"."::: ) (Set (Var "o")) ")" )))))))) ; theorem :: FUNCTOR3:13 (Bool "for" (Set (Var "C")) "," (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")) "," (Set (Var "F3")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "p")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "p1")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "st" (Bool (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 (Set (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "p")) ")" )) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set "(" (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: FUNCTOR3:14 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "q")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "q1")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2"))) & (Bool (Set (Var "G2")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G3")))) "holds" (Bool (Set (Set "(" (Set (Var "q1")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "q")) ")" ) ($#k6_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "q1")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set "(" (Set (Var "q")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1")) ")" )))))))) ; theorem :: FUNCTOR3:15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "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")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "r")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "H1")) "," (Set (Var "H2")) "st" (Bool (Bool (Set (Var "H1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k6_functor3 :::"*"::: ) (Set (Var "G1")) ")" ) ($#k6_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "r")) ($#k6_functor3 :::"*"::: ) (Set "(" (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1")) ")" )))))))) ; theorem :: FUNCTOR3:16 (Bool "for" (Set (Var "A")) "," (Set (Var "D")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "q")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k5_functor3 :::"*"::: ) (Set (Var "q")) ")" ) ($#k6_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "H1")) ($#k5_functor3 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1")) ")" )))))))) ; theorem :: FUNCTOR3:17 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (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")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set "(" (Set (Var "H1")) ($#k1_functor3 :::"*"::: ) (Set (Var "G1")) ")" ) ($#k5_functor3 :::"*"::: ) (Set (Var "p"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "H1")) ($#k5_functor3 :::"*"::: ) (Set "(" (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "p")) ")" )))))))) ; theorem :: FUNCTOR3:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k4_functor2 :::"idt"::: ) (Set (Var "G1")) ")" ) ($#k6_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r8_pboole :::"="::: ) (Set ($#k4_functor2 :::"idt"::: ) (Set "(" (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1")) ")" )))))) ; theorem :: FUNCTOR3:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set "(" ($#k4_functor2 :::"idt"::: ) (Set (Var "F1")) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k4_functor2 :::"idt"::: ) (Set "(" (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1")) ")" )))))) ; theorem :: FUNCTOR3:20 (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")) (Bool "for" (Set (Var "p")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set "(" ($#k12_functor0 :::"id"::: ) (Set (Var "B")) ")" ) ($#k5_functor3 :::"*"::: ) (Set (Var "p"))) ($#r8_pboole :::"="::: ) (Set (Var "p")))))) ; theorem :: FUNCTOR3:21 (Bool "for" (Set (Var "C")) "," (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 "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "q")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "q")) ($#k6_functor3 :::"*"::: ) (Set "(" ($#k12_functor0 :::"id"::: ) (Set (Var "B")) ")" )) ($#r8_pboole :::"="::: ) (Set (Var "q")))))) ; begin definitionlet "A", "B", "C" 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")); let "G1", "G2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); let "t" be ($#m1_functor2 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); let "s" be ($#m1_functor2 :::"transformation"::: ) "of" (Set (Const "G1")) "," (Set (Const "G2")); func "s" :::"(#)"::: "t" -> ($#m1_functor2 :::"transformation"::: ) "of" (Set "G1" ($#k1_functor3 :::"*"::: ) "F1") "," (Set "G2" ($#k1_functor3 :::"*"::: ) "F2") equals :: FUNCTOR3:def 3 (Set (Set "(" "s" ($#k6_functor3 :::"*"::: ) "F2" ")" ) ($#k3_functor2 :::"`*`"::: ) (Set "(" "G1" ($#k5_functor3 :::"*"::: ) "t" ")" )); end; :: deftheorem defines :::"(#)"::: FUNCTOR3:def 3 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "s")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set (Var "s")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k6_functor3 :::"*"::: ) (Set (Var "F2")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set "(" (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "t")) ")" )))))))); theorem :: FUNCTOR3:22 (Bool "for" (Set (Var "C")) "," (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")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "p")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "q")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "q")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "p"))) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "G2")) ($#k5_functor3 :::"*"::: ) (Set (Var "p")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set "(" (Set (Var "q")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1")) ")" )))))))) ; theorem :: FUNCTOR3:23 (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")) (Bool "for" (Set (Var "p")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set "(" ($#k4_functor2 :::"idt"::: ) (Set "(" ($#k12_functor0 :::"id"::: ) (Set (Var "B")) ")" ) ")" ) ($#k7_functor3 :::"(#)"::: ) (Set (Var "p"))) ($#r8_pboole :::"="::: ) (Set (Var "p")))))) ; theorem :: FUNCTOR3:24 (Bool "for" (Set (Var "C")) "," (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 "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "q")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "q")) ($#k7_functor3 :::"(#)"::: ) (Set "(" ($#k4_functor2 :::"idt"::: ) (Set "(" ($#k12_functor0 :::"id"::: ) (Set (Var "B")) ")" ) ")" )) ($#r8_pboole :::"="::: ) (Set (Var "q")))))) ; theorem :: FUNCTOR3:25 (Bool "for" (Set (Var "C")) "," (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")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "p")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "p"))) ($#r8_pboole :::"="::: ) (Set (Set "(" ($#k4_functor2 :::"idt"::: ) (Set (Var "G1")) ")" ) ($#k7_functor3 :::"(#)"::: ) (Set (Var "p")))))))) ; theorem :: FUNCTOR3:26 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "q")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "q")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "q")) ($#k7_functor3 :::"(#)"::: ) (Set "(" ($#k4_functor2 :::"idt"::: ) (Set (Var "F1")) ")" ))))))) ; theorem :: FUNCTOR3:27 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "s")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "u")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "H1")) "," (Set (Var "H2")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "G2"))) & (Bool (Set (Var "H1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "s")) ")" ) ($#k7_functor3 :::"(#)"::: ) (Set (Var "t"))) ($#r8_pboole :::"="::: ) (Set (Set (Var "u")) ($#k7_functor3 :::"(#)"::: ) (Set "(" (Set (Var "s")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "t")) ")" )))))))))) ; theorem :: FUNCTOR3:28 (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "t"))) "is" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2")))))))) ; theorem :: FUNCTOR3:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "s")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1"))) "is" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1")))))))) ; theorem :: FUNCTOR3:30 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "s")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "(" (Bool (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2")))) & (Bool (Set (Set (Var "s")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "t"))) "is" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2")))) ")" )))))) ; theorem :: FUNCTOR3:31 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (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 "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "s1")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) (Bool "for" (Set (Var "t")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t1")) "being" ($#m1_functor2 :::"transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "st" (Bool (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"))) & (Bool (Set (Var "G1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G2"))) & (Bool (Set (Var "G2")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "G3")))) "holds" (Bool (Set (Set "(" (Set (Var "s1")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "s")) ")" ) ($#k7_functor3 :::"(#)"::: ) (Set "(" (Set (Var "t1")) ($#k3_functor2 :::"`*`"::: ) (Set (Var "t")) ")" )) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "s1")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "t1")) ")" ) ($#k3_functor2 :::"`*`"::: ) (Set "(" (Set (Var "s")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "t")) ")" )))))))))) ; begin theorem :: FUNCTOR3:32 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "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 "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) ) ")" )) "holds" (Bool "(" (Bool (Set (Var "F2")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool "ex" (Set (Var "f")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F1")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ) ($#k1_altcat_3 :::"""::: ) )) & (Bool (Set (Set (Var "f")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) ) ")" ))) ")" )))) ; definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "F1", "F2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); pred "F1" "," "F2" :::"are_naturally_equivalent"::: means :: FUNCTOR3:def 4 (Bool "(" (Bool "F1" ($#r2_functor2 :::"is_naturally_transformable_to"::: ) "F2") & (Bool "F2" ($#r1_functor2 :::"is_transformable_to"::: ) "F1") & (Bool "ex" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" "F1" "," "F2" "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) ))) ")" ); 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")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool "ex" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F1")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")) "holds" (Bool (Set (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) ))) ")" )) ; symmetry (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool "ex" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")) "holds" (Bool (Set (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "F2")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F1"))) & (Bool (Set (Var "F1")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool "ex" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F1")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Const "A")) "holds" (Bool (Set (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) ))) ")" )) ; end; :: deftheorem defines :::"are_naturally_equivalent"::: FUNCTOR3:def 4 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (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")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F1")) ($#r2_functor2 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r1_functor2 :::"is_transformable_to"::: ) (Set (Var "F1"))) & (Bool "ex" (Set (Var "t")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "t")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) ))) ")" ) ")" ))); definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "F1", "F2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) "," (Set (Const "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) ; mode :::"natural_equivalence"::: "of" "F1" "," "F2" -> ($#m2_functor2 :::"natural_transformation"::: ) "of" "F1" "," "F2" means :: FUNCTOR3:def 5 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" "A" "holds" (Bool (Set it ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) )); end; :: deftheorem defines :::"natural_equivalence"::: FUNCTOR3:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (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")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m2_functor2 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "holds" (Bool "(" (Bool (Set (Var "b5")) "is" ($#m1_functor3 :::"natural_equivalence"::: ) "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")) ($#k2_functor2 :::"!"::: ) (Set (Var "a"))) "is" ($#v3_altcat_3 :::"iso"::: ) )) ")" )))); theorem :: FUNCTOR3:33 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) & (Bool (Set (Var "F2")) "," (Set (Var "F3")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool (Set (Var "F1")) "," (Set (Var "F3")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ))) ; theorem :: FUNCTOR3:34 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (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 "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "e1")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) & (Bool (Set (Var "F2")) "," (Set (Var "F3")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool (Set (Set (Var "e1")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "e"))) "is" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F3"))))))) ; theorem :: FUNCTOR3:35 (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2"))) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) & (Bool (Set (Set (Var "G1")) ($#k5_functor3 :::"*"::: ) (Set (Var "e"))) "is" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2")))) ")" ))))) ; theorem :: FUNCTOR3:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) "," (Set (Var "G2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) & (Bool (Set (Set (Var "f")) ($#k6_functor3 :::"*"::: ) (Set (Var "F1"))) "is" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1")))) ")" ))))) ; theorem :: FUNCTOR3:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "f")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) & (Bool (Set (Var "G1")) "," (Set (Var "G2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2"))) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) & (Bool (Set (Set (Var "f")) ($#k7_functor3 :::"(#)"::: ) (Set (Var "e"))) "is" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Set (Var "G1")) ($#k1_functor3 :::"*"::: ) (Set (Var "F1"))) "," (Set (Set (Var "G2")) ($#k1_functor3 :::"*"::: ) (Set (Var "F2")))) ")" )))))) ; definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "F1", "F2" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "e" be ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); assume (Bool (Set (Const "F1")) "," (Set (Const "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) ; func "e" :::"""::: -> ($#m1_functor3 :::"natural_equivalence"::: ) "of" "F2" "," "F1" means :: FUNCTOR3:def 6 (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 (Set "(" "e" ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ) ($#k1_altcat_3 :::"""::: ) ))); end; :: deftheorem defines :::"""::: FUNCTOR3:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F2")) "," (Set (Var "F1")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "e")) ($#k8_functor3 :::"""::: ) )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "e")) ($#k2_functor2 :::"!"::: ) (Set (Var "a")) ")" ) ($#k1_altcat_3 :::"""::: ) ))) ")" ))))); theorem :: FUNCTOR3:38 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"object":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "e")) ($#k8_functor3 :::"""::: ) ")" ) ($#k2_functor2 :::"!"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "e")) ($#k2_functor2 :::"!"::: ) (Set (Var "o")) ")" ) ($#k1_altcat_3 :::"""::: ) )))))) ; theorem :: FUNCTOR3:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool (Set (Set (Var "e")) ($#k5_functor2 :::"`*`"::: ) (Set "(" (Set (Var "e")) ($#k8_functor3 :::"""::: ) ")" )) ($#r8_pboole :::"="::: ) (Set ($#k4_functor2 :::"idt"::: ) (Set (Var "F2"))))))) ; theorem :: FUNCTOR3:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "e")) ($#k8_functor3 :::"""::: ) ")" ) ($#k5_functor2 :::"`*`"::: ) (Set (Var "e"))) ($#r8_pboole :::"="::: ) (Set ($#k4_functor2 :::"idt"::: ) (Set (Var "F1"))))))) ; definitionlet "A", "B" be ($#l2_altcat_1 :::"category":::); let "F" be ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"idt"::: redefine func :::"idt"::: "F" -> ($#m1_functor3 :::"natural_equivalence"::: ) "of" "F" "," "F"; end; theorem :: FUNCTOR3:41 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "e")) ($#k8_functor3 :::"""::: ) ")" ) ($#k8_functor3 :::"""::: ) ) ($#r8_pboole :::"="::: ) (Set (Var "e")))))) ; theorem :: FUNCTOR3:42 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F3")) "," (Set (Var "F2")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "e")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "e1")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) (Bool "for" (Set (Var "k")) "being" ($#m1_functor3 :::"natural_equivalence"::: ) "of" (Set (Var "F1")) "," (Set (Var "F3")) "st" (Bool (Bool (Set (Var "k")) ($#r8_pboole :::"="::: ) (Set (Set (Var "e1")) ($#k5_functor2 :::"`*`"::: ) (Set (Var "e")))) & (Bool (Set (Var "F1")) "," (Set (Var "F2")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) ) & (Bool (Set (Var "F2")) "," (Set (Var "F3")) ($#r1_functor3 :::"are_naturally_equivalent"::: ) )) "holds" (Bool (Set (Set (Var "k")) ($#k8_functor3 :::"""::: ) ) ($#r8_pboole :::"="::: ) (Set (Set "(" (Set (Var "e")) ($#k8_functor3 :::"""::: ) ")" ) ($#k5_functor2 :::"`*`"::: ) (Set "(" (Set (Var "e1")) ($#k8_functor3 :::"""::: ) ")" )))))))) ; theorem :: FUNCTOR3:43 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l2_altcat_1 :::"category":::) (Bool "for" (Set (Var "F1")) "being" ($#v15_functor0 :::"covariant"::: ) ($#m2_functor0 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k9_functor3 :::"idt"::: ) (Set (Var "F1")) ")" ) ($#k8_functor3 :::"""::: ) ) ($#r8_pboole :::"="::: ) (Set ($#k9_functor3 :::"idt"::: ) (Set (Var "F1")))))) ;