Require Export cat_.
Require Export universal_.
Implicit Arguments On.
Category over an object |
Module Cat_Over_.
Export Cat_.
Export Universal_.
Section Cat_Over.
Variable A:Cat; u:A.
Inductive obj_over : Type :=
| obj_over_intro : (x:A; f:(mor x u)) obj_over.
Definition obj_of_obj_over [a:obj_over] : A.
Proof.
NewDestruct 1; Exact x.
Defined.
Definition mor_of_obj_over [a:obj_over] : (mor (obj_of_obj_over a) u).
Proof.
NewDestruct a; Exact f.
Defined.
Inductive mor_over [x,y:obj_over] : Type :=
| mor_over_intro : (f:(mor (obj_of_obj_over x) (obj_of_obj_over y)))
(oo (mor_of_obj_over y) f)==(mor_of_obj_over x) -> (mor_over x y).
Definition mor_of_mor_over [x,y:obj_over; f:(mor_over x y)] :
(mor (obj_of_obj_over x) (obj_of_obj_over y)).
Proof.
NewDestruct 1; Exact f.
Defined.
Lemma mor_over_extens : (x,y:obj_over; f,g:(mor_over x y))
(mor_of_mor_over f)==(mor_of_mor_over g) -> f==g.
Proof.
NewDestruct f; NewDestruct g; Simpl; NewDestruct 1.
Assert E : e==e0.
Apply proof_irrelevance.
NewDestruct E.
Reflexivity.
Qed.
Definition oo_over [
x,y,z:obj_over; g:(mor_over y z); f:(mor_over x y)
] : (mor_over x z).
Proof.
NewDestruct 1; NewDestruct 1; Intros.
Split with (oo f f0).
Abstract Rewrite oo_assoc; Rewrite e; Assumption.
Defined.
Definition ii_over [x:obj_over] : (mor_over x x).
Proof.
NewDestruct x; Split with (ii x); Trivial.
Defined.
Remark cat_over_theory : (Cat_Theory oo_over ii_over).
Proof.
Unfold oo_over ii_over; Split; Simpl; Intros.
NewDestruct h; NewDestruct g; NewDestruct f.
Apply mor_over_extens; Simpl.
Rewrite oo_assoc; Auto.
NewDestruct x; NewDestruct y; NewDestruct f.
Apply mor_over_extens; Simpl; Auto.
NewDestruct x; NewDestruct y; NewDestruct f.
Apply mor_over_extens; Simpl; Auto.
Qed.
Local cat_over_data : Cat_Data.
Proof.
Split with obj_over mor_over.
Exact oo_over.
Exact ii_over.
Defined.
Definition cat_over : Cat.
Proof.
Split with cat_over_data.
Exact cat_over_theory.
Defined.
Definition make_over [x:A; f:(mor x u)] : cat_over.
Proof.
Intros; Split with x; Exact f.
Defined.
Section Base.
Local F_obj : (v:cat_over) A.
Proof.
NewDestruct 1.
Exact x.
Defined.
Local F_data : (Functor_Data cat_over A).
Proof.
Split with F_obj.
NewDestruct 1.
Exact f.
Defined.
Remark F_theory : (Functor_Theory (fct F_data)).
Proof.
Split; Simpl.
NewDestruct x; Rename f into hx.
NewDestruct y; Rename x0 into y; Rename f into hy.
NewDestruct z; Rename x0 into z; Rename f into hz.
Simpl.
NewDestruct g; Rename f into g.
NewDestruct f.
Simpl.
Reflexivity.
NewDestruct x; Reflexivity.
Qed.
Definition base : (Functor cat_over A).
Proof.
Split with F_data.
Exact F_theory.
Defined.
End Base.
Section Final_Over.
Local final_data : (v:cat_over) (mor v (make_over (ii u))).
Proof.
NewDestruct v.
Split with f.
Abstract Simpl; Auto.
Defined.
Remark final_theory : (Final_Theory final_data).
Proof.
Unfold Final_Theory.
NewDestruct x.
NewDestruct f0.
Simpl in f0; Simpl in e.
Assert f==f0.
Rewrite <- e; Auto.
NewDestruct H.
Simpl.
Assert (final_data_subproof f)==e.
Apply proof_irrelevance.
NewDestruct H.
Reflexivity.
Qed.
Definition final_over : (Final cat_over).
Proof.
Split with (make_over (ii u)) final_data.
Exact final_theory.
Defined.
End Final_Over.
End Cat_Over.
Section Cat_Under.
Variable A:Cat; u:A.
Definition cat_under : Cat := (!cat_over (Dual_Cat A) u).
Definition make_under [x:A; f:(mor u x)] : cat_under.
Proof.
Intros; Split with x; Simpl; Exact f.
Defined.
End Cat_Under.
End Cat_Over_.