diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_2830.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_2830.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/bug_2830.v b/test-suite/bugs/closed/bug_2830.v index 801c61b132..a321bb324e 100644 --- a/test-suite/bugs/closed/bug_2830.v +++ b/test-suite/bugs/closed/bug_2830.v @@ -194,14 +194,17 @@ Instance skel_equiv A : Equivalence (@skel A). Admitted. Import FunctionalExtensionality. -Instance set_cat : Category Type (fun A B => A -> B) := { + +Instance set_cat : Category Type (fun A B => A -> B). +refine {| id := fun A => fun x => x ; comp c b a f g := fun x => f (g x) ; eqv := fun A B => @skel (A -> B) -}. +|}. intros. compute. symmetry. apply eta_expansion. intros. compute. symmetry. apply eta_expansion. -intros. compute. reflexivity. Defined. +intros. compute. reflexivity. +Defined. (* The [list] type constructor is a Functor. *) |