(* natural transformations between functors described in kozen1/2.thy *) theory kozennt imports kozen1 kozen2 begin types (* for natural transformation, with and without objects *) ('c, 'd) nt12T = "(('c, 'd) kozen1.F, ('c, 'd) kozen2.F) arrow" ('c, 'd) nt12cT = "'c obj => 'd obj => ('c, 'd) nt12T" (* ('c, 'd) nt12pT = "('c * 'd) obj => ('c, 'd) nt12T" *) (* H is a natural transformation from F1 to F2 ie an arrow in Fun [C x D, E] *) consts (* object is ('c :: catC * 'd :: catD) *) H :: "('c :: catC, 'd :: catD) nt12T" thetaH :: "('c :: catC, 'd :: catD) nt12cT" axioms (* H is a natural transformation: F1 -> F2 : C x D -> E, for each arrow in C x D, get commuting diagram in E *) nt_H : "kozen2.F (carr, darr) oe H = H oe kozen1.F (carr, darr)" (* thetaH is a natural transformation: G1 -> G2 : C -> Fun [D, E], for each object c : C, have an arrow in Fun [D, E], ie a natural transformation : G1 c -> G2 c : D -> E, ie, for each object d : D, have an arrow in E, : G1 c d -> G2 c d *) defs thetaH_def : "thetaH c d == H" (* the converse direction *) (* J is a natural transformation from G1 to G2 ie an arrow in Fun [C, Fun [D, E]], ie for each object c : C, an arrow in Fun [D, E] from G1 c to G2 c, ie a natural transformation : G1 c -> G2 c : D -> E, ie, for each object d : D, an arrow in E : G1 c d -> G2 c d *) consts J :: "('c :: catC, 'd :: catD) nt12cT" etaJ :: "('c :: catC, 'd :: catD) nt12T" axioms (* J is a nt *) J_nt : "kozen2.Ga carr d oe J cs d = J ct d oe kozen1.Ga carr d" (* for each c, J c is a nt *) J_c_nt : "kozen2.Go c darr oe J c ds = J c dt oe kozen1.Go c darr" defs etaJ_def : "etaJ == J arbitrary arbitrary" end