structure funcat = struct val thy = the_context () end ; val _ = use_legacy_bindings funcat.thy ; (* composition of functors is a functor *) val comp_fun = prove_goal funcat.thy "(J o F) id = id & (J o F) (g o f) = (J o F) g o (J o F) f" (fn _ => [ (Safe_tac), (simp_tac (esimps [fidF, fidJ]) 1), (simp_tac (esimps [fcompF, fcompJ]) 1) ]) ; (* identity functor is a functor *) val id_fun = prove_goalw funcat.thy [idC_def] "idC id = id & idC (g o f) = idC g o idC f" fn_at ; (* composition of functors obeys identity and associativity *) val fun_comp_id_ass = prove_goalw funcat.thy [idC_def, idD_def] "F o idC = F & idD o F = F & K o (J o F) = (K o J) o F" (fn _ => [ Safe_tac, (ALLGOALS (rtac ext)), Auto_tac ]) ; (* composition of natural transformations is a natural transformation *) val comp_nt1 = prove_goal funcat.thy "H f o (ntGH o ntFG) = (ntGH o ntFG) o F f" (fn _ => [ (simp_tac (esimps [o_assoc, ntGH, mk_oap ntFG]) 1) ]) ; (* this theorem only requires assumptions for particular f :: 'a => 'b *) val comp_nt2 = prove_goal funcat.thy "[| H f o ntGH = ntGH o G f ; G f o ntFG = ntFG o F f |] ==> \ \ H f o (ntGH o ntFG) = (ntGH o ntFG) o F f" (fn [ntGH, ntFG] => [ (simp_tac (esimps [o_assoc, ntGH, mk_oap ntFG]) 1) ]) ; (* identity natural transformation is a natural transformation *) val id_nt = prove_goalw funcat.thy [nt_idF_def] "F f o nt_idF = nt_idF o F f" (fn_at) ; (* composition of natural transformations obeys identity and associativity *) val nt_comp_id_ass = prove_goalw funcat.thy [nt_idF_def, nt_idG_def] "ntFG o nt_idF = ntFG & nt_idG o ntFG = ntFG & \ \ ntHH2 o (ntGH o ntFG) = (ntHH2 o ntGH) o ntFG" (fn _ => [ Safe_tac, (ALLGOALS (rtac ext)), Auto_tac ]) ; (** the category of arrows and arrow morphisms *) (* arrow_morphism_id is an arrow_morphism *) val id_is_am = prove_goalw funcat.thy [arrow_morphism_id_def] "is_arrow_morphism (arr, arrow_morphism_id, arr)" fn_at ; val _ = qed_goal_spec_mp "comp_is_am" funcat.thy "is_arrow_morphism (a, (fs, ft), b) --> \ \ is_arrow_morphism (b, (gs, gt), c) --> \ \ is_arrow_morphism (a, (gs, gt) oa (fs, ft), c)" (fn _ => [ Clarsimp_tac 1, (asm_simp_tac (esimps [o_assoc]) 1), (asm_simp_tac (esimps [o_assoc RS sym]) 1) ]) ; (* composition of arrow_morphisms obeys identity and associativity *) val am_comp_id_ass = prove_goalw funcat.thy [arrow_morphism_id_def] "(fs, ft) oa arrow_morphism_id = (fs, ft) & \ \ arrow_morphism_id oa (fs, ft) = (fs, ft) & \ \ ((hs, ht) oa (gs, gt)) oa (fs, ft) = \ \ (hs, ht) oa ((gs, gt) oa (fs, ft))" (fn _ => [ (simp_tac (esimps [o_assoc]) 1) ]) ;