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 "∀A∈Ob. u A ∈ Hom⇘BB⇙ (F⇘𝗈⇙ A) (G⇘𝗈⇙ A)" 
  and "∀A∈Ob. ∀B∈Ob. ∀f∈Hom 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:
  "(λA∈Ob. 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 "(λA∈Ob. Id A) : Ob → Ar"
    by (rule funcsetI) auto
  show "(λA∈Ob. Id A) ∈ extensional (Ob)"
    by (rule restrict_extensional)
  fix A 
  assume A: "A ∈ Ob" 
  hence "Id A ∈ Hom A A" ..
  thus "(λX∈Ob. 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 ∙ (λA∈Ob. Id A) A
      = (λA∈Ob. Id A) B ∙ (id_func AA)⇘𝖺⇙ f"
    by (simp add:  id_func_def)
qed (auto intro: id_func_functor, unfold_locales, unfold_locales)

end