(* one pair of corresponding functors, F : Fun [C x D, E] and G : Fun [C, Fun [D, E]] *) theory kozen3 imports kozenc begin (* action of the functors in question on objects *) typedecl ('c, 'd) F arities F :: (catC, catD) catE (* an object of Fun [C x D, E] : type of its action on arrows *) types ('cs, 'ct, 'ds, 'dt) fxeT = "('cs, 'ct) arrow * ('ds, 'dt) arrow => (('cs, 'ds) F, ('ct, 'dt) F) arrow" (* an object of Fun [C, Fun [D, E]], on an object of C, it gives a functor from D to E, Go; on an arrow of C it gives an arrow of Fun [D, E], ie a natural transformation Ga, giving an arrow in E for each object of D *) ('c, 'ds, 'dt) cfoT = "'c obj => ('ds, 'dt) arrow => (('c, 'ds) F, ('c, 'dt) F) arrow" ('cs, 'ct, 'd) cfaT = "(('cs, 'ct) arrow) => 'd obj => (('cs, 'd) F, ('ct, 'd) F) arrow" (* define a functor from X (ie C x D) to E *) consts F :: "('cs :: catC, 'ct :: catC, 'ds :: catD, 'dt :: catD) fxeT" (* F is a functor *) axioms idF : "F idCD = idE" compF : "F (g ocd f) = F g oe F f" (* the isomorphism theta, a functor from Fun [C x D, E] to Fun [C, Fun [D, E]] for F : Fun [C x D, E], ie, F is a functor from C x D to E action of theta F on object of C is an object of Fun [D, E], ie a functor from D to E; we give its action on arrows *) consts theta_F_obj_arr :: "('c :: catC, 'ds :: catD, 'dt :: catD) cfoT" defs theta_F_obj_arr_def : "theta_F_obj_arr cty darr == F (idC, darr)" (* for F : Fun [C x D, E], action of theta F on arrow of C is an arrow of Fun [D, E], ie a natural transformation, giving an arrow in E for each object of D *) consts theta_F_arr :: "('cs :: catC, 'ct :: catC, 'd :: catD) cfaT" defs theta_F_arr_def : "theta_F_arr carr dty == F (carr, idD)" (* the converse direction *) consts Go :: "('c :: catC, 'ds :: catD, 'dt :: catD) cfoT" Ga :: "('cs :: catC, 'ct :: catC, 'd :: catD) cfaT" (* result of Go is a functor, result of Ga is a natural transformation, Ga is a functor *) axioms idGo : "Go c idD = idE" compGo : "Go c (g od f) = Go c g oe Go c f" ntGa_ty : "arrst cs carr ct ==> arrst ds darr dt ==> Go ct darr oe Ga carr ds = Ga carr dt oe Go cs darr" idGa : "Ga idC d = idE" (* Ga id is the identity natural transformation *) compGa : "Ga (g oc f) d = Ga g d oe Ga f d" (* the isomorphism eta, a functor from Fun [C, Fun [D, E]] to Fun [C x D, E] we give action of eta G on arrows *) consts etaG :: "('cs :: catC, 'ct :: catC, 'ds :: catD, 'dt :: catD) fxeT" primrec etaG_def : "etaG (carr, darr) = Go (target carr) darr oe Ga carr (source darr)" (* axioms for proving theta and eta mutually inverse *) axioms etaG_F : "etaG = F" end