Skip to content

Instantly share code, notes, and snippets.

@bmsherman bmsherman/Refine.v

Created Aug 2, 2016
Embed
What would you like to do?
(* 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
You can’t perform that action at this time.