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

Core definition

Module Type FunctorDefinition (C D : CategoryDefinition).

  Parameter omap : C.t → D.t.
  Parameter fmap : ∀ {A B}, C.m A B → D.m (omap A) (omap B).

  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.

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 : CategoryDefinition) (F : FunctorDefinition 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 : CategoryDefinition) (F : FunctorDefinition 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.