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.