Qualified import of Data.Sum.Base fixing #2280 (#2290)

* Qualified import of `Data.Sum.Base as Sum`

* resolve merge conflict in favour of #2293

Author: jamesmckinna

src/Codata/Sized/Delay.agda

@@ -16,9 +16,9 @@ open import Data.Empty
 open import Relation.Nullary
 open import Data.Nat.Base
 open import Data.Maybe.Base hiding (map ; fromMaybe ; zipWith ; alignWith ; zip ; align)
-open import Data.Product.Base as P hiding (map ; zip)
-open import Data.Sum.Base as S hiding (map)
-open import Data.These.Base as T using (These; this; that; these)
+open import Data.Product.Base hiding (map ; zip)
+open import Data.Sum.Base hiding (map)
+open import Data.These.Base using (These; this; that; these)
 open import Function.Base using (id)
 
 ------------------------------------------------------------------------

src/Data/Container/Combinator.agda

@@ -10,8 +10,8 @@ module Data.Container.Combinator where
 
 open import Level using (Level; _⊔_; lower)
 open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
-open import Data.Product.Base as P using (_,_; <_,_>; proj₁; proj₂; ∃)
-open import Data.Sum.Base as S using ([_,_]′)
+open import Data.Product.Base as Product using (_,_; <_,_>; proj₁; proj₂; ∃)
+open import Data.Sum.Base as Sum using ([_,_]′)
 open import Data.Unit.Polymorphic.Base using (⊤)
 import Function.Base as F
 
@@ -58,25 +58,25 @@ module _ {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s
   _∘_ .Position = ◇ C₁ (Position C₂)
 
   to-∘ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A) → ⟦ _∘_ ⟧ A
-  to-∘ (s , f) = ((s , proj₁ F.∘ f) , P.uncurry (proj₂ F.∘ f) F.∘′ ◇.proof)
+  to-∘ (s , f) = ((s , proj₁ F.∘ f) , Product.uncurry (proj₂ F.∘ f) F.∘′ ◇.proof)
 
   from-∘ : ∀ {a} {A : Set a} → ⟦ _∘_ ⟧ A → ⟦ C₁ ⟧ (⟦ C₂ ⟧ A)
-  from-∘ ((s , f) , g) = (s , < f , P.curry (g F.∘′ any) >)
+  from-∘ ((s , f) , g) = (s , < f , Product.curry (g F.∘′ any) >)
 
 -- Product. (Note that, up to isomorphism, this is a special case of
 -- indexed product.)
 
   infixr 2 _×_
 
   _×_ : Container (s₁ ⊔ s₂) (p₁ ⊔ p₂)
-  _×_ .Shape    = Shape C₁ P.× Shape C₂
-  _×_ .Position = P.uncurry λ s₁ s₂ → (Position C₁ s₁) S.⊎ (Position C₂ s₂)
+  _×_ .Shape    = Shape C₁ Product.× Shape C₂
+  _×_ .Position = Product.uncurry λ s₁ s₂ → (Position C₁ s₁) Sum.⊎ (Position C₂ s₂)
 
-  to-× : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A → ⟦ _×_ ⟧ A
+  to-× : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A → ⟦ _×_ ⟧ A
   to-× ((s₁ , f₁) , (s₂ , f₂)) = ((s₁ , s₂) , [ f₁ , f₂ ]′)
 
-  from-× : ∀ {a} {A : Set a} → ⟦ _×_ ⟧ A → ⟦ C₁ ⟧ A P.× ⟦ C₂ ⟧ A
-  from-× ((s₁ , s₂) , f) = ((s₁ , f F.∘ S.inj₁) , (s₂ , f F.∘ S.inj₂))
+  from-× : ∀ {a} {A : Set a} → ⟦ _×_ ⟧ A → ⟦ C₁ ⟧ A Product.× ⟦ C₂ ⟧ A
+  from-× ((s₁ , s₂) , f) = ((s₁ , f F.∘ Sum.inj₁) , (s₂ , f F.∘ Sum.inj₂))
 
 -- Indexed product.
 
@@ -87,7 +87,7 @@ module _ {i s p} (I : Set i) (Cᵢ : I → Container s p) where
   Π .Position = λ s → ∃ λ i → Position (Cᵢ i) (s i)
 
   to-Π : ∀ {a} {A : Set a} → (∀ i → ⟦ Cᵢ i ⟧ A) → ⟦ Π ⟧ A
-  to-Π f = (proj₁ F.∘ f , P.uncurry (proj₂ F.∘ f))
+  to-Π f = (proj₁ F.∘ f , Product.uncurry (proj₂ F.∘ f))
 
   from-Π : ∀ {a} {A : Set a} → ⟦ Π ⟧ A → ∀ i → ⟦ Cᵢ i ⟧ A
   from-Π (s , f) = λ i → (s i , λ p → f (i , p))
@@ -108,15 +108,15 @@ module _ {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where
   infixr 1 _⊎_
 
   _⊎_ : Container (s₁ ⊔ s₂) p
-  _⊎_ .Shape    = (Shape C₁ S.⊎ Shape C₂)
+  _⊎_ .Shape    = (Shape C₁ Sum.⊎ Shape C₂)
   _⊎_ .Position = [ Position C₁ , Position C₂ ]′
 
-  to-⊎ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A → ⟦ _⊎_ ⟧ A
-  to-⊎ = [ P.map S.inj₁ F.id , P.map S.inj₂ F.id ]′
+  to-⊎ : ∀ {a} {A : Set a} → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A → ⟦ _⊎_ ⟧ A
+  to-⊎ = [ Product.map Sum.inj₁ F.id , Product.map Sum.inj₂ F.id ]′
 
-  from-⊎ : ∀ {a} {A : Set a} → ⟦ _⊎_ ⟧ A → ⟦ C₁ ⟧ A S.⊎ ⟦ C₂ ⟧ A
-  from-⊎ (S.inj₁ s₁ , f) = S.inj₁ (s₁ , f)
-  from-⊎ (S.inj₂ s₂ , f) = S.inj₂ (s₂ , f)
+  from-⊎ : ∀ {a} {A : Set a} → ⟦ _⊎_ ⟧ A → ⟦ C₁ ⟧ A Sum.⊎ ⟦ C₂ ⟧ A
+  from-⊎ (Sum.inj₁ s₁ , f) = Sum.inj₁ (s₁ , f)
+  from-⊎ (Sum.inj₂ s₂ , f) = Sum.inj₂ (s₂ , f)
 
 -- Indexed sum.
 

src/Data/Container/Combinator/Properties.agda

@@ -13,7 +13,7 @@ open import Data.Container.Core
 open import Data.Container.Combinator
 open import Data.Container.Relation.Unary.Any
 open import Data.Empty using (⊥-elim)
-open import Data.Product.Base as Prod using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
+open import Data.Product.Base as P using (∃; _,_; proj₁; proj₂; <_,_>; uncurry; curry)
 open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_])
 open import Function.Base as F using (_∘′_)
 open import Function.Bundles
@@ -45,7 +45,7 @@ module Composition {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Co
 module Product (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′)
        {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
 
-  correct : ∀ {x} {X : Set x} →  ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X Prod.× ⟦ C₂ ⟧ X)
+  correct : ∀ {x} {X : Set x} →  ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X P.× ⟦ C₂ ⟧ X)
   correct {X = X} = mk↔ₛ′ (from-× C₁ C₂) (to-× C₁ C₂) (λ _ → refl) from∘to
     where
     from∘to : (to-× C₁ C₂) F.∘ (from-× C₁ C₂) ≗ F.id