Theory NatTrans

(*  Title:       Category theory using Isar and Locales
    ID:          $Id: NatTrans.thy,v 1.9 2008-12-30 15:30:12 ballarin Exp $
    Author:      Greg O'Keefe, June, July, August 2003

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

header {* 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 ∈ Hom2 (F\<o> A) (G\<o> A)" 
  and "∀A∈Ob. ∀B∈Ob. ∀f∈Hom A B. (G\<a> f) •2 (u A) = (u B) •2 (F\<a> 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 two_cats_axioms.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)\<o> A)  ((id_func AA)\<o> 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)\<a> f • (λA∈Ob. Id A) A
      = (λA∈Ob. Id A) B • (id_func AA)\<a> f"
    by (simp add:  id_func_def)
qed (auto intro: id_func_functor, unfold_locales, unfold_locales)

end