Library SetCategoryFacts


Require Import Utf8.
Require Import FunctionalExtensionality.
Require Export Category SetCategory Product Coproduct.
Require Import DiscreteCategory CategoryMorphisms CategoryObjects.
Require Import Common Morphism.

Set Implicit Arguments.

Generalizable All Variables.

Initial and terminal objects of the category of sets.

We use notations to get around universe level instantiation again.
Notation IndexedTInitialOf obj coerce initial_obj :=
  ((fun zexist _
                   (fun x : initial_obj%typematch x with end)
                   (fun _functional_extensionality_dep _ _ (fun x : initial_obj%typematch x with end)))
   : IsInitialObject (C := IndexedCategoryOf obj coerce) initial_obj%type).

Notation IndexedTTerminalOf obj coerce terminal_obj constr all_eq :=
  ((fun z : objexist (fun m : zterminal_obj x : zterminal_obj, x = m)
                         (fun _ : zconstr)
                         (fun H : zterminal_objfunctional_extensionality_dep H
                                                                                     (fun _ : zconstr)
                                                                                     (fun x : zall_eq _ _)))
   : IsTerminalObject (C := IndexedCategoryOf obj coerce) terminal_obj%type).

Notation IndexedEmptySetInitialOf obj coerce := (IndexedTInitialOf obj coerce ).
Notation IndexedFalseInitialOf obj coerce := (IndexedTInitialOf obj coerce False).

Notation IndexedUnitTerminalOf obj coerce := (IndexedTTerminalOf obj coerce unit tt unit_eq).
Notation IndexedTrueTerminalOf obj coerce := (IndexedTTerminalOf obj coerce True I True_eq).

Notation EmptySetInitialOf obj := (IndexedEmptySetInitialOf obj (fun xx)).
Notation FalseInitialOf obj := (IndexedFalseInitialOf obj (fun xx)).

Notation UnitTerminalOf obj := (IndexedUnitTerminalOf obj (fun xx)).
Notation TrueTerminalOf obj := (IndexedTrueTerminalOf obj (fun xx)).

Notation CoercedEmptySetInitialOf obj T := (IndexedEmptySetInitialOf obj (fun xx : T)).
Notation CoercedFalseInitialOf obj T := (IndexedFalseInitialOf obj (fun xx : T)).

Notation CoercedUnitTerminalOf obj T := (IndexedUnitTerminalOf obj (fun xx : T)).
Notation CoercedTrueTerminalOf obj T := (IndexedTrueTerminalOf obj (fun xx : T)).

Section InitialTerminal.
  Definition CategoryOfTypesFalseInitial : IsInitialObject (C := CategoryOfTypes) False := Eval simpl in FalseInitialOf Type.
  Definition CategoryOfSetsFalseInitial : IsInitialObject (C := CategoryOfSets) False := Eval simpl in FalseInitialOf Set.
  Definition CategoryOfPropsFalseInitial : IsInitialObject (C := CategoryOfProps) False := Eval simpl in FalseInitialOf Prop.

  Definition CategoryOfTypesEmptyInitial : IsInitialObject (C := CategoryOfTypes) := Eval simpl in EmptySetInitialOf Type.
  Definition CategoryOfSetsEmptyInitial : IsInitialObject (C := CategoryOfSets) := Eval simpl in EmptySetInitialOf Set.

  Definition CategoryOfTypesTrueTerminal : IsTerminalObject (C := CategoryOfTypes) True := Eval simpl in TrueTerminalOf Type.
  Definition CategoryOfSetsTrueTerminal : IsTerminalObject (C := CategoryOfSets) True := Eval simpl in TrueTerminalOf Set.
  Definition CategoryOfPropsTrueTerminal : IsTerminalObject (C := CategoryOfProps) True := Eval simpl in TrueTerminalOf Prop.

  Definition CategoryOfTypesUnitTerminal : IsTerminalObject (C := CategoryOfTypes) unit := Eval simpl in UnitTerminalOf Type.
  Definition CategoryOfSetsUnitTerminal : IsTerminalObject (C := CategoryOfSets) unit := Eval simpl in UnitTerminalOf Set.

  Definition CategoryOfTypesSingletonTerminal : IsTerminalObject (C := CategoryOfTypes) unit := Eval hnf in CategoryOfTypesUnitTerminal.
  Definition CategoryOfSetsSingletonTerminal : IsTerminalObject (C := CategoryOfSets) unit := Eval hnf in CategoryOfSetsUnitTerminal.
End InitialTerminal.

