:: ISOCAT_1 semantic presentation begin theorem :: ISOCAT_1:1 canceled; theorem :: ISOCAT_1:2 canceled; theorem :: ISOCAT_1:3 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_cat_1 :::"Morphism"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v9_cat_1 :::"invertible"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_cat_3 :::"/."::: ) (Set (Var "f"))) "is" ($#v9_cat_1 :::"invertible"::: ) ))))) ; theorem :: ISOCAT_1:4 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "F1")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F2")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ")" )))))) ; theorem :: ISOCAT_1:5 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F1"))) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Set (Var "G2")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F2"))))))) ; theorem :: ISOCAT_1:6 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "t")) "is" ($#v1_nattra_1 :::"invertible"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "F1")) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) "," (Set (Set (Var "F2")) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) ($#r1_cat_1 :::"are_isomorphic"::: ) ))))) ; definitionlet "C", "D" be ($#l1_cat_1 :::"Category":::); redefine mode :::"Functor"::: "of" "C" "," "D" means :: ISOCAT_1:def 1 (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" "D" "st" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "holds" (Bool "(" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" "C" "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" it ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Functor"::: ISOCAT_1:def 1 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b3")) "being" bbbadM1_SUBSET_1((Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b1"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "b2"))) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "D")) "st" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "d"))))) ")" ) & (Bool "(" "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k3_graph_1 :::"dom"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set "(" ($#k4_graph_1 :::"cod"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ) ")" ))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "C")) "st" (Bool (Bool (Set ($#k3_graph_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_graph_1 :::"cod"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "g")) ($#k1_cat_1 :::"(*)"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "g")) ")" ) ($#k1_cat_1 :::"(*)"::: ) (Set "(" (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "f")) ")" ))) ")" ) ")" ) ")" ))); theorem :: ISOCAT_1:7 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "B")) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Morphism":::) "of" (Set (Var "A")) "st" (Bool (Set (Set (Var "F")) ($#k3_funct_2 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))))))) ; theorem :: ISOCAT_1:8 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "st" (Bool (Set (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))))))) ; theorem :: ISOCAT_1:9 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) ) ; func "F" :::"""::: -> ($#m2_cat_1 :::"Functor"::: ) "of" "B" "," "A" equals :: ISOCAT_1:def 2 (Set "F" ($#k2_funct_1 :::"""::: ) ); end; :: deftheorem defines :::"""::: ISOCAT_1:def 2 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_isocat_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_funct_1 :::"""::: ) )))); definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); redefine attr "F" is :::"isomorphic"::: means :: ISOCAT_1:def 3 (Bool "(" (Bool "F" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) "F") ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "B")) ")" ); end; :: deftheorem defines :::"isomorphic"::: ISOCAT_1:def 3 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) ) "iff" (Bool "(" (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "B")))) ")" ) ")" ))); theorem :: ISOCAT_1:10 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_isocat_1 :::"""::: ) ) "is" ($#v12_cat_1 :::"isomorphic"::: ) ))) ; theorem :: ISOCAT_1:11 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool (Set (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_cat_1 :::"Obj"::: ) (Set "(" (Set (Var "F")) ($#k1_isocat_1 :::"""::: ) ")" ))))) ; theorem :: ISOCAT_1:12 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_isocat_1 :::"""::: ) ")" ) ($#k1_isocat_1 :::"""::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Var "F"))))) ; theorem :: ISOCAT_1:13 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_isocat_1 :::"""::: ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "B")))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k1_isocat_1 :::"""::: ) ")" ) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) ")" ))) ; theorem :: ISOCAT_1:14 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) ) & (Bool (Set (Var "G")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) "holds" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) "is" ($#v12_cat_1 :::"isomorphic"::: ) )))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); pred "A" "," "B" :::"are_isomorphic"::: means :: ISOCAT_1:def 4 (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B" "st" (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )); reflexivity (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "A")) "st" (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) ))) ; symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) ))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) ))) ; end; :: deftheorem defines :::"are_isomorphic"::: ISOCAT_1:def 4 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_isocat_1 :::"are_isomorphic"::: ) ) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Set (Var "F")) "is" ($#v12_cat_1 :::"isomorphic"::: ) )) ")" )); notationlet "A", "B" be ($#l1_cat_1 :::"Category":::); synonym "A" :::"~="::: "B" for "A" "," "B" :::"are_isomorphic"::: ; end; theorem :: ISOCAT_1:15 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_isocat_1 :::"~="::: ) (Set (Var "B"))) & (Bool (Set (Var "B")) ($#r1_isocat_1 :::"~="::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "A")) ($#r1_isocat_1 :::"~="::: ) (Set (Var "C")))) ; theorem :: ISOCAT_1:16 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "o")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_cat_2 :::"[:"::: ) (Set "(" ($#k3_cat_1 :::"1Cat"::: ) "(" (Set (Var "o")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "A")) ($#k8_cat_2 :::":]"::: ) ) ($#r1_isocat_1 :::"~="::: ) (Set (Var "A"))))) ; theorem :: ISOCAT_1:17 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) ($#r1_isocat_1 :::"~="::: ) (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "A")) ($#k8_cat_2 :::":]"::: ) ))) ; theorem :: ISOCAT_1:18 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k8_cat_2 :::"[:"::: ) (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k8_cat_2 :::":]"::: ) ) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) ($#r1_isocat_1 :::"~="::: ) (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) ($#k8_cat_2 :::":]"::: ) ))) ; theorem :: ISOCAT_1:19 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_isocat_1 :::"~="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_isocat_1 :::"~="::: ) (Set (Var "D")))) "holds" (Bool (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "C")) ($#k8_cat_2 :::":]"::: ) ) ($#r1_isocat_1 :::"~="::: ) (Set ($#k8_cat_2 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "D")) ($#k8_cat_2 :::":]"::: ) ))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "F2"))) ; let "t" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); let "G" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); func "G" :::"*"::: "t" -> ($#m1_nattra_1 :::"transformation"::: ) "of" (Set "G" ($#k9_cat_1 :::"*"::: ) "F1") "," (Set "G" ($#k9_cat_1 :::"*"::: ) "F2") equals :: ISOCAT_1:def 5 (Set "G" ($#k1_partfun1 :::"*"::: ) "t"); end; :: deftheorem defines :::"*"::: ISOCAT_1:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G")) ($#k2_isocat_1 :::"*"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_partfun1 :::"*"::: ) (Set (Var "t")))))))); definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "G1", "G2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); assume (Bool (Set (Const "G1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Const "G2"))) ; let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "t" be ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Const "G1")) "," (Set (Const "G2")); func "t" :::"*"::: "F" -> ($#m1_nattra_1 :::"transformation"::: ) "of" (Set "G1" ($#k9_cat_1 :::"*"::: ) "F") "," (Set "G2" ($#k9_cat_1 :::"*"::: ) "F") equals :: ISOCAT_1:def 6 (Set "t" ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_cat_1 :::"Obj"::: ) "F" ")" )); end; :: deftheorem defines :::"*"::: ISOCAT_1:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set (Var "t")) ($#k3_isocat_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k7_cat_1 :::"Obj"::: ) (Set (Var "F")) ")" ))))))); theorem :: ISOCAT_1:20 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "G1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k3_isocat_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" )))))))) ; theorem :: ISOCAT_1:21 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r1_nattra_1 :::"is_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_nattra_1 :::"transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k2_isocat_1 :::"*"::: ) (Set (Var "t")) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k9_cat_3 :::"/."::: ) (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))))))) ; theorem :: ISOCAT_1:22 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "G1")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F1"))) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Set (Var "G2")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F2"))))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); assume (Bool (Set (Const "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "F2"))) ; let "t" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); let "G" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); func "G" :::"*"::: "t" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set "G" ($#k9_cat_1 :::"*"::: ) "F1") "," (Set "G" ($#k9_cat_1 :::"*"::: ) "F2") equals :: ISOCAT_1:def 7 (Set "G" ($#k2_isocat_1 :::"*"::: ) "t"); end; :: deftheorem defines :::"*"::: ISOCAT_1:def 7 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k2_isocat_1 :::"*"::: ) (Set (Var "t")))))))); theorem :: ISOCAT_1:23 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "t")) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k9_cat_3 :::"/."::: ) (Set "(" (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")) ")" )))))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "G1", "G2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); assume (Bool (Set (Const "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Const "G2"))) ; let "F" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "t" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "G1")) "," (Set (Const "G2")); func "t" :::"*"::: "F" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set "G1" ($#k9_cat_1 :::"*"::: ) "F") "," (Set "G2" ($#k9_cat_1 :::"*"::: ) "F") equals :: ISOCAT_1:def 8 (Set "t" ($#k3_isocat_1 :::"*"::: ) "F"); end; :: deftheorem defines :::"*"::: ISOCAT_1:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k3_isocat_1 :::"*"::: ) (Set (Var "F")))))))); theorem :: ISOCAT_1:24 (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k4_nattra_1 :::"."::: ) (Set "(" (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" )))))))) ; theorem :: ISOCAT_1:25 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set ($#k2_cat_1 :::"Hom"::: ) "(" (Set "(" (Set (Var "F1")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "F2")) ($#k8_cat_1 :::"."::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: ISOCAT_1:26 (Bool "for" (Set (Var "B")) "," (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "t1")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t2")) ($#k4_nattra_1 :::"."::: ) (Set (Var "a")))) ")" )) "holds" (Bool (Set (Var "t1")) ($#r2_funct_2 :::"="::: ) (Set (Var "t2")))))) ; theorem :: ISOCAT_1:27 (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "s9")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F3")))) "holds" (Bool (Set (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set "(" (Set (Var "s9")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "s")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s9")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s")) ")" )))))))) ; theorem :: ISOCAT_1:28 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "t9")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2"))) & (Bool (Set (Var "G2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G3")))) "holds" (Bool (Set (Set "(" (Set (Var "t9")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t")) ")" ) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "t9")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: ISOCAT_1:29 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "H1")) "," (Set (Var "H2")) "st" (Bool (Bool (Set (Var "H1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "G")) ")" ) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "u")) ($#k5_isocat_1 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: ISOCAT_1:30 (Bool "for" (Set (Var "A")) "," (Set (Var "D")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "t")) ")" ) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "H")) ($#k4_isocat_1 :::"*"::: ) (Set "(" (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F")) ")" )))))))) ; theorem :: ISOCAT_1:31 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set "(" (Set (Var "H")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G")) ")" ) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "H")) ($#k4_isocat_1 :::"*"::: ) (Set "(" (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s")) ")" )))))))) ; theorem :: ISOCAT_1:32 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "G")) ")" ) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set ($#k6_nattra_1 :::"id"::: ) (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")) ")" )))))) ; theorem :: ISOCAT_1:33 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "F")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k6_nattra_1 :::"id"::: ) (Set "(" (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")) ")" )))))) ; theorem :: ISOCAT_1:34 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "B")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "t")))))) ; theorem :: ISOCAT_1:35 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "B")) ")" ) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set (Var "s")))))) ; definitionlet "A", "B", "C" be ($#l1_cat_1 :::"Category":::); let "F1", "F2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); let "G1", "G2" be ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Const "B")) "," (Set (Const "C")); let "s" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "F1")) "," (Set (Const "F2")); let "t" be ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Const "G1")) "," (Set (Const "G2")); func "t" :::"(#)"::: "s" -> ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set "G1" ($#k9_cat_1 :::"*"::: ) "F1") "," (Set "G2" ($#k9_cat_1 :::"*"::: ) "F2") equals :: ISOCAT_1:def 9 (Set (Set "(" "t" ($#k5_isocat_1 :::"*"::: ) "F2" ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" "G1" ($#k4_isocat_1 :::"*"::: ) "s" ")" )); end; :: deftheorem defines :::"(#)"::: ISOCAT_1:def 9 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "holds" (Bool (Set (Set (Var "t")) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F2")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" (Set (Var "G1")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s")) ")" )))))))); theorem :: ISOCAT_1:36 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "t")) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "G2")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F1")) ")" )))))))) ; theorem :: ISOCAT_1:37 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "B")) ")" ) ")" ) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set (Var "s")))))) ; theorem :: ISOCAT_1:38 (Bool "for" (Set (Var "C")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "t")) ($#k6_isocat_1 :::"(#)"::: ) (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set "(" ($#k10_cat_1 :::"id"::: ) (Set (Var "B")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "t")))))) ; theorem :: ISOCAT_1:39 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "u")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "H1")) "," (Set (Var "H2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2"))) & (Bool (Set (Var "H1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "H2")))) "holds" (Bool (Set (Set (Var "u")) ($#k6_isocat_1 :::"(#)"::: ) (Set "(" (Set (Var "t")) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "u")) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "t")) ")" ) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s"))))))))))) ; theorem :: ISOCAT_1:40 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) "st" (Bool (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2")))) "holds" (Bool (Set (Set (Var "t")) ($#k5_isocat_1 :::"*"::: ) (Set (Var "F"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "t")) ($#k6_isocat_1 :::"(#)"::: ) (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "F")) ")" ))))))) ; theorem :: ISOCAT_1:41 (Bool "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2")))) "holds" (Bool (Set (Set (Var "G")) ($#k4_isocat_1 :::"*"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_nattra_1 :::"id"::: ) (Set (Var "G")) ")" ) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s")))))))) ; theorem :: ISOCAT_1:42 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "," (Set (Var "F3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F1")) "," (Set (Var "F2")) (Bool "for" (Set (Var "s9")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "F2")) "," (Set (Var "F3")) (Bool "for" (Set (Var "t")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G1")) "," (Set (Var "G2")) (Bool "for" (Set (Var "t9")) "being" ($#m2_nattra_1 :::"natural_transformation"::: ) "of" (Set (Var "G2")) "," (Set (Var "G3")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F2"))) & (Bool (Set (Var "F2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "F3"))) & (Bool (Set (Var "G1")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G2"))) & (Bool (Set (Var "G2")) ($#r2_nattra_1 :::"is_naturally_transformable_to"::: ) (Set (Var "G3")))) "holds" (Bool (Set (Set "(" (Set (Var "t9")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "t")) ")" ) ($#k6_isocat_1 :::"(#)"::: ) (Set "(" (Set (Var "s9")) ($#k7_nattra_1 :::"`*`"::: ) (Set (Var "s")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "t9")) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s9")) ")" ) ($#k7_nattra_1 :::"`*`"::: ) (Set "(" (Set (Var "t")) ($#k6_isocat_1 :::"(#)"::: ) (Set (Var "s")) ")" )))))))))) ; theorem :: ISOCAT_1:43 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "I")) ($#r3_nattra_1 :::"~="::: ) (Set (Var "J")))) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "I"))) ($#r3_nattra_1 :::"~="::: ) (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "J")))) & (Bool (Set (Set (Var "I")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set (Set (Var "J")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F")))) ")" ))))) ; theorem :: ISOCAT_1:44 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) (Bool "for" (Set (Var "I")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "I")) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set (Var "I"))) ($#r3_nattra_1 :::"~="::: ) (Set (Var "F"))) & (Bool (Set (Set (Var "I")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set (Var "G"))) ")" ))))) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); pred "A" :::"is_equivalent_with"::: "B" means :: ISOCAT_1:def 10 (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B"(Bool "ex" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "B" "," "A" "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) "A")) & (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) "B")) ")" ))); reflexivity (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) (Bool "ex" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) ")" ))) ; symmetry (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))(Bool "ex" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "B")))) ")" )))) "holds" (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A"))(Bool "ex" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "B")))) & (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) ")" )))) ; end; :: deftheorem defines :::"is_equivalent_with"::: ISOCAT_1:def 10 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_isocat_1 :::"is_equivalent_with"::: ) (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))(Bool "ex" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "B")))) ")" ))) ")" )); notationlet "A", "B" be ($#l1_cat_1 :::"Category":::); synonym "A" "," "B" :::"are_equivalent"::: for "A" :::"is_equivalent_with"::: "B"; end; theorem :: ISOCAT_1:45 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_isocat_1 :::"~="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) ($#r2_isocat_1 :::"is_equivalent_with"::: ) (Set (Var "B")))) ; theorem :: ISOCAT_1:46 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_isocat_1 :::"are_equivalent"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "C")) ($#r2_isocat_1 :::"are_equivalent"::: ) )) "holds" (Bool (Set (Var "A")) "," (Set (Var "C")) ($#r2_isocat_1 :::"are_equivalent"::: ) )) ; definitionlet "A", "B" be ($#l1_cat_1 :::"Category":::); assume (Bool (Set (Const "A")) "," (Set (Const "B")) ($#r2_isocat_1 :::"are_equivalent"::: ) ) ; mode :::"Equivalence"::: "of" "A" "," "B" -> ($#m2_cat_1 :::"Functor"::: ) "of" "A" "," "B" means :: ISOCAT_1:def 11 (Bool "ex" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" "B" "," "A" "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) it) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) "A")) & (Bool (Set it ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) "B")) ")" )); end; :: deftheorem defines :::"Equivalence"::: ISOCAT_1:def 11 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_isocat_1 :::"are_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "ex" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "b3"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "b3")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "B")))) ")" )) ")" ))); theorem :: ISOCAT_1:47 (Bool "for" (Set (Var "A")) "being" ($#l1_cat_1 :::"Category":::) "holds" (Bool (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A"))) "is" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "A")) "," (Set (Var "A")))) ; theorem :: ISOCAT_1:48 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_isocat_1 :::"are_equivalent"::: ) ) & (Bool (Set (Var "B")) "," (Set (Var "C")) ($#r2_isocat_1 :::"are_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "B")) "," (Set (Var "C")) "holds" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) "is" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "A")) "," (Set (Var "C")))))) ; theorem :: ISOCAT_1:49 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_isocat_1 :::"are_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "ex" (Set (Var "G")) "being" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool "(" (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A")))) & (Bool (Set (Set (Var "F")) ($#k9_cat_1 :::"*"::: ) (Set (Var "G"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "B")))) ")" )))) ; theorem :: ISOCAT_1:50 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "F")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "G")) "being" ($#m2_cat_1 :::"Functor"::: ) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "G")) ($#k9_cat_1 :::"*"::: ) (Set (Var "F"))) ($#r3_nattra_1 :::"~="::: ) (Set ($#k10_cat_1 :::"id"::: ) (Set (Var "A"))))) "holds" (Bool (Set (Var "F")) "is" ($#v14_cat_1 :::"faithful"::: ) )))) ; theorem :: ISOCAT_1:51 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#l1_cat_1 :::"Category":::) "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r2_isocat_1 :::"are_equivalent"::: ) )) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_isocat_1 :::"Equivalence"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v13_cat_1 :::"full"::: ) ) & (Bool (Set (Var "F")) "is" ($#v14_cat_1 :::"faithful"::: ) ) & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "B")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "A")) "st" (Bool (Set (Var "b")) "," (Set (Set (Var "F")) ($#k8_cat_1 :::"."::: ) (Set (Var "a"))) ($#r1_cat_1 :::"are_isomorphic"::: ) )) ")" ) ")" ))) ; definitionlet "C" be ($#l1_cat_1 :::"Category":::); func :::"IdMap"::: "C" -> ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "C") "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "C") means :: ISOCAT_1:def 12 (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" "C" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "o"))))); end; :: deftheorem defines :::"IdMap"::: ISOCAT_1:def 12 : (Bool "for" (Set (Var "C")) "being" ($#l1_cat_1 :::"Category":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "C"))) "," (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "C"))) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_isocat_1 :::"IdMap"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Object":::) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k4_cat_1 :::"id"::: ) (Set (Var "o"))))) ")" )));