(* first, our category of types and functions has finite products *) structure index = struct val thy = the_context () end ; use_legacy_bindings index.thy ; val _ = qed_goal "product_property" index.thy "(fst o h = f & snd o h = g) = (prodf f g = h)" (fn _ => [ (safe_tac (cis [ext])), (ALLGOALS (simp_tac (esimps [prodf_def]))) ]) ; val _ = qed_goal "sum_property" index.thy "(h o Inl = f & h o Inr = g) = (sum_case f g = h)" (fn _ => [ (safe_tac (cis [ext])), (case_tac "x" 1), Auto_tac ]) ; val _ = qed_goal "H_assoc" index.thy "H_comp h (H_comp g f) = H_comp (H_comp h g) f" (fn _ => [ (safe_tac (cis [ext])), Simp_tac 1 ]) ; val _ = qed_goal "H_o_id" index.thy "H_comp f H_id = f" (fn _ => [ (safe_tac (cis [ext])), Simp_tac 1 ]) ; val _ = qed_goal "H_id_o" index.thy "H_comp H_id f = f" (fn _ => [ (safe_tac (cis [ext])), Simp_tac 1 ]) ; (* given f :: 'a' => 'a, H f is a functor *) val _ = qed_goal "H_fun_id" index.thy "H fa H_id = H_id" (fn _ => [ (safe_tac (cis [ext])), Simp_tac 1 ]) ; val _ = qed_goal "H_fun_comp" index.thy "H fa (H_comp g f) = H_comp (H fa g) (H fa f)" (fn _ => [ (safe_tac (cis [ext])), Simp_tac 1 ]) ; (* H (taking an object A to a category H_A), is a contravariant functor *) val _ = qed_goal "H_cv_id" index.thy "H id = id" (fn _ => [ (safe_tac (cis [ext])), Simp_tac 1 ]) ; val _ = qed_goal "H_cv_comp" index.thy "H (f o g) = H g o H f" (fn _ => [ (safe_tac (cis [ext])), Simp_tac 1 ]) ;