Coq Functor type class with statically checked functor laws

Functor.v

Require Import Coq.Program.Basics.
Require Import Coq.Program.Syntax.
Require Import Coq.Init.Datatypes.
Require Import Coq.Unicode.Utf8.

Open Local Scope program_scope.
Open Local Scope list_scope.
Open Local Scope type_scope.

Class Functor (φ : Type → Type) := {
  fmap : forall {α β}, (α → β) → φ α → φ β;
  (** Functor laws **)
  fmap_identity : forall α (x : φ α), fmap id x = x;
  fmap_composition : forall α β γ (f : β → γ) (g : α → β) (x : φ α),
                     fmap (f ∘ g) x = (fmap f ∘ fmap g) x
}.

Instance list_functor : Functor list := {
  fmap α β := fix fmap f xs := match xs with
                               | [] => []
                               | x :: xs => (f x) :: (fmap f xs)
                               end
}.
Proof.
(** fmap_identity **)
intros.
induction x as [| x xs].
  reflexivity.
  rewrite IHxs. reflexivity.
(** fmap_composition **)
intros.
induction x as [| x xs].
  reflexivity.
  rewrite IHxs. reflexivity.
Qed.