make one thing work by simply deleting useless imports.

agda · Dec 21, 2023 · e6a6ea4 · e6a6ea4
1 parent da8bb03
commit e6a6ea4
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/Categories/Category/Monoidal/Instance/Sets.agda b/src/Categories/Category/Monoidal/Instance/Sets.agda
@@ -9,9 +9,9 @@ open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry; map; <
 open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Unit using (⊤)
 open import Relation.Binary.PropositionalEquality.Core
-open import Function.Inverse using (module Inverse; _↔_)
+-- open import Function.Inverse using (module Inverse; _↔_)
 open import Function.Related.TypeIsomorphisms
-open import Function.Equality using () renaming (_⟨$⟩_ to fun)
+-- open import Function.Equality using () renaming (_⟨$⟩_ to fun)
 open import Function using (_$_)
 
 open import Categories.Category.BinaryProducts using (BinaryProducts)