Library HoTT.categories.Category.Core

Definition of a PreCategory

Require Export Overture.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

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

Local Open Scope morphism_scope.

Quoting the HoTT Book: Definition 9.1.1. A precategory A consists of the following.
(i) A type A₀ of objects. We write a : A for a : A₀.
(ii) For each a, b : A, a set hom_A(a, b) of arrows or morphisms.
(iii) For each a : A, a morphism 1ₐ : hom_A(a, a).
(iv) For each a, b, c : A, a function
hom_A(b, c) hom_A(a, b) hom_A(a, c)
denoted infix by g f g f , or sometimes simply by g f.
(v) For each a, b : A and f : hom_A(a, b), we have f = 1_b f and f = f 1ₐ.
(vi) For each a, b, c, d : A and f : hom_A(a, b), g : hom_A(b, c), h : hom_A(c,d), we have h (g f) = (h g) f. In addition to these laws, we ask for a few redundant laws to give us more judgmental equalities. For example, since (p^)^ p for paths p, we ask for the symmetrized version of the associativity law, so we can swap them when we take the dual.

Record PreCategory :=
  Build_PreCategory' {
      object :> Type;
      morphism : object object Type;

      identity : x, morphism x x;
      compose : s d d',
                  morphism d d'
                   morphism s d
                   morphism s d'
                              where "f 'o' g" := (compose f g);

      associativity : x1 x2 x3 x4
                             (m1 : morphism x1 x2)
                             (m2 : morphism x2 x3)
                             (m3 : morphism x3 x4),
                        (m3 o m2) o m1 = m3 o (m2 o m1);
      
Ask for the symmetrized version of associativity, so that (Cᵒᵖ)ᵒᵖ and C are equal without Funext
      associativity_sym : x1 x2 x3 x4
                                 (m1 : morphism x1 x2)
                                 (m2 : morphism x2 x3)
                                 (m3 : morphism x3 x4),
                            m3 o (m2 o m1) = (m3 o m2) o m1;

      left_identity : a b (f : morphism a b), identity b o f = f;
      right_identity : a b (f : morphism a b), f o identity a = f;
      
Ask for the double-identity version so that InitialTerminalCategory.Functors.from_terminal Cᵒᵖ X and (InitialTerminalCategory.Functors.from_terminal C X)ᵒᵖ are convertible.
      identity_identity : x, identity x o identity x = identity x;

      trunc_morphism : s d, IsHSet (morphism s d)
    }.

Bind Scope category_scope with PreCategory.
Bind Scope object_scope with object.
Bind Scope morphism_scope with morphism.

We want eta-expanded primitive projections to simpl away.
Arguments object !C%category / : rename.
Arguments morphism !C%category / s d : rename.
Arguments identity {!C%category} / x%object : rename.
Arguments compose {!C%category} / {s d d'}%object (m1 m2)%morphism : rename.

Local Infix "o" := compose : morphism_scope.
Perhaps we should consider making this notation more global. Perhaps we should pre-reserve all of the notations.
Local Notation "x --> y" := (morphism _ x y) (at level 99, right associativity, y at level 200) : type_scope.
Local Notation "1" := (identity _) : morphism_scope.

Define a convenience wrapper for building a precategory without specifying the redundant proofs.
Definition Build_PreCategory
           object morphism compose identity
           associativity left_identity right_identity
  := @Build_PreCategory'
       object
       morphism
       compose
       identity
       associativity
       (fun _ _ _ _ _ _ _symmetry _ _ (associativity _ _ _ _ _ _ _))
       left_identity
       right_identity
       (fun _left_identity _ _ _).

Global Existing Instance trunc_morphism.

create a hint db for all category theory things
Create HintDb category discriminated.
create a hint db for morphisms in categories
Create HintDb morphism discriminated.

Hint Resolve @left_identity @right_identity @associativity : category morphism.
Hint Rewrite @left_identity @right_identity : category.
Hint Rewrite @left_identity @right_identity : morphism.

Simple laws about the identity morphism

Section identity_unique.
  Variable C : PreCategory.

The identity morphism is unique.
  Lemma identity_unique (id0 id1 : x, morphism C x x)
        (id1_left : s d (m : morphism C s d), id1 _ o m = m)
        (id0_right : s d (m : morphism C s d), m o id0 _ = m)
  : id0 == id1.
  Proof.
    intro.
    etransitivity;
      [ symmetry; apply id1_left
      | apply id0_right ].
  Qed.

Anything equal to the identity acts like it. This is obvious, but useful as a helper lemma for automation.
  Definition concat_left_identity s d (m : morphism C s d) i
  : i = 1 i o m = m
    := fun H ⇒ (ap10 (ap _ H) _ @ left_identity _ _ _ m)%path.

  Definition concat_right_identity s d (m : morphism C s d) i
  : i = 1 m o i = m
    := fun H ⇒ (ap _ H @ right_identity _ _ _ m)%path.
End identity_unique.

Make a separate module for Notations, which can be exported/imported separately.
Module Export CategoryCoreNotations.
  Infix "o" := compose : morphism_scope.
Perhaps we should consider making this notation more global. Perhaps we should pre-reserve all of the notations.
  Local Notation "x --> y" := (@morphism _ x y) (at level 99, right associativity, y at level 200) : type_scope.
  Local Notation "x --> y" := (morphism _ x y) (at level 99, right associativity, y at level 200) : type_scope.
  Notation "1" := (identity _) : morphism_scope.
End CategoryCoreNotations.

We have a tactic for trying to run a tactic after associating morphisms either all the way to the left, or all the way to the right
Tactic Notation "try_associativity_quick" tactic(tac) :=
  first [ rewrite <- ?associativity; tac
        | rewrite → ?associativity; tac ].