Library models.FreeCategories

Require Import Category.
Require Import Functor.

Free category generated by a quiver

Definition

Module FreeCategory (Q : Quiver) <: Category.

  Inductive path (A : Q.t) : Q.t → Type :=
    | nil : path A A
    | cons {B C} : Q.m A B → path B C → path A C.

  Arguments nil {A}.
  Arguments cons {A B C}.

  Definition emb {A B} (e : Q.m A B) : path A B :=
    cons e nil.

  Fixpoint app {A B C} (x : path A B) : path B C → path A C :=
    match x with
      | nil ⇒ fun y ⇒ y
      | cons e x ⇒ fun y ⇒ cons e (app x y)
    end.

  Definition t := Q.t.
  Definition m (A B : t) := path A B.

  Definition id A : m A A :=
    nil.

  Definition compose {A B C} (g : m B C) (f : m A B) : m A C :=
    app f g.

  Proposition compose_id_left {A B} (f : m A B) :
    compose (id B) f = f.

  Proposition compose_id_right {A B} (f : m A B) :
    compose f (id A) = f.

  Proposition compose_assoc {A B C D} (f : m A B) (g : m B C) (h : m C D) :
    compose (compose h g) f = compose h (compose g f).

  Include CategoryTheory.
End FreeCategory.

Module Type FreeCategoryInstance (Q : Quiver).
  Include FreeCategory Q.
End FreeCategoryInstance.

Related constructions

The free category construction can be characterized as the left adjoint FreeCategory ⊣ U : Cat → Quiv to the forgetful functor from Cat to the category Quiv of quivers and their homomorphisms. This gives us a number of useful constructions.

Embedding

The adjunction's unit defines an embedding of any quiver into the free category that is generates.

Module FreeCategoryEmbedding (Q : Quiver) (C : FreeCategoryInstance Q)
    <: QuiverHomomorphism Q C.
  Definition omap (A : Q.t) : C.t := A.
  Definition fmap {A B} : Q.m A B → C.m (omap A) (omap B) := C.emb.
End FreeCategoryEmbedding.

Interpretation functor

The adjoint transpose of a quiver homomorphism from Q into a category D is a functor which interprets the paths in the free as composite morphisms in D.

Module FreeCategoryInterpretation
  (Q : Quiver) (D : Category) (F : QuiverHomomorphism Q D)
  (C : FreeCategoryInstance Q) <: Functor C D.

  Definition omap : C.t → D.t :=
    F.omap.

  Fixpoint fmap {A B} (f : C.m A B) : D.m (omap A) (omap B) :=
    match f with
      | C.nil ⇒ D.id (omap A)
      | C.cons e f' ⇒ D.compose (fmap f') (F.fmap e)
    end.

  Proposition fmap_id A :
    fmap (C.id A) = D.id (omap A).

  Proposition fmap_compose {A B C} (g : C.m B C) (f : C.m A B) :
    fmap (C.compose g f) = D.compose (fmap g) (fmap f).

  Include FunctorTheory C D.

  Theorem fmap_emb {A B} (f : Q.m A B) :
    fmap (C.emb f) = F.fmap f.
End FreeCategoryInterpretation.