remove duplicate definition

copumpkin · Nov 14, 2016 · 018b837 · 018b837
1 parent eb97bc0
commit 018b837
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/Categories/Object/BinaryCoproducts.agda b/Categories/Object/BinaryCoproducts.agda
@@ -171,7 +171,3 @@ Bin→Binary bc = record { coproduct = λ {A} {B} → record {
   where
     open CP.BinCoproducts bc
 
-module BinCoproducts (coprod : BinCoproducts) where
-  open CP.BinCoproducts coprod public
-  open BinaryCoproducts (Bin→Binary coprod) public hiding ([_,_]; i₁; i₂; commute₁; commute₂; universal)
-