Library CategoryObjects


Require Import Utf8.
Require Import ProofIrrelevance FunctionalExtensionality.
Require Import JMeq.
Require Export Category CategoryIsomorphisms.
Require Import Common Notations.

Set Implicit Arguments.

Generalizable All Variables.

Category Objects


Section CategoryObjects1.
  Context `(C : @Category obj).

  Definition UniqueUpToUniqueIsomorphism' (P : C.(Object) → Prop) : Prop :=
     x, P x x', P x' m : C.(Morphism) x x', IsIsomorphism m is_unique m.

  Definition UniqueUpToUniqueIsomorphism (P : C.(Object) → Type) :=
     x, P x x', P x'{ m : C.(Morphism) x x' | IsIsomorphism m & is_unique m }.

  Section terminal.
    Definition IsTerminalObject' (x : C) : Prop :=
       x', ! m : C.(Morphism) x' x, True.

    Definition IsTerminalObject (x : C) :=
       x', { m : C.(Morphism) x' x | is_unique m }.

    Record TerminalObject :=
      {
        TerminalObject_Object' : obj;
        TerminalObject_Morphism : x, Morphism C x TerminalObject_Object';
        TerminalObject_Property : x, is_unique (TerminalObject_Morphism x)
      }.

    Definition TerminalObject_Object : TerminalObjectC := TerminalObject_Object'.

    Global Coercion TerminalObject_Object : TerminalObject >-> Object.

    Definition TerminalObject_IsTerminalObject (x : TerminalObject) : IsTerminalObject x
      := fun x'exist _ (TerminalObject_Morphism x x') (TerminalObject_Property x x').

    Definition IsTerminalObject_TerminalObject x : IsTerminalObject xTerminalObject
      := fun H ⇒ @Build_TerminalObject x (fun o'proj1_sig (H o')) (fun o'proj2_sig (H o')).

    Global Coercion TerminalObject_IsTerminalObject : TerminalObject >-> IsTerminalObject.
    Global Coercion IsTerminalObject_TerminalObject : IsTerminalObject >-> TerminalObject.
  End terminal.

  Section initial.
    Definition IsInitialObject' (x : C) : Prop :=
       x', ! m : C.(Morphism) x x', True.

    Definition IsInitialObject (x : C) :=
       x', { m : C.(Morphism) x x' | is_unique m }.

    Record InitialObject :=
      {
        InitialObject_Object' :> obj;
        InitialObject_Morphism : x, Morphism C InitialObject_Object' x;
        InitialObject_Property : x, is_unique (InitialObject_Morphism x)
      }.

    Definition InitialObject_Object : InitialObjectC := InitialObject_Object'.

    Global Coercion InitialObject_Object : InitialObject >-> Object.

    Definition InitialObject_IsInitialObject (x : InitialObject) : IsInitialObject x
      := fun x'exist _ (InitialObject_Morphism x x') (InitialObject_Property x x').

    Definition IsInitialObject_InitialObject x : IsInitialObject xInitialObject
      := fun H ⇒ @Build_InitialObject x (fun x'proj1_sig (H x')) (fun x'proj2_sig (H x')).

    Global Coercion InitialObject_IsInitialObject : InitialObject >-> IsInitialObject.
    Global Coercion IsInitialObject_InitialObject : IsInitialObject >-> InitialObject.
  End initial.
End CategoryObjects1.

Arguments UniqueUpToUniqueIsomorphism {_ C} P.
Arguments IsInitialObject' {_ C} x.
Arguments IsInitialObject {_ C} x.
Arguments IsTerminalObject' {_ C} x.
Arguments IsTerminalObject {_ C} x.

Section CategoryObjects2.
  Context `(C : @Category obj).

  Ltac unique := hnf; intros; specialize_all_ways; destruct_sig;
    unfold is_unique, unique, uniqueness in *;
      repeat (destruct 1);
      repeat match goal with
               | [ x : _ |- _ ] ⇒ x
             end; eauto with category; try split; try solve [ etransitivity; eauto with category ].

  Theorem TerminalObjectUnique : UniqueUpToUniqueIsomorphism (IsTerminalObject (C := C)).
    unique.
  Qed.

  Theorem InitialObjectUnique : UniqueUpToUniqueIsomorphism (IsInitialObject (C := C)).
    unique.
  Qed.
End CategoryObjects2.