Library Subcategory


Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Export Category Functor.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

Subcategories


Local Ltac faithful_t :=
  repeat (unfold Object in *; simpl in *;
          match goal with
            | _intro
            | _progress trivial
            | [ |- _ = _ ] ⇒ (apply functional_extensionality_dep; intro)
            | _progress simpl_eq
            | [ H : _ = _ |- _ ] ⇒ fg_equal_in H
          end).

Section sig_obj_mor.
  Context `(A : @Category objA).
  Variable Pobj : objAProp.
  Variable Pmor : s d : sig Pobj, A.(Morphism) (proj1_sig s) (proj1_sig d) → Prop.
  Variable Pidentity : x, @Pmor x x (Identity (C := A) _).
  Variable Pcompose : s d d',
                       m1 m2,
                        @Pmor d d' m1
                        → @Pmor s d m2
                        → @Pmor s d' (Compose (C := A) m1 m2).

  Definition Category_sig : @Category (sig Pobj).
    match goal with
      | [ |- @Category ?obj ] ⇒
        refine (@Build_Category obj
                                (fun s dsig (@Pmor s d))
                                (fun xexist _ _ (Pidentity x))
                                (fun s d d' m1 m2exist _ _ (Pcompose (proj2_sig m1)
                                                                         (proj2_sig m2)))
                                _
                                _
                                _
               )
    end;
    abstract (intros; simpl_eq; auto with category).
  Defined.

  Definition proj1_sig_functor : Functor Category_sig A
    := Build_Functor Category_sig A
                     (@proj1_sig _ _)
                     (fun s d ⇒ @proj1_sig _ _)
                     (fun _ _ _ _ _eq_refl)
                     (fun _eq_refl).
End sig_obj_mor.

Arguments proj1_sig_functor {objA A Pobj Pmor Pidentity Pcompose}.

Section sig_obj.
  Context `(A : @Category objA).
  Variable Pobj : objAProp.

  Definition Category_sig_obj : @Category (sig Pobj).
    match goal with
      | [ |- @Category ?obj ] ⇒
        refine (@Build_Category obj
                                (fun s dA.(Morphism) (proj1_sig s)
                                                         (proj1_sig d))
                                (fun xIdentity (C := A) (proj1_sig x))
                                (fun s d d' m1 m2Compose (C := A) m1 m2)
                                _
                                _
                                _
               )
    end;
    abstract (intros; destruct_sig; simpl; auto with category).
  Defined.

  Definition proj1_sig_obj_functor : Functor Category_sig_obj A
    := Build_Functor Category_sig_obj A
                     (@proj1_sig _ _)
                     (fun s d mm)
                     (fun _ _ _ _ _eq_refl)
                     (fun _eq_refl).

  Definition Category_sig_obj_as_sig : @Category (sig Pobj)
    := @Category_sig _ A Pobj
                     (fun _ _ _True)
                     (fun _I)
                     (fun _ _ _ _ _ _ _I).

  Definition sig_functor_obj : Functor Category_sig_obj_as_sig Category_sig_obj
    := Build_Functor Category_sig_obj_as_sig Category_sig_obj
                     (fun xx)
                     (fun _ _ ⇒ @proj1_sig _ _)
                     (fun _ _ _ _ _eq_refl)
                     (fun _eq_refl).

  Definition sig_functor_obj_inv : Functor Category_sig_obj Category_sig_obj_as_sig
    := Build_Functor Category_sig_obj Category_sig_obj_as_sig
                     (fun xx)
                     (fun _ _ mexist _ m I)
                     (fun _ _ _ _ _eq_refl)
                     (fun _eq_refl).

  Lemma sig_obj_eq
  : ComposeFunctors sig_functor_obj sig_functor_obj_inv
    = IdentityFunctor _
     ComposeFunctors sig_functor_obj_inv sig_functor_obj
       = IdentityFunctor _.
    split; functor_eq; destruct_sig; destruct_head True; reflexivity.
  Qed.

  Lemma sig_obj_compat
  : ComposeFunctors proj1_sig_obj_functor sig_functor_obj
    = proj1_sig_functor.
    functor_eq.
  Qed.
End sig_obj.

Arguments proj1_sig_obj_functor {objA A Pobj}.

Section sig_mor.
  Context `(A : @Category objA).
  Variable Pmor : s d, A.(Morphism) s dProp.

  Variable Pidentity : x, @Pmor x x (Identity (C := A) _).
  Variable Pcompose : s d d',
                       m1 m2,
                        @Pmor d d' m1
                        → @Pmor s d m2
                        → @Pmor s d' (Compose (C := A) m1 m2).

  Definition Category_sig_mor : @Category objA.
    match goal with
      | [ |- @Category ?obj ] ⇒
        refine (@Build_Category obj
                                (fun s dsig (@Pmor s d))
                                (fun xexist _ (Identity (C := A) x) (Pidentity x))
                                (fun s d d' m1 m2
                                   exist _
                                         (Compose (proj1_sig m1) (proj1_sig m2))
                                         (Pcompose (proj2_sig m1) (proj2_sig m2)))
                                _
                                _
                                _
               )
    end;
    abstract (intros; simpl_eq; auto with category).
  Defined.

  Definition proj1_sig_mor_functor : Functor Category_sig_mor A
    := Build_Functor Category_sig_mor A
                     (fun xx)
                     (fun s d ⇒ @proj1_sig _ _)
                     (fun _ _ _ _ _eq_refl)
                     (fun _eq_refl).

  Definition Category_sig_mor_as_sig : @Category (sig (fun _ : objATrue))
    := @Category_sig _ A _
                     (fun s d ⇒ @Pmor (proj1_sig s) (proj1_sig d))
                     (fun _Pidentity _)
                     (fun _ _ _ _ _ m1 m2Pcompose m1 m2).

  Definition sig_functor_mor : Functor Category_sig_mor_as_sig Category_sig_mor
    := Build_Functor Category_sig_mor_as_sig Category_sig_mor
                     (@proj1_sig _ _)
                     (fun _ _ mm)
                     (fun _ _ _ _ _eq_refl)
                     (fun _eq_refl).

  Definition sig_functor_mor_inv : Functor Category_sig_mor Category_sig_mor_as_sig
    := Build_Functor Category_sig_mor Category_sig_mor_as_sig
                     (fun xexist _ x I)
                     (fun _ _ mm)
                     (fun _ _ _ _ _eq_refl)
                     (fun _eq_refl).

  Lemma sig_mor_eq
  : ComposeFunctors sig_functor_mor sig_functor_mor_inv = IdentityFunctor _
     ComposeFunctors sig_functor_mor_inv sig_functor_mor = IdentityFunctor _.
    split; apply Functor_Eq; repeat intro; destruct_sig; destruct_head True;
    subst_eq_refl_in_match;
    reflexivity.
  Qed.

  Lemma sig_mor_compat
  : ComposeFunctors proj1_sig_mor_functor sig_functor_mor = proj1_sig_functor.
    functor_eq.
  Qed.
End sig_mor.

Arguments proj1_sig_mor_functor {objA A Pmor Pidentity Pcompose}.

Definition Subcategory := @Category_sig.
Definition SubcategoryInclusionFunctor := @proj1_sig_functor.
Definition FullSubcategory := @Category_sig_obj.
Definition FullSubcategoryInclusionFunctor := @proj1_sig_obj_functor.
Definition WideSubcategory := @Category_sig_mor.
Definition WideSubcategoryInclusionFunctor := @proj1_sig_mor_functor.