catch up with master; add monoidal and closed to _CoqProject

affeldt-aist · Jun 9, 2021 · db98f34 · db98f34
1 parent 3ff9195
commit db98f34
Show file tree

Hide file tree

Showing 3 changed files with 92 additions and 86 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -26,5 +26,7 @@ example_array.v
 example_monty.v
 smallstep.v
 example_transformer.v
+monoidal_category.v
+closed_category.v
 
 -R . monae
diff --git a/closed_category.v b/closed_category.v
@@ -26,6 +26,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Local Open Scope category_scope.
 
 Module CatWithFinProd.
 Section def.
@@ -35,7 +36,7 @@ Record mixin_of (C : category) : Type := Mixin {
  snd : forall a b, {hom prod a b, b};
  univ : forall c a b, {hom c,a} -> {hom c,b} -> {hom c, prod a b};
  _ : forall c a b (f : {hom c,a}) (g : {hom c,b}),
-     f = [hom of (fst a b) \o (univ f g)];
+     f = [hom (fst a b) \o (univ f g)];
 }.
 Record class_of (T : Type) : Type := Class {
  base : Category.mixin_of T;