(* 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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment