Coq definitions and proofs of several functors

functors.v

Require Import Coq.Program.Basics.
Open Local Scope program_scope.

Definition id (A: Type) (e: A): A := e.

Module Type FUNCTOR.
  Set Implicit Arguments.
  Parameter F: forall (A: Type), Type.
  Parameter fmap: forall (A B: Type), (A -> B) -> F A -> F B.

  Axiom associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
    fmap (g ∘ f) e = fmap g (fmap f e).

  Axiom identity: forall (A: Type) (e: F A),
    fmap (id A) e = e.
End FUNCTOR.

Inductive Identity (A: Type): Type :=
  | Id: A -> Identity A.

Module IdentityFunctor <: FUNCTOR.
  Set Implicit Arguments.

  Definition F := Identity.

  Definition fmap (A B: Type) (f: A -> B) (e: F A): F B :=
    match e with
      | Id a => Id B (f a)
    end.

  Lemma associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
    fmap (fun x: A => g (f x)) e = fmap g (fmap f e).
  Proof.
    intros.
    induction e.
    simpl.
    reflexivity.
  Qed.

  Lemma identity: forall (A: Type) (e: F A),
    fmap (id A) e = e.
  Proof.
    intros.
    induction e.
    simpl.
    reflexivity.
  Qed.
End IdentityFunctor.

Inductive Maybe (A: Type): Type :=
  | Nothing: Maybe A
  | Just: A -> Maybe A.

Module MaybeFunctor <: FUNCTOR.
  Set Implicit Arguments.

  Definition F := Maybe.

  Definition fmap (A B: Type) (f: A -> B) (e: F A): F B :=
    match e with
      | Nothing => Nothing B
      | Just a => Just B (f a)
    end.

  Lemma associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
    fmap (g ∘ f) e = fmap g (fmap f e).
  Proof.
    intros.
    induction e.
    simpl.
    reflexivity.
    simpl.
    reflexivity.
  Qed.

  Lemma identity: forall (A: Type) (e: F A),
    fmap (id A) e = e.
  Proof.
    intros.
    induction e.
    simpl.
    reflexivity.
    simpl.
    reflexivity.
  Qed.
End MaybeFunctor.

Inductive List (A: Type): Type :=
| Nil: List A
| Cons: A -> List A -> List A.

Module ListFunctor <: FUNCTOR.
  Set Implicit Arguments.

  Definition F := List.

  Fixpoint fmap (A B: Type) (f: A -> B) (e: F A) {struct e}: F B :=
    match e with
      | Nil => Nil B
      | Cons a b => Cons B (f a) (fmap f b)
    end.

  Lemma associativity: forall (A B C: Type) (f: A -> B) (g: B -> C) (e: F A),
    fmap (g ∘ f) e = fmap g (fmap f e).
  Proof.
    intros.
    induction e.
    simpl.
    reflexivity.
    simpl.
    rewrite IHe.
    reflexivity.
  Qed.

  Lemma identity : forall (A : Type) (e: F A),
    fmap (id A) e = e.
  Proof.
    intros.
    induction e.
    simpl.
    reflexivity.
    simpl.
    rewrite IHe.
    reflexivity.
  Qed.
End ListFunctor.

Recursive Extraction IdentityFunctor MaybeFunctor ListFunctor.