(* for object A in base category with finite products, get new category H_A where H_A-arrows (B, C) = arrows (A \times B, C), see Ross Paterson. A New Notation for Arrows, ICFP'01, s3.3 *) theory index imports HOL_Gen begin consts (* set of arrows in H_A *) H_arrows :: "'a => 'b * 'c => ('a * 'b => 'c) set" H_comp :: "['a * 'c => 'd, 'a * 'b => 'c] => ('a * 'b => 'd)" H_id :: "'a * 'b => 'b" (* given f :: 'a' => 'a, get functor H f :: H_a' -> H_a, which is the identity on objects *) H :: "('a' => 'a) => ('a * 'b => 'c) => ('a' * 'b => 'c)" (* the contravariant functor *) primrec H_arrows_def : "H_arrows a (b, c) = (UNIV :: ('a * 'b => 'c) set)" primrec H_id_def : "H_id (a, b) = b" primrec H_comp_def : "H_comp g f (a, b) = g (a, f (a, b))" primrec H_def : "H fa g (a', b) = g (fa a', b)" (* first, category of types and functions has finite products *) consts prodf :: "['x => 'a, 'x => 'b] => 'x => 'a * 'b" defs prodf_def : "prodf f g x == (f x, g x)" end