theory funcat imports Gen HOL_Gen begin (* to do with category of functors and nts *) typedecl 'c F typedecl 'c G typedecl 'c H typedecl 'c H2 typedecl 'd J typedecl 'e K (* natural transformations between functors from catC to catD *) axclass catC < type axclass catD < type axclass catE < type axclass catF < type arities F :: (catC) catD G :: (catC) catD H :: (catC) catD H2 :: (catC) catD J :: (catD) catE K :: (catE) catF consts (* identity functors on category C, D *) idC :: "('a :: catC => 'b :: catC) => ('a => 'b)" idD :: "('a :: catD => 'b :: catD) => ('a => 'b)" F :: "('a :: catC => 'b :: catC) => ('a F => 'b F)" G :: "('a :: catC => 'b :: catC) => ('a G => 'b G)" H :: "('a :: catC => 'b :: catC) => ('a H => 'b H)" H2 :: "('a :: catC => 'b :: catC) => ('a H2 => 'b H2)" J :: "('a :: catD => 'b :: catD) => ('a J => 'b J)" K :: "('a :: catE => 'b :: catE) => ('a J => 'b J)" nt_idF :: "'a :: catC F => 'a F" nt_idG :: "'a :: catC G => 'a G" ntFG :: "'a :: catC F => 'a G" ntGH :: "'a :: catC G => 'a H" ntHH2 :: "'a :: catC H => 'a H2" defs nt_idF_def : "nt_idF == id" nt_idG_def : "nt_idG == id" idC_def : "idC == id" idD_def : "idD == id" axioms (* F and J are functors *) fcompF : "F (g o f) = F g o F f" fidF : "F id = id" fcompJ : "J (g o f) = J g o J f" fidJ : "J id = id" (* ntFG and ntGH are natural transformations *) ntFG : "G f o ntFG = ntFG o F f" ntGH : "H f o ntGH = ntGH o G f" (** the category of arrows and arrow morphisms *) consts is_arrow_morphism :: (* source arrow, arrow_morphism, target arrow *) "('as => 'at) * (('as => 'bs) * ('at => 'bt)) * ('bs => 'bt) => bool" (* identity arrow morphism, on arrow 's => 't *) arrow_morphism_id :: "(('s => 's) * ('t => 't))" arrow_morphism_comp :: "('bs => 'cs) * ('bt => 'ct) => ('as => 'bs) * ('at => 'bt) => ('as => 'cs) * ('at => 'ct)" (infixl "oa" 55) recdef is_arrow_morphism "measure size" "is_arrow_morphism (sarr, (ams, amt), tarr) = (tarr o ams = amt o sarr)" primrec "arrow_morphism_comp (gs, gt) f = (case f of (fs, ft) => (gs o fs, gt o ft))" defs arrow_morphism_id_def : "arrow_morphism_id == (id, id)" end