Merge pull request #738 from anuyts/remove-product

Remove Product, which is a copy of BinProduct
agda · Mar 25, 2022 · 7f18d48 · 7f18d48
2 parents d727f3e + 71c34d3
commit 7f18d48
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 92 deletions.
diff --git a/Cubical/Categories/Constructions/Product.agda b/Cubical/Categories/Constructions/Product.agda
diff --git a/Cubical/Categories/Functor/Product.agda b/Cubical/Categories/Functor/Product.agda
diff --git a/Cubical/Categories/Monoidal/Base.agda b/Cubical/Categories/Monoidal/Base.agda
@@ -4,9 +4,9 @@
 module Cubical.Categories.Monoidal.Base where
 
 open import Cubical.Categories.Category.Base
-open import Cubical.Categories.Constructions.Product
+open import Cubical.Categories.Constructions.BinProduct
 open import Cubical.Categories.Functor.Base
-open import Cubical.Categories.Functor.Product
+open import Cubical.Categories.Functor.BinProduct
 open import Cubical.Categories.Morphism
 open import Cubical.Categories.NaturalTransformation.Base
 open import Cubical.Foundations.Prelude