Refine.v

(* Categories *)
Class Cat {C : Type} :=
  { arr : C -> C -> Type
  ; eq : forall {A B : C}, arr A B -> arr A B -> Prop }.

Arguments Cat : clear implicits.

Section Functor.
Context {C D : Type} `{Cat C} `{Cat D}.

Require Import Morphisms.

Record Functor : Type := Build_Functor
  { fobj : C -> D
  ; fmap : forall {A B : C}, arr A B -> arr (fobj A) (fobj B)
  ; fmap_Proper : forall {A B : C}, Proper (eq ==> eq) (@fmap A B) 
  }.

Global Instance fmap_ProperI (F : Functor) A B : 
  Proper (eq ==> eq) (@fmap F A B)
  := fmap_Proper F.

End Functor.

Arguments Functor C D {_ _} : clear implicits.

Definition compose_Functor {C D E : Type} `{catC : Cat C} `{catD : Cat D}
  `{catE : Cat E} (F : Functor C D) (G : Functor D E)
  : Functor C E.
Proof.
simple refine (Build_Functor _ _ _).
(* Why doesn't the above tactic change the goal? 
   In fact, it is doing something. Leaving the final underscore
   causes Coq to guess the hole corresponding to the 'fmap_Proper' instance
   using the instance 'fmap_ProperI', and so spawns a subgoal to create
   "another" term of type 'Functor C E'. This circularity is obviously
   undesirable.
 *)

unshelve eapply Build_Functor.

(* 'unshelve eapply', instead, simply creates a goal for each 
  argument to the term that is passed in, as desired. *)
Abort.