added enriched_cat_case6.v

math-comp · Oct 4, 2023 · 39361f5 · 39361f5
1 parent 101a634
commit 39361f5
Show file tree

Hide file tree

Showing 3 changed files with 613 additions and 3 deletions.
diff --git a/tests/enriched_cat_case1.v b/tests/enriched_cat_case1.v
@@ -43,6 +43,7 @@ HB.structure Definition ICMon := { T of isICMon T }.
 
 (*****  wrapping ****************************************************)
 
+
 #[wrapper]
 HB.mixin Record hom_isMagma T of Quiver T :=
     { hom_isMagma_private : forall A B, isMagma (@hom T A B) }.
@@ -54,6 +55,10 @@ HB.structure
 #[wrapper]
 HB.mixin Record hom_isMon T of Quiver T :=
     { hom_isMon_private : forall A B, Mon (@hom T A B) }.
+#[verbose]
+HB.structure
+   Definition Mon_enriched_quiver :=
+     { Obj of isQuiver Obj & hom_isMon Obj }.
 *)
 (* need to add explicitly Magma_enriched_quiver, otherwise switch 
    from mixin to structure *)
@@ -168,10 +173,15 @@ Obligation 3.
    destruct (x a); auto.
 Qed.
 
+Fail Check Type : Mon_enriched_quiver.type.             
+Fail Check hom (nat:Type) nat: Mon.type.
+
 HB.instance Definition funQ_Monoid (A B: Type) :
   isMon (hom A B) := funQ_isMon A B.
 
 Check Type : Mon_enriched_quiver.type.             
+Check hom (nat:Type) nat: Mon.type.
+
 
 (** INSTANCE 2 **********************************************
 

diff --git a/tests/enriched_cat_case5.v b/tests/enriched_cat_case5.v
@@ -144,13 +144,13 @@ HB.factory Record isMICAlg T of Mon T := {
     amidem : idempotent amop; 
   }.
 
-HB.builders Context T (f : isMICAlg T).
+HB.builders Context T (_ : isMICAlg T).
 
   Lemma amop_mop_eq : amop = mop.
-    destruct f; simpl.
+   (* destruct f; simpl. *)
     eapply functional_extensionality; intro.
     eapply functional_extensionality; intro.
-    auto.
+    apply ameq.
   Qed.  
 
   Definition dum_comm :=