Section EpiMono.
  Variables S : Type.

  Local Ltac t' :=
    match goal with
      | _progress (intros; subst; trivial)
      | _eexists; reflexivity
      | _discriminate
      | [ H : _False |- _ ] ⇒ contradict H; solve [ t' ]
      | [ H : ¬_ |- _ ] ⇒ contradict H; solve [ t' ]
      | [ dec : _, {_} + {_} |- _ ] ⇒
        match goal with
          | [ _ : appcontext[dec ?x] |- _ ] ⇒ destruct (dec x)
          | [ |- appcontext[dec ?x] ] ⇒ destruct (dec x)
        end
      | _apply functional_extensionality_dep; intro
      | _progress (unfold compose in *; simpl in *; fg_equal)
      | _progress apply_hyp'
      | _progress destruct_type bool
      | [ H : (_ _, _), x : _ |- _ ] ⇒ destruct (H x); clear H
      | _progress specialize_uniquely
    end.

  Local Ltac t :=
    repeat match goal with
             | _t'
             | [ H : ?A_ |- _ ] ⇒
               match goal with
                 | [ _ : A |- _ ] ⇒ fail 1
                 | _let a := fresh in assert (a : A) by (repeat t'); specialize (H a)
               end
           end.

  Lemma InjMono B (f : BS) :
    ( x y : B, f x = f yx = y)
    → ( A (g g' : AB), (compose f g) = (compose f g')g = g').
  Proof.
    t.
  Qed.

  Lemma MonoInj B (f : BS) :
    ( A (g g' : AB), (compose f g) = (compose f g')g = g')
    → ( x y : B, f x = f yx = y).
  Proof.
    intros H x y; t.
    pose proof (fun H'H bool (fun bif b then x else y) (fun _y) H' true).
    t.
  Qed.

  Lemma SurjEpi A (f : AS) :
    ( x : S, y : A, f y = x)
    → ( C (g g' : SC), (compose g f) = (compose g' f)g = g').
  Proof.
    t.
  Qed.

  Lemma EpiSurj A (f : AS) (member_dec : x : S, { y, f y = x} + {¬ y, f y = x}) :
    ( C (g g' : SC), (compose g f) = (compose g' f)g = g')
    → ( x : S, y : A, f y = x).
  Proof.
    intro H.
    assert (H' := fun H'H bool (fun yif member_dec y then true else false) (fun ytrue) H').
    clear H.
    t.
  Qed.
End EpiMono.

Section set_cat_has_prod.
  Local Ltac prod_t :=
    repeat match goal with
             | _apply functional_extensionality_dep
             | _progress intros []
             | _intro
             | _progress simpl_eq
             | _progress fg_equal
             | _progress intuition
             | [ |- @eq (_ _) (?f ?x) _ ] ⇒ destruct (f x)
           end.

  Global Instance prodT_is_product X Y : is_product CategoryOfTypes X Y (X × Y)%type.
  refine (@Build_is_product _ _
                            X Y (X × Y)%type
                            (@fst _ _)
                            (@snd _ _)
                            (fun A f gfun x(f x, g x))
                            _
                            _
                            _);
    simpl; try reflexivity;
    abstract prod_t.
  Defined.

  Global Instance prod_is_product X Y : is_product CategoryOfSets X Y (X × Y)%type.
  refine (@Build_is_product _ _
                            X Y (X × Y)%type
                            (@fst _ _)
                            (@snd _ _)
                            (fun A f gfun x(f x, g x))
                            _
                            _
                            _);
    simpl; try reflexivity;
    abstract prod_t.
  Defined.

  Global Instance conj_is_product X Y : is_product CategoryOfProps X Y (X Y).
  refine (@Build_is_product _ _
                            X Y (X Y)
                            (fun Hmatch H with conj A _A end)
                            (fun Hmatch H with conj _ AA end)
                            (fun A f gfun xconj (f x) (g x))
                            _
                            _
                            _);
    simpl; try reflexivity;
    abstract prod_t.
  Defined.
End set_cat_has_prod.

Section set_cat_has_coprod.
  Local Ltac coprod_t :=
    repeat match goal with
             | _apply functional_extensionality_dep
             | _progress intros []
             | _intro
             | _progress simpl_eq
             | _progress fg_equal
             | _progress intuition
             | [ |- @eq (_ _) (?f ?x) _ ] ⇒ destruct (f x)
           end.

  Global Instance sumT_is_coproduct X Y : is_coproduct CategoryOfTypes X Y (X + Y)%type.
  refine (@Build_is_coproduct _ _
                            X Y (X + Y)%type
                            (@inl _ _)
                            (@inr _ _)
                            (fun A f gfun xmatch x with inl xf x | inr xg x end)
                            _
                            _
                            _);
    simpl; try reflexivity;
    abstract coprod_t.
  Defined.

  Global Instance sum_is_coproduct X Y : is_coproduct CategoryOfSets X Y (X + Y)%type.
  refine (@Build_is_coproduct _ _
                            X Y (X + Y)%type
                            (@inl _ _)
                            (@inr _ _)
                            (fun A f gfun xmatch x with inl xf x | inr xg x end)
                            _
                            _
                            _);
    simpl; try reflexivity;
    abstract coprod_t.
  Defined.

  Global Instance or_is_coproduct X Y : is_coproduct CategoryOfProps X Y (X Y).
  refine (@Build_is_coproduct _ _
                            X Y (X Y)
                            (@or_introl _ _)
                            (@or_intror _ _)
                            (fun A f gfun xmatch x with or_introl xf x | or_intror xg x end)
                            _
                            _
                            _);
    simpl; try reflexivity;
    abstract coprod_t.
  Defined.
End set_cat_has_coprod.