module conventions

copumpkin · Nov 14, 2016 · d461d2a · d461d2a
1 parent 289cd83
commit d461d2a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Categories/Object/Exponentiating.agda b/Categories/Object/Exponentiating.agda
@@ -7,7 +7,7 @@ module Categories.Object.Exponentiating {o ℓ e}
     (binary : BinaryProducts C)  where
 
 open Category C
-open BinaryProducts C binary
+open BinaryProducts binary
 
 import Categories.Object.Product
 open Categories.Object.Product C