Skip to content

Commit 99da9cb

Browse files
committed
cosmetic changes: limit Data.Sum.Base imports
1 parent c3d32b1 commit 99da9cb

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/Function/Related/TypeIsomorphisms.agda

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ open import Data.Product.Base as Product
2626
open import Data.Product.Function.NonDependent.Propositional
2727
import Data.Product.Properties as Product
2828
open import Data.Sum.Base as Sum
29+
using (_⊎_; inj₁; inj₂; [_,_]; [_,_]′)
2930
import Data.Sum.Properties as Sum
3031
open import Data.Sum.Function.Propositional using (_⊎-cong_)
3132
open import Data.Unit.Polymorphic.Base using (⊤)

0 commit comments

Comments
 (0)