(* natural transformations between functors described in kozen1/2.thy *) structure kozennt = struct val thy = the_context () end ; val _ = use_legacy_bindings kozennt.thy ; val icss = HOL_ss addsimps (prod_id_def :: ic_defs) addsimprocs [obj_is_arb.sp] ; val [J_nt', J_c_nt'] = map (simplify icss) [J_nt, J_c_nt] ; (* for each c : C, thetaH c is a nt : G1 c -> G2 c : D -> E *) val _ = qed_goalw "thetaH_c_nt" kozennt.thy [KT1.theta_F_obj_arr_def, KT2.theta_F_obj_arr_def, thetaH_def] "kozen2.theta_F_obj_arr c darr oe thetaH c ds = \ \ thetaH c dt oe kozen1.theta_F_obj_arr c darr" (fn _ => [ (rtac nt_H 1) ]) ; (* thetaH is an nt : G1 -> G2 : C -> Fun [D, E], this is a commutative diagram in Fun [D, E], ie of nts : D -> E, so requires commutation at each component, ie for each d : D *) val _ = qed_goalw "thetaH_nt" kozennt.thy [KT1.theta_F_arr_def, KT2.theta_F_arr_def, thetaH_def] "kozen2.theta_F_arr carr d oe thetaH cs d = \ \ thetaH ct d oe kozen1.theta_F_arr carr d" (fn _ => [ (rtac nt_H 1) ]) ; (* etaJ is a natural transformation: F1 -> F2 : C x D -> E, for each arrow in C x D, get commuting diagram in E *) val _ = qed_goalw "etaJ_nt" kozennt.thy [etaJ_def] "kozen2.etaG (carr, darr) oe etaJ = etaJ oe kozen1.etaG (carr, darr)" (fn _ => [ (simp_tac (esimps [source_def, target_def, compE_def]) 1), (simp_tac (esimps [arr_assoc, J_c_nt', mk_oaap J_nt']) 1) ]) ; (* set show_types ; reset show_types ; set show_sorts ; reset show_sorts ; *) (* still need to show theta and eta are functors, but this is rather trivial *)