Library DiscreteCategoryFunctors


Require Import Utf8.
Require Import FunctionalExtensionality.
Require Export Category DiscreteCategory.
Require Import Functor SetCategory ComputableCategory.

Set Implicit Arguments.

Generalizable All Variables.

Discrete Category Functors

Section FunctorFromDiscrete.
  Variable O : Type.
  Context `(D : @Category objD).
  Variable objOf : OobjD.

  Let FunctorFromDiscrete_MorphismOf s d (m : Morphism (DiscreteCategory O) s d)
  : Morphism D (objOf s) (objOf d)
    := match m with
         | eq_reflIdentity _
       end.

  Definition FunctorFromDiscrete : Functor (DiscreteCategory O) D.
  Proof.
    refine {| ObjectOf := objOf; MorphismOf := FunctorFromDiscrete_MorphismOf |};
    abstract (
        intros; hnf in *; subst; simpl;
        auto with category
      ).
  Defined.
End FunctorFromDiscrete.

Notation ObjectFunctorTo Index2Object Index2Cat Sets :=
  ((Build_Functor (@ComputableCategory _ _ Index2Cat) (CategoryOf Sets)
                  (fun C'Index2Object C')
                  (fun _ _ FObjectOf F)
                  (fun _ _ _ _ _eq_refl)
                  (fun _eq_refl))).

Section Obj.
  Definition ObjectFunctor I (Index2Object : IType)
             `(Index2Cat : i : I, @Category (@Index2Object i))
  : Functor _ CategoryOfTypes
    := ObjectFunctorTo Index2Object Index2Cat Type.
  Definition ObjectFunctorToSet I (Index2Object : ISet)
             `(Index2Cat : i : I, @Category (@Index2Object i))
  : Functor _ CategoryOfSets
    := ObjectFunctorTo Index2Object Index2Cat Set.
  Definition ObjectFunctorToProp I (Index2Object : IProp)
             `(Index2Cat : i : I, @Category (@Index2Object i))
  : Functor _ CategoryOfProps
    := ObjectFunctorTo Index2Object Index2Cat Prop.
End Obj.

Arguments ObjectFunctor {I Index2Object Index2Cat}.
Arguments ObjectFunctorToSet {I Index2Object Index2Cat}.
Arguments ObjectFunctorToProp {I Index2Object Index2Cat}.

Section InducedFunctor.
  Variable O : Type.
  Context `(O' : @Category obj).
  Variable f : OO'.

  Definition InducedDiscreteFunctor : Functor (DiscreteCategory O) O'.
    match goal with
      | [ |- Functor ?C ?D ] ⇒
        refine (Build_Functor C D
                              f
                              (fun s d m
                                 match m with eq_reflIdentity (f s) end)
                              _
                              _
               )
    end;
    abstract (
        intros; simpl in *; repeat subst; trivial;
        repeat rewrite RightIdentity; repeat rewrite LeftIdentity;
        repeat rewrite Associativity;
        reflexivity
      ).
  Defined.
End InducedFunctor.

Section disc.
  Local Ltac t := functor_eq;
                  subst;
                  auto.

  Definition DiscreteFunctor : Functor CategoryOfTypes CategoryOfCategories.
    refine (Build_Functor CategoryOfTypes CategoryOfCategories
                          (fun OexistT _ _ (DiscreteCategory O))
                          (fun s d fInducedDiscreteFunctor _ f)
                          _
                          _
           );
    abstract t.
  Defined.

  Definition DiscreteSetFunctor : Functor CategoryOfSets CategoryOfCategories.
    refine (Build_Functor CategoryOfSets CategoryOfCategories
                          (fun OexistT _ _ (DiscreteCategory O))
                          (fun s d fInducedDiscreteFunctor _ f)
                          _
                          _
           );
    abstract t.
  Defined.
End disc.

Section DiscreteAdjoints.
  Lemma DiscreteObjectIdentity : ComposeFunctors ObjectFunctor DiscreteFunctor = IdentityFunctor _.
    functor_eq.
  Qed.
End DiscreteAdjoints.