Library interfaces.Functor

In this library we define module interfaces for various kind of fixed functors between category modules. Note that functors can also be treated as first-order objects; see the FunctorCategory library.

Require Import interfaces.Category.

Functors

Quiver homorphisms

In some cases it is useful to define mappings between quivers or mappings between categories which do not preserve composition and identities. The following interface is used for this.

Module Type QuiverHomomorphism (C D : Quiver).
Parameter omap : C.t → D.t.
Parameter fmap : ∀ {A B}, C.m A B → D.m (omap A) (omap B).
End QuiverHomomorphism.

Functors

Most of the time, we do want the extra properties that the identities and composites are preserved.

Module Type FunctorDefinition (C D : CategoryDefinition).
  Include QuiverHomomorphism C D.

  Axiom fmap_id :
    ∀ A, fmap (C.id A) = D.id (omap A).

  Axiom 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).

End FunctorDefinition.

Theory

In that case, the following properties and definitions can be derived.

Module FunctorTheory (C D : Category) (F : FunctorDefinition C D).
  Import F.

  Program Canonical Structure fmap_iso {A B} (f : C.iso A B) : D.iso (omap A) (omap B) :=
    {|
      D.fw := fmap (C.fw f);
      D.bw := fmap (C.bw f);
    |}.

End FunctorTheory.

Module Type Functor (C D : Category) :=
  FunctorDefinition C D <+
  FunctorTheory C D.

Additional properties

Module Type Faithful (C D : Quiver) (F : QuiverHomomorphism C D).

  Axiom faithful :
    ∀ {A B} (f g : C.m A B), F.fmap f = F.fmap g → f = g.

End Faithful.

Module Type Full (C D : Quiver) (F : QuiverHomomorphism C D).

  Axiom full :
    ∀ {A B} (d : D.m (F.omap A) (F.omap B)),
    ∃ (c : C.m A B ), F.fmap c = d.

End Full.

Module Type FullFunctor (C D : Category) :=
  Functor C D <+ Full C D.

Module Type FaithfulFunctor (C D : Category) :=
  Functor C D <+ Faithful C D.

Module Type FullAndFaithfulFunctor (C D : Category) :=
  Functor C D <+ Full C D <+ Faithful C D.

Bifunctors

We also provide separate definitions for bifunctors, which we use to define monoidal structures. Although bifunctors can be described as functors from product categories (see BifunctorTheory below), it is much more convenient to give a direct definition in terms of binary functions.

Definition

Module Type BifunctorDefinition (C1 C2 D : CategoryDefinition).

  Parameter omap : C1.t → C2.t → D.t.

  Parameter fmap :
    ∀ {A1 A2 B1 B2},
      C1.m A1 B1 → C2.m A2 B2 → D.m (omap A1 A2) (omap B1 B2).

  Axiom fmap_id :
    ∀ A1 A2, fmap (C1.id A1) (C2.id A2) = D.id (omap A1 A2).

  Axiom fmap_compose :
    ∀ {A1 A2 B1 B2 C1 C2},
      ∀ (g1 : C1.m B1 C1) (g2 : C2.m B2 C2) (f1 : C1.m A1 B1) (f2 : C2.m A2 B2),
        fmap (C1.compose g1 f1) (C2.compose g2 f2) =
          D.compose (fmap g1 g2) (fmap f1 f2).

End BifunctorDefinition.

Properties

Module BifunctorTheory (C1 C2 D : Category) (F : BifunctorDefinition C1 C2 D).

Preservation of isomorphisms

  Program Canonical Structure fmap_iso {A1 A2 B1 B2} (f1 : C1.iso A1 B1) (f2 : C2.iso A2 B2) :=
    {|
      D.fw := F.fmap (C1.fw f1) (C2.fw f2);
      D.bw := F.fmap (C1.bw f1) (C2.bw f2);
    |}.

A bifunctor can be seen as a functor from the product category.

  Module PC := Prod C1 C2.

  Module PF <: Functor PC D.

    Definition omap (X : PC.t) : D.t :=
      F.omap (fst X) (snd X).

    Definition fmap {A B} (f : PC.m A B) : D.m (omap A) (omap B) :=
      F.fmap (fst f) (snd f).

    Proposition fmap_id {A} :
      fmap (PC.id A) = D.id (omap A).

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

    Include FunctorTheory PC D.
  End PF.

End BifunctorTheory.

Bundled interface

Module Type Bifunctor (C1 C2 D : Category).
Include BifunctorDefinition C1 C2 D.
Include BifunctorTheory C1 C2 D.
End Bifunctor.