(* try to do isomorphism between Fun [C x D, E] and Fun [C, Fun [D, E]], see Dexter Kozen, Christoph Kreitz, and Eva Richter. Automating proofs in category theory. (IJCAR'06) *) theory kozenc imports HOL_Gen begin (* formerly used functions to model arrows types ('src, 'tgt) arrow = "'src => 'tgt" *) typedef 'a obj = "{arbitrary :: 'a}" by auto consts mk_obj :: "'a obj" dest_pair_obj :: "('a * 'b) obj => 'a obj * 'b obj" mk_pair_obj :: "'a obj * 'b obj => ('a * 'b) obj" defs mk_obj_def : "mk_obj == Abs_obj arbitrary" mk_pair_obj_def : "mk_pair_obj p == Abs_obj arbitrary" dest_pair_obj_def : "dest_pair_obj p == (Abs_obj arbitrary, Abs_obj arbitrary)" typedecl ('src, 'tgt) arrow consts (* arrow has right source and target *) arrst :: "['src obj, ('src, 'tgt) arrow, 'tgt obj] => bool" source :: "(('src, 'tgt) arrow) => 'src obj" target :: "(('src, 'tgt) arrow) => 'tgt obj" defs arrst_def : "arrst src arr tgt == True" source_def : "source (arr :: ('src, 'tgt) arrow) == arbitrary :: 'src obj" target_def : "target (arr :: ('src, 'tgt) arrow) == arbitrary :: 'tgt obj" (* identity and composition of arrows *) consts arr_id :: "('c, 'c) arrow" ("ida") arr_comp :: "[('c2, 'c3) arrow, ('c1, 'c2) arrow] => ('c1, 'c3) arrow" (infixl "oa" 55) axioms arr_id : "arr_id oa f = f & f oa arr_id = f" arr_assoc : "f oa (g oa h) = f oa g oa h" (* the three categories C, D, E *) axclass catC < type axclass catD < type axclass catCD < type axclass catE < type arities * :: (catC, catD) catCD (* the product category, identity and composition, an arrow is a pair of arrows in C and in D *) consts prod_id :: "('c, 'c) arrow * ('d, 'd) arrow" ("idx") prod_comp :: "[('c2, 'c3) arrow * ('d2, 'd3) arrow, ('c1, 'c2) arrow * ('d1, 'd2) arrow] => ('c1, 'c3) arrow * ('d1, 'd3) arrow" (infixl "ox" 55) defs prod_id_def : "prod_id == (ida, ida)" primrec prod_comp_def : "prod_comp (gc, gd) fcd = (case fcd of (fc, fd) => (gc oa fc, gd oa fd))" (* composition of arrows in the various categories *) consts compC :: "('a :: catC, 'b :: catC) arrow => ('c :: catC, 'a) arrow => ('c, 'b) arrow" (infixl "oc" 55) compD :: "('a :: catD, 'b :: catD) arrow => ('c :: catD, 'a) arrow => ('c, 'b) arrow" (infixl "od" 55) compE :: "('a :: catE, 'b :: catE) arrow => ('c :: catE, 'a) arrow => ('c, 'b) arrow" (infixl "oe" 55) compCD :: "[('c2 :: catC, 'c3 :: catC) arrow * ('d2, 'd3 :: catD) arrow, ('c1 :: catC, 'c2) arrow * ('d1 :: catD, 'd2 :: catD) arrow] => ('c1, 'c3) arrow * ('d1, 'd3) arrow" (infixl "ocd" 55) idC :: "('a :: catC, 'a) arrow" idD :: "('a :: catD, 'a) arrow" idCD :: "('a :: catC, 'a) arrow * ('d :: catD, 'd) arrow" idE :: "('a :: catE, 'a) arrow" defs compC_def : "compC == arr_comp" compD_def : "compD == arr_comp" compCD_def : "compCD == prod_comp" compE_def : "compE == arr_comp" idC_def : "idC == ida" idD_def : "idD == ida" idCD_def : "idCD == idx" idE_def : "idE == ida" end