Require Export misc_.
Require Export map_.
Require Export map_.
Require Export cat_sig_.
Implicit Arguments On.
Categories. |
| Development of Category Theory. |
Notations and conventions:
|
Module Cat_ <: Cat_Sig_.
Export Map_.
Export Misc_.
Definition of category |
Section Cat_Theory.
Variable A:Type; mor:A->A->Type.
Variable oo:(x,y,z:A)(mor y z)->(mor x y)->(mor x z).
Variable ii:(x:A)(mor x x).
Record Cat_Theory : Prop := {
ax_oo_assoc : (x,y,z,w:A; h:(mor z w); g:(mor y z); f:(mor x y))
(oo h (oo g f))==(oo (oo h g) f);
ax_ii_sx : (x,y:A; f:(mor x y)) (oo (ii y) f)==f;
ax_ii_dx : (x,y:A; f:(mor x y)) (oo f (ii x))==f
}.
End Cat_Theory.
Record Cat_Data : Type := {
obj :> Type;
mor : obj->obj->Type;
oo : (x,y,z:obj; g:(mor y z); f:(mor x y)) (mor x z);
ii : (x:obj) (mor x x)
}.
Implicits ii [1].
Record Cat : Type := {
cat_data :> (Cat_Data);
cat_theory :> (Cat_Theory (!oo cat_data) (!ii cat_data))
}.
Section Cat_Facts.
Variable A:Cat.
Lemma oo_congr : (x,y,z:A; g1,g2:(mor y z); f1,f2:(mor x y))
g1==g2 -> f1==f2 -> (oo g1 f1)==(oo g2 f2).
Proof.
NewDestruct 1; NewDestruct 1; Reflexivity.
Qed.
Lemma oo_assoc : (x,y,z,w:A; h:(mor z w); g:(mor y z); f:(mor x y))
(oo h (oo g f))==(oo (oo h g) f).
Proof.
Apply (ax_oo_assoc A).
Qed.
Lemma ii_sx : (x,y:A; f:(mor x y))(oo (ii y) f)==f.
Proof.
Apply (ax_ii_sx A).
Qed.
Lemma ii_dx : (x,y:A; f:(mor x y))(oo f (ii x))==f.
Proof.
Apply (ax_ii_dx A).
Qed.
End Cat_Facts.
Hints Resolve oo_assoc ii_sx ii_dx oo_congr.
Definition src [A:Cat; x,y:A; f:(mor x y)] : A := x.
Definition trg [A:Cat; x,y:A; f:(mor x y)] : A := y.
Equality between morphisms of a category |
| We introduce a notion of equality between morphisms that permits to compare morphisms with different source and targets. |
Section Eq_Mor.
Variable A:Cat.
Inductive eq_mor [x,y:A; f:(mor x y)] : (u,v:A; g:(mor u v)) Prop :=
| eq_mor_refl : (eq_mor f f).
Hints Resolve eq_mor_refl.
Lemma eq_mor_sym : (x,y:A; f:(mor x y); u,v:A; g:(mor u v))
(eq_mor f g) -> (eq_mor g f).
Proof.
NewDestruct 1; Split.
Qed.
Lemma eq_mor_trans :
(x,y:A; f:(mor x y); u,v:A; g:(mor u v); s,t:A; h:(mor s t))
(eq_mor f g) -> (eq_mor g h) -> (eq_mor f h).
Proof.
NewDestruct 1; NewDestruct 1; Split.
Qed.
Lemma eq_mor_src : (x,y:A; f:(mor x y); u,v:A; g:(mor u v))
(eq_mor f g) -> (src f) == (src g).
Proof.
NewDestruct 1; Split.
Qed.
Lemma eq_mor_trg : (x,y:A; f:(mor x y); u,v:A; g:(mor u v))
(eq_mor f g) -> (trg f) == (trg g).
Proof.
NewDestruct 1; Split.
Qed.
Now we prove that this eq_mor actually specialize to eqT if the source and the target of the two morphisms being compared are the same.
|
Lemma eq_mor_eqT : (x,y:A; f,g:(mor x y)) (eq_mor f g) -> f==g.
Proof.
Intros.
LetTac P := [w,z:A; h:(mor w z)]
(H:(mor w z)==(mor x y))f==(transport H h).
Cut (P ? ? g).
Unfold P; Intros.
Apply (H0 (refl_eqT (mor x y))).
Elim H.
Unfold P; Intros.
Rewrite transport_refl; Split.
Qed.
End Eq_Mor.
Inverse of a morphism. |
Section Inverse_Mor.
Variable A:Cat; sx,dx:A; f:(mor sx dx).
Section Inverse_Mor_Theory.
Variable g:(mor dx sx).
Record Inverse_Mor_Theory : Prop := {
ax_inverse_eq_sx : (oo g f)==(ii sx);
ax_inverse_eq_dx : (oo f g)==(ii dx)
}.
End Inverse_Mor_Theory.
Record Inverse_Mor : Type := {
inverse_mor :> (mor dx sx);
inverse_mor_theory : (Inverse_Mor_Theory inverse_mor)
}.
Section Inverse_Mor_Facts.
Variable g:Inverse_Mor.
Lemma inverse_eq_sx : (oo g f)==(ii sx).
Proof.
Elim g; Simpl; NewDestruct 1; Auto.
Qed.
Lemma inverse_eq_dx : (oo f g)==(ii dx).
Proof.
Elim g; Simpl; NewDestruct 1; Auto.
Qed.
End Inverse_Mor_Facts.
Hints Resolve inverse_eq_sx inverse_eq_dx.
End Inverse_Mor.
Functors |
Section Functor_Theory.
Variable A,B:Cat.
Variable F0:A->B; F1:(x,y:A) (mor x y) -> (mor (F0 x) (F0 y)).
Record Functor_Theory : Prop := {
ax_fct_oo : (x,y,z:A; g:(mor y z); f:(mor x y))
(F1 (oo g f))==(oo (F1 g) (F1 f));
ax_fct_ii : (x:A) (F1 (ii x))==(ii (F0 x))
}.
End Functor_Theory.
Record Functor_Data [A,B:Cat] : Type := {
fct_obj :> A->B;
fct : (x,y:A; f:(mor x y)) (mor (fct_obj x) (fct_obj y))
}.
Record Functor [A,B:Cat] : Type := {
functor_data :> (Functor_Data A B);
functor_theory :> (Functor_Theory (fct functor_data))
}.
Section Functor_Facts.
Variable A,B:Cat; F:(Functor A B).
Lemma fct_oo : (x,y,z:A; g:(mor y z); f:(mor x y))
(fct F (oo g f))==(oo (fct F g) (fct F f)).
Proof.
Intros; Apply (ax_fct_oo F).
Qed.
Lemma fct_ii : (x:A) (fct F (ii x))==(ii (F x)).
Proof.
Intros; Apply (ax_fct_ii F).
Qed.
End Functor_Facts.
Hints Resolve fct_oo fct_ii.
Definition Morph [A,B:Cat] : Type := (Functor A B).
Section Eq_Fct.
Variable A,B:Cat.
Definition eq_fct [F,G:(Functor A B)] : Prop :=
(x,y:A; f:(mor x y)) (eq_mor (fct F f) (fct G f)).
Variable F,G:(Functor A B); F_eq_G:(eq_fct F G).
Lemma eq_fct_src : (x,y:A; f:(mor x y))
(src (fct F f))==(src (fct G f)).
Proof.
Intros; NewDestruct (F_eq_G f); Reflexivity.
Qed.
Lemma eq_fct_trg : (x,y:A; f:(mor x y))
(trg (fct F f))==(trg (fct G f)).
Proof.
Intros; NewDestruct (F_eq_G f); Reflexivity.
Qed.
Lemma eq_fct_obj : (x:A)(F x)==(G x).
Proof.
Intros.
Change (src (ii (F x)))==(src (ii (G x))).
Do 2 Rewrite <- fct_ii.
Apply eq_fct_src.
Qed.
Extensionality for functors |
We prove that eq_fct implies eqT.
|
Lemma functor_extens : F==G.
Proof.
Assert U := eq_fct_obj.
NewDestruct F; NewDestruct G.
NewDestruct functor_data0.
NewDestruct functor_data1.
Simpl in U.
Assert E : fct_obj0==fct_obj1.
Apply nondep_extensionality.
Apply U.
NewDestruct E.
Clear F G U.
Rename fct_obj0 into FF.
Assert E : fct0==fct1.
Apply extensionality
with T := [x:A](y:A)(mor x y)->(mor (FF x) (FF y)).
Intros.
Apply extensionality
with T := [y:A](mor x y)->(mor (FF x) (FF y)).
Intros.
Apply nondep_extensionality.
Intros.
Unfold eq_fct in F_eq_G.
Simpl in F_eq_G.
Apply eq_mor_eqT.
Apply (F_eq_G x1).
NewDestruct E.
Assert E : functor_theory0 == functor_theory1.
Apply proof_irrelevance.
NewDestruct E.
Reflexivity.
Qed.
End Eq_Fct.
Category of categories. |
Now we prove that categories with functors form a category (in a higher universe). We do not build the term of type Cat__.Obj in this file. We will use the parametric module Make_Small_Cat_ to do that. Here we simply make sure that the module Cat_ will be of module type Cat_Sig_ by defying the term morph_id, morph_comp etc.
|
| Identity functor. |
Definition morph_id [A:Cat] : (Functor A A).
Proof.
Intro.
Split with (!Build_Functor_Data A A [x:A]x [x,y:A; f:(mor x y)]f).
Abstract Split; Simpl; Intros; Reflexivity.
Defined.
| Composition of functors. |
Section Functor_Comp.
Variable A,B,C:Cat.
Variable G:(Functor B C); F:(Functor A B).
Local h : (Functor_Data A C) :=
(!Build_Functor_Data A C
[x:A](G (F x))
[x,y:A; f:(mor x y)] (fct G (fct F f))).
Remark h_th : (Functor_Theory (fct h)).
Proof.
Split; Simpl; Intros.
Repeat Rewrite fct_oo; Auto.
Repeat Rewrite fct_ii; Auto.
Qed.
Definition morph_comp : (Functor A C).
Proof.
Split with h; Exact h_th.
Defined.
End Functor_Comp.
Lemma morph_comp_assoc : (A,B,C,D:Cat)
(H:(Functor C D); G:(Functor B C); F:(Functor A B))
(morph_comp H (morph_comp G F))==(morph_comp (morph_comp H G) F).
Proof.
Intros; Apply functor_extens.
Unfold morph_comp eq_fct; Simpl; Intros.
Apply eq_mor_refl.
Qed.
Lemma morph_id_sx : (A,B:Cat; F:(Functor A B))
(morph_comp (morph_id B) F)==F.
Proof.
Intros; Apply functor_extens.
Unfold morph_comp morph_id eq_fct; Simpl; Intros.
Apply eq_mor_refl.
Qed.
Lemma morph_id_dx : (A,B:Cat; F:(Functor A B))
(morph_comp F (morph_id A))==F.
Proof.
Intros; Apply functor_extens.
Unfold morph_comp morph_id eq_fct; Simpl; Intros.
Apply eq_mor_refl.
Qed.
Section Embedding.
Variable A,B:Cat; F:(Functor A B).
Definition embedding : Type := (x,y:A)
(inverse [f:(mor x y)](fct F f)).
End Embedding.
Dual Category |
Section Dual_Cat.
Variable A:Cat.
Local dual_mor [x,y:A] : Type := (mor y x).
Local B := (Build_Cat_Data
[x,y,z:A; g:(dual_mor y z); f:(dual_mor x y)] (oo f g)
[x:A](ii x)).
Definition Dual_Cat : Cat.
Proof.
Split with B;
Abstract Simpl; Unfold dual_mor; Split; Auto.
Defined.
End Dual_Cat.
End Cat_.
Module Type A_Cat_.
Variable A:Cat_.Obj.
End A_Cat_.