Library CatSem.CAT.subcategories

Require Export CatSem.CAT.functor.
Require Export CatSem.CAT.functor_properties.

Set Implicit Arguments.
Unset Strict Implicit.

Unset Automatic Introduction.

Section SubCat_def.

Variable ob: Type.
Variable mor: ob -> ob -> Type.
Variable C: Cat_struct mor.

Section SubCat_struct.

Variable subobP: ob -> Prop.

Definition subob:= {a:ob | subobP a}.

Definition SC_inj_ob (a: subob): ob := proj1_sig a.
Coercion SC_inj_ob : subob >-> ob.

Variable submorP: forall a b: ob, mor a b -> Prop.

Definition submor (a b: ob) := {f : mor a b | submorP f}.


Definition SC_inj_mor (a b: ob) (f: submor a b) :=
                   proj1_sig f.
Coercion SC_inj_mor: submor >-> mor.

Class SubCat_compat := {
  
  sub_id: forall a: subob, submorP (id (proj1_sig a));
  sub_comp: forall (a b c:ob) (f: mor a b) (g: mor b c),
                   submorP f -> submorP g -> submorP (f ;; g)
}.


Hypothesis SC: SubCat_compat.



Lemma submor_equiv (a b: ob) : @Equivalence (submor a b)
           (fun f g => proj1_sig f == proj1_sig g).
Proof.
  intros a b.
  split.
  unfold Reflexive.
  intro x; simpl.
  apply hom_refl.

  unfold Symmetric;
  intros x y; simpl;
  apply hom_sym.

  unfold Transitive;
  intros x y z; simpl;
  apply hom_trans.
Qed.

Definition submor_setoid (a b: ob) := Build_Setoid (submor_equiv a b).


Program Definition subid (a: subob) : submor a a :=
  exist _ (id (proj1_sig a)) _ .
Next Obligation.
Proof.
  apply sub_id.
Qed.

Program Definition subcomp (a b c: subob)(f: submor a b) (g: submor b c):
                submor a c :=
        exist _ (f ;; g) _ .
Next Obligation.
Proof.
  destruct f;
  destruct g;
  apply sub_comp;
  auto.
Qed.

Obligation Tactic := cat; try apply assoc.

Program Instance SubCat_struct: Cat_struct (obj := subob) submor := {
  mor_oid a b := submor_setoid a b;
  comp a b c f g := subcomp f g;
  id a := subid a
}.
Next Obligation.
Proof.
  unfold Proper.
  do 2 red.
  unfold subcomp;
  simpl.
  intros x y H x0 y0 H0.
  rewrite H; rewrite H0.
  apply hom_refl.
Qed.

Definition SubCat := Build_Cat SubCat_struct.

End SubCat_struct.


End SubCat_def.

Section Injection_Functor.

Variable ob: Type.
Variable mor: ob -> ob -> Type.
Variable C: Cat_struct mor.

Variable subobP : ob -> Prop.
Variable submorP : forall a b, mor a b -> Prop.
Variable SC: SubCat_compat C subobP submorP.

Program Definition FINJ : Functor (SubCat_struct SC) C := Build_Functor
  (Fobj := fun a => proj1_sig a)
  (Fmor := fun a b f => proj1_sig f) _ .
Next Obligation.
Proof.
  apply Build_Functor_struct.

  intros a b;
  unfold Proper. red.
  auto.

  cat.
  cat.
Qed.

Program Instance FINJ_Faithful : Faithful FINJ.

End Injection_Functor.