From 7c3b0a81bbe5edd9696c0de3e7ac8ffde02e9225 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Manuel=20B=C3=A4renz?= <m.baerenz@sonnen.de>
Date: Fri, 18 Sep 2020 12:09:45 +0200
Subject: [PATCH 1/2] Hide overlapping imports

---
 src/Generic/Lib/Category.agda     | 2 +-
 src/Generic/Lib/Data/Product.agda | 2 +-
 src/Generic/Lib/Data/Sum.agda     | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Generic/Lib/Category.agda b/src/Generic/Lib/Category.agda
index 51d3a48..b9c46b8 100644
--- a/src/Generic/Lib/Category.agda
+++ b/src/Generic/Lib/Category.agda
@@ -1,6 +1,6 @@
 module Generic.Lib.Category where
 
-open import Category.Functor public
+open import Category.Functor public hiding (Morphism)
 open import Category.Applicative public
 open import Category.Monad public
 
diff --git a/src/Generic/Lib/Data/Product.agda b/src/Generic/Lib/Data/Product.agda
index efb22ca..3c940ca 100644
--- a/src/Generic/Lib/Data/Product.agda
+++ b/src/Generic/Lib/Data/Product.agda
@@ -1,6 +1,6 @@
 module Generic.Lib.Data.Product where
 
-open import Data.Product renaming (map to pmap; zip to pzip) hiding (map₁; map₂) public
+open import Data.Product renaming (map to pmap; zip to pzip) hiding (map₁; map₂; dmap; _<*>_; assocʳ; assocˡ) public
 
 open import Generic.Lib.Intro
 open import Generic.Lib.Category
diff --git a/src/Generic/Lib/Data/Sum.agda b/src/Generic/Lib/Data/Sum.agda
index 82221be..bbc2dae 100644
--- a/src/Generic/Lib/Data/Sum.agda
+++ b/src/Generic/Lib/Data/Sum.agda
@@ -1,3 +1,3 @@
 module Generic.Lib.Data.Sum where
 
-open import Data.Sum hiding (swap) renaming (map to smap) hiding (map₁; map₂) public
+open import Data.Sum hiding (swap) renaming (map to smap) hiding (map₁; map₂; assocʳ; assocˡ) public

From a89e1739567a72b8761114e27ffa66633ce9bcf7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Manuel=20B=C3=A4renz?= <m.baerenz@sonnen.de>
Date: Fri, 18 Sep 2020 12:09:59 +0200
Subject: [PATCH 2/2] Fix whitespace

---
 src/Generic/Lib/Decidable.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Generic/Lib/Decidable.agda b/src/Generic/Lib/Decidable.agda
index 6154076..48a4662 100644
--- a/src/Generic/Lib/Decidable.agda
+++ b/src/Generic/Lib/Decidable.agda
@@ -24,7 +24,7 @@ record Eq {α} (A : Set α) : Set α where
   field _≟_ : IsSet A
 
   _==_ : A -> A -> Bool
-  x == y = ⌊ x ≟ y ⌋ 
+  x == y = ⌊ x ≟ y ⌋
 open Eq {{...}} public
 
 record _↦_ {α} (A B : Set α) : Set α where
@@ -70,11 +70,11 @@ prodM2 h f g d e = drec (λ x -> drec (h x) g e) f d
 
 sumF2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
       -> (A -> C) -> (B -> C) -> (¬ A -> ¬ B -> ¬ C) -> Dec A -> Dec B -> Dec C
-sumF2 f g h = sumM2 (yes ∘ f) (yes ∘ g) (no % ∘ h) 
+sumF2 f g h = sumM2 (yes ∘ f) (yes ∘ g) (no % ∘ h)
 
 prodF2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
        -> (A -> B -> C) -> (¬ A -> ¬ C) -> (¬ B -> ¬ C) -> Dec A -> Dec B -> Dec C
-prodF2 h f g = prodM2 (yes % ∘ h) (no ∘ f) (no ∘ g) 
+prodF2 h f g = prodM2 (yes % ∘ h) (no ∘ f) (no ∘ g)
 
 dcong : ∀ {α β} {A : Set α} {B : Set β} {x y}
       -> (f : A -> B) -> (f x ≡ f y -> x ≡ y) -> x # y -> f x # f y
@@ -89,7 +89,7 @@ dcong₂ : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ} {x₁ x₂ y₁
 dcong₂ f inj = prodF2 (cong₂ f) (λ c -> c ∘ proj₁ ∘ inj) (λ c -> c ∘ proj₂ ∘ inj)
 
 dhcong₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {x₁ x₂ y₁ y₂}
-        -> (f : ∀ x -> B x -> C) 
+        -> (f : ∀ x -> B x -> C)
         -> (f x₁ y₁ ≡ f x₂ y₂ -> [ B ] y₁ ≅ y₂)
         -> x₁ # x₂
         -> (∀ y₂ -> y₁ # y₂)