Require Export cat__.
Implicit Arguments On.
Natural Transformations |
Notations and conventions:
|
Module NT__.
Export Misc__.
Export Cat__.
Section NT.
Variable A,B:Cat; F,G:(Functor A B).
Definition NT_Comm [n:(x:A)(mor (F x) (G x))] : Prop :=
(x,y:A; f:(mor x y))
(oo (n y) (fct F f))==(oo (fct G f) (n x)).
Record NT : Type := {
nt_data :> (x:A) (mor (F x) (G x));
ax_nt_comm :> (NT_Comm nt_data)
}.
Lemma nt_comm : (n:NT; x,y:A; f:(mor x y))
(oo (n y) (fct F f))==(oo (fct G f) (n x)).
Proof.
Intros; Apply ax_nt_comm.
Qed.
Lemma nt_extens : (n,m:NT)
((x:A) (n x)==(m x)) -> n==m.
Proof.
NewDestruct n; NewDestruct m; Simpl; Intros.
Assert nt_data0==nt_data1.
Apply extensionality with T := [x:A](mor (F x) (G x)).
Assumption.
NewDestruct H0.
Assert ax_nt_comm0==ax_nt_comm1.
Apply proof_irrelevance.
NewDestruct H0.
Reflexivity.
Qed.
End NT.
Hints Resolve nt_comm nt_extens.
Category of functors |
| Functors with natural transformations form a category. |
Section Functor_Cat.
Variable A,B:Cat.
Definition nt_id [F:(Functor A B)] : (NT F F).
Proof.
Intros; Split with [x:A](ii (F x)).
Abstract Unfold NT_Comm; Intros;
Rewrite ii_sx; Rewrite ii_dx; Reflexivity.
Defined.
Implicits nt_id [1].
Section NT_Comp.
Variable F,G,H:(Functor A B).
Variable m:(NT G H); n:(NT F G).
Local p [x:A] : (mor (F x) (H x)) := (oo (m x) (n x)).
Remark p_theory : (NT_Comm p).
Proof.
Unfold p NT_Comm; Intros.
Rewrite <- oo_assoc.
Rewrite (nt_comm n).
Rewrite oo_assoc.
Rewrite (nt_comm m).
Rewrite oo_assoc.
Reflexivity.
Qed.
Definition nt_comp : (NT F H).
Proof.
Split with p; Exact p_theory.
Defined.
End NT_Comp.
Lemma nt_comp_assoc : (F,G,H,I:(Functor A B))
(n:(NT F G); m:(NT G H); p:(NT H I))
(nt_comp p (nt_comp m n))==(nt_comp (nt_comp p m) n).
Proof.
Intros; Apply nt_extens; Simpl; Auto.
Qed.
Lemma nt_sx_id : (F,G:(Functor A B); n:(NT F G))
(nt_comp nt_id n)==n.
Proof.
Intros; Apply nt_extens; Simpl; Auto.
Qed.
Lemma nt_dx_id : (F,G:(Functor A B); n:(NT F G))
(nt_comp n nt_id)==n.
Proof.
Intros; Apply nt_extens; Simpl; Auto.
Qed.
End Functor_Cat.
Hints Resolve nt_comp_assoc nt_sx_id nt_dx_id.
End NT__.