Skip to content

Commit 9c05244

Browse files
Saransh-cppandreasabel
authored andcommitted
Data.Product imports to Data.Product.Base (#2003)
1 parent 5b8c288 commit 9c05244

File tree

28 files changed

+28
-28
lines changed

28 files changed

+28
-28
lines changed

README/Data/Container/FreeMonad.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ open import Data.Unit
1616
open import Data.Bool.Base using (Bool; true)
1717
open import Data.Nat
1818
open import Data.Sum using (inj₁; inj₂)
19-
open import Data.Product renaming (_×_ to _⟨×⟩_)
19+
open import Data.Product.Base renaming (_×_ to _⟨×⟩_)
2020
open import Data.Container using (Container; _▷_)
2121
open import Data.Container.Combinator
2222
open import Data.Container.FreeMonad as FreeMonad

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
1111
module Algebra.Apartness.Properties.HeytingCommutativeRing
1212
{c ℓ₁ ℓ₂} (HCR : HeytingCommutativeRing c ℓ₁ ℓ₂) where
1313

14-
open import Data.Product using (_,_; proj₂)
14+
open import Data.Product.Base using (_,_; proj₂)
1515
open import Algebra using (CommutativeRing; RightIdentity)
1616

1717
open HeytingCommutativeRing HCR

src/Algebra/Construct/Add/Identity.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ open import Algebra.Core using (Op₂)
1414
open import Algebra.Definitions
1515
open import Algebra.Structures
1616
open import Relation.Binary.Construct.Add.Point.Equality renaming (_≈∙_ to lift≈)
17-
open import Data.Product using (_,_)
17+
open import Data.Product.Base using (_,_)
1818
open import Level using (Level; _⊔_)
1919
open import Relation.Binary.Core
2020
open import Relation.Binary.Definitions

src/Algebra/Construct/Flip/Op.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
module Algebra.Construct.Flip.Op where
1111

1212
open import Algebra
13-
import Data.Product as Prod
13+
import Data.Product.Base as Prod
1414
import Data.Sum as Sum
1515
open import Function.Base using (flip)
1616
open import Level using (Level)

src/Algebra/Construct/LexProduct/Inner.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88

99
open import Algebra
1010
open import Data.Bool.Base using (false; true)
11-
open import Data.Product using (_×_; _,_; swap; map; uncurry′)
11+
open import Data.Product.Base using (_×_; _,_; swap; map; uncurry′)
1212
open import Function.Base using (_∘_)
1313
open import Level using (Level; _⊔_)
1414
open import Relation.Binary.Definitions using (Decidable)

src/Algebra/Construct/LiftedChoice.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ open import Algebra.Consequences.Base
1414
open import Relation.Binary
1515
open import Relation.Nullary using (¬_; yes; no)
1616
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
17-
open import Data.Product using (_×_; _,_)
17+
open import Data.Product.Base using (_×_; _,_)
1818
open import Level using (Level; _⊔_)
1919
open import Relation.Binary.PropositionalEquality as P using (_≡_)
2020
open import Relation.Unary using (Pred)

src/Algebra/Construct/NaturalChoice/Min.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ open import Algebra.Core
1010
open import Algebra.Bundles
1111
open import Algebra.Construct.NaturalChoice.Base
1212
open import Data.Sum using (inj₁; inj₂; [_,_])
13-
open import Data.Product using (_,_)
13+
open import Data.Product.Base using (_,_)
1414
open import Function.Base using (id)
1515
open import Relation.Binary
1616
import Algebra.Construct.NaturalChoice.MinOp as MinOp

src/Algebra/Construct/Subst/Equality.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99

1010
{-# OPTIONS --cubical-compatible --safe #-}
1111

12-
open import Data.Product as Prod
12+
open import Data.Product.Base as Prod
1313
open import Relation.Binary.Core
1414

1515
module Algebra.Construct.Subst.Equality

src/Algebra/Lattice/Morphism/Construct/Identity.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ module Algebra.Lattice.Morphism.Construct.Identity where
1111
open import Algebra.Lattice.Bundles
1212
open import Algebra.Lattice.Morphism.Structures
1313
using ( module LatticeMorphisms )
14-
open import Data.Product using (_,_)
14+
open import Data.Product.Base using (_,_)
1515
open import Function.Base using (id)
1616
open import Level using (Level)
1717
open import Relation.Binary.Morphism.Construct.Identity using (isRelHomomorphism)

src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ open import Algebra.Lattice.Morphism.Structures
1515
import Algebra.Consequences.Setoid as Consequences
1616
import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
1717
import Algebra.Lattice.Properties.Lattice as LatticeProperties
18-
open import Data.Product using (_,_; map)
18+
open import Data.Product.Base using (_,_; map)
1919
open import Relation.Binary
2020
import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
2121
import Relation.Binary.Reasoning.Setoid as SetoidReasoning

0 commit comments

Comments
 (0)