Library Category


Require Import Utf8.
Require Import JMeq.
Require Export Notations.
Require Import Common.

Set Implicit Arguments.

Generalizable All Variables.

Categories

We include the object type as a parameter, because, otherwise, we can't make a category of categories easily.
Record Category {obj : Type} :=
  {
    Object :> _ := obj;
    Morphism : objobjType;

    Identity : x, Morphism x x;
    Compose : s d d', Morphism d d'Morphism s dMorphism s d';
    Associativity : o1 o2 o3 o4
                           (m1 : Morphism o1 o2)
                           (m2 : Morphism o2 o3)
                           (m3 : Morphism o3 o4),
                      Compose (Compose m3 m2) m1 = Compose m3 (Compose m2 m1);
    LeftIdentity : a b (f : Morphism a b), Compose (Identity b) f = f;
    RightIdentity : a b (f : Morphism a b), Compose f (Identity a) = f
  }.

Delimit Scope category_scope with category.
Delimit Scope object_scope with object.
Delimit Scope morphism_scope with morphism.

Bind Scope category_scope with Category.
Bind Scope object_scope with Object.
Bind Scope morphism_scope with Morphism.

Arguments Object {obj%type} C%category : rename.
Arguments Morphism {obj%type} C%category s%object d%object : rename.
Arguments Identity {obj%type} [C%category] x%object : rename.
Arguments Compose {obj%type} [C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.

Infix "○" := (@Compose _ _ _ _ _) : morphism_scope.
Infix "~>" := (@Morphism _ _) : category_scope.
Infix "~>" := (@Morphism _ _) : type_scope.
Create HintDb category discriminated.
Create HintDb morphism discriminated.

Hint Resolve @LeftIdentity @RightIdentity @Associativity : category.
Hint Resolve @LeftIdentity @RightIdentity @Associativity : morphism.
Hint Rewrite @LeftIdentity @RightIdentity : category.
Hint Rewrite @LeftIdentity @RightIdentity : morphism.

We create aliases for categories, calling them small and locally small in accordance with mathematical terminology.
Definition LocallySmallCategory {obj : Type} := @Category obj.
Definition SmallCategory {obj : Set} := @Category obj.
Identity Coercion LocallySmallCategory_Category_Id
: LocallySmallCategory >-> Category.
Identity Coercion SmallCategory_LocallySmallCategory_Id
: SmallCategory >-> Category.

Version of Associativity that avoids going off into the weeds in the presence of unification variables

Local Open Scope morphism_scope.

Definition NoEvar T (_ : T) := True.

Lemma AssociativityNoEvar `(C : @Category obj) : (o1 o2 o3 o4 : C) (m1 : C.(Morphism) o1 o2)
  (m2 : C.(Morphism) o2 o3) (m3 : C.(Morphism) o3 o4),
  NoEvar (m1, m2) NoEvar (m2, m3) NoEvar (m1, m3)
  → (m3 m2) m1 = m3 (m2 m1).
  intros; apply Associativity.
Qed.

Ltac noEvar := match goal with
                 | [ |- context[NoEvar ?X] ] ⇒ (has_evar X; fail 1)
                                                  || cut (NoEvar X); [ intro; tauto | constructor ]
               end.

Hint Rewrite @AssociativityNoEvar using noEvar : category.
Hint Rewrite @AssociativityNoEvar using noEvar : morphism.

Ltac try_associativity_quick tac := try_rewrite Associativity tac.
Ltac try_associativity tac := try_rewrite_by AssociativityNoEvar ltac:(idtac; noEvar) tac.

Ltac find_composition_to_identity :=
  match goal with
    | [ H : @Compose _ _ _ _ _ ?a ?b = @Identity _ _ _ |- context[@Compose ?A ?B ?C ?D ?E ?c ?d] ]
      ⇒ let H' := fresh in
        assert (H' : b = d a = c) by (split; reflexivity); clear H';
          assert (H' : @Compose A B C D E c d = @Identity _ _ _) by (
            exact H ||
              (unfold Object; simpl in H |- *; exact H || (rewrite H; reflexivity))
          );
          first [
            rewrite H'
            | simpl in H' |- *; rewrite H'
            | let H'T := type of H' in fail 2 "error in rewriting a found identity" H "[" H'T "]"
          ]; clear H'
  end.