Skip to content

Commit 41696ed

Browse files
committed
chore: move imports around in Algebra.Definitions
merge
1 parent a34b4b5 commit 41696ed

File tree

1 file changed

+0
-8
lines changed

1 file changed

+0
-8
lines changed

src/Algebra/Definitions.agda

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,7 @@
1515

1616
{-# OPTIONS --cubical-compatible --safe #-}
1717

18-
<<<<<<< HEAD
1918
open import Relation.Binary.Core using (Rel)
20-
=======
21-
open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
22-
>>>>>>> f0e0101df (chore: move imports around in Algebra.Definitions)
2319

2420
module Algebra.Definitions
2521
{a ℓ} {A : Set a} -- The underlying set
@@ -29,13 +25,9 @@ module Algebra.Definitions
2925
open import Algebra.Core using (Op₁; Op₂)
3026
open import Data.Product.Base using (_×_; ∃-syntax)
3127
open import Data.Sum.Base using (_⊎_)
32-
<<<<<<< HEAD
3328
open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂)
3429
open import Relation.Nullary.Negation.Core using (¬_)
3530

36-
=======
37-
open import Relation.Nullary.Negation.Core using (¬_)
38-
>>>>>>> f0e0101df (chore: move imports around in Algebra.Definitions)
3931

4032
------------------------------------------------------------------------
4133
-- Properties of operations

0 commit comments

Comments
 (0)