Theory NatTrans

(*  Title:       Category theory using Isar and Locales
    Author:      Greg O'Keefe, June, July, August 2003
    License: LGPL

Define natural transformation, prove that the identity arrow function is one.
*)

section ‹Natural Transformations›

theory NatTrans
imports Functors
begin

(* guess the third axiom is implied by the fifth *)
locale natural_transformation = two_cats +
  fixes F and G and u
  assumes "Functor F : AA  BB"
  and "Functor G : AA  BB"
  and "u : ob AA  ar BB"
  and "u  extensional (ob AA)"
  and "AOb. u A  HomBB(F𝗈 A) (G𝗈 A)" 
  and "AOb. BOb. fHom A B. (G𝖺 f) BB(u A) = (u B) BB(F𝖺 f)"

abbreviation
  nt_syn  ("_ : _  _ in Func '(_ , _ ')" [81]) where
  "u : F  G in Func(AA, BB)  natural_transformation AA BB F G u"

(* is this doing what I think its doing? *)
locale endoNT = natural_transformation + one_cat

theorem (in endoNT) id_restrict_natural:
  "(λAOb. Id A) : (id_func AA)  (id_func AA) in Func(AA,AA)"
proof (intro natural_transformation.intro natural_transformation_axioms.intro 
    two_cats.intro ballI)
  show "(λAOb. Id A) : Ob  Ar"
    by (rule funcsetI) auto
  show "(λAOb. Id A)  extensional (Ob)"
    by (rule restrict_extensional)
  fix A 
  assume A: "A  Ob" 
  hence "Id A  Hom A A" ..
  thus "(λXOb. Id X) A  Hom ((id_func AA)𝗈 A)  ((id_func AA)𝗈 A)"
    using A by (simp add: id_func_def) 
  fix B and f
  assume B: "B  Ob" 
    and "f  Hom A B"
  hence "f  Ar" and "A = Dom f" and "B = Cod f" and "Dom f  Ob" and "Cod f  Ob"
    using A by (simp_all add: hom_def)
  thus "(id_func AA)𝖺 f  (λAOb. Id A) A
      = (λAOb. Id A) B  (id_func AA)𝖺 f"
    by (simp add:  id_func_def)
qed (auto intro: id_func_functor, unfold_locales, unfold_locales)

end