Moved most of Function.Core to Function.Utilities (#976)

Author: MatthewDaggitt

CHANGELOG.md

@@ -14,7 +14,7 @@ module Algebra.Bundles where
 open import Algebra.Core
 open import Algebra.Structures
 open import Relation.Binary
-open import Function.Core
+open import Function.Base
 open import Level
 
 ------------------------------------------------------------------------

src/Algebra/Bundles.agda

@@ -16,7 +16,7 @@ open import Relation.Nullary using (¬_; yes; no)
 open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Product using (_×_; _,_)
 open import Level using (Level; _⊔_)
-open import Function.Core using (id; _on_)
+open import Function.Base using (id; _on_)
 open import Function.Injection using (Injection)
 open import Function.Equality using (Π)
 open import Relation.Binary using (Setoid; _Preserves_⟶_)

src/Algebra/Construct/LiftedChoice.agda

@@ -21,7 +21,7 @@ open import Algebra.Definitions _≈_
 open import Algebra.FunctionProperties.Consequences setoid
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Relation.Binary
-open import Function.Core
+open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; module Equivalence)
 open import Data.Product using (_,_)

src/Algebra/Properties/BooleanAlgebra.agda

@@ -18,7 +18,7 @@ open import Algebra.Structures
 open import Algebra.Definitions _≈_
 open import Relation.Binary
 open import Relation.Binary.Reasoning.Setoid setoid
-open import Function.Core
+open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; module Equivalence)
 open import Data.Product using (_,_)

src/Algebra/Properties/DistributiveLattice.agda

@@ -17,7 +17,7 @@ import Algebra.Properties.Semilattice as SemilatticeProperties
 open import Relation.Binary
 import Relation.Binary.Lattice as R
 open import Relation.Binary.Reasoning.Setoid  setoid
-open import Function.Core
+open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Equivalence using (_⇔_; module Equivalence)
 open import Data.Product using (_,_; swap)

src/Algebra/Properties/Lattice.agda

@@ -8,7 +8,7 @@
 
 module Axiom.Extensionality.Propositional where
 
-open import Function.Core
+open import Function.Base
 open import Level using (Level; _⊔_; suc; lift)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core

src/Axiom/Extensionality/Propositional.agda

@@ -14,7 +14,7 @@ open import Data.Bool.Base using (Bool; false; true)
 open import Data.Nat using (ℕ; zero; suc; _+_)
 open import Data.Product as Prod hiding (map)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Function.Core
+open import Function.Base
 open import Function.Equivalence using (_⇔_; equivalence)
 open import Level using (_⊔_)
 open import Relation.Binary as B hiding (Rel)

src/Category/Monad/Partiality.agda

@@ -23,7 +23,7 @@ open import Data.List.Base using (List; []; _∷_)
 open import Data.List.NonEmpty using (List⁺; _∷_)
 open import Data.Product as Prod using (∃; _×_; _,_)
 open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
-open import Function.Core
+open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (_↔_; _↔̇_; Inverse; inverse)
 open import Level using (_⊔_)

src/Codata/Musical/Colist.agda

@@ -17,7 +17,7 @@ open import Data.Product as Prod
 open import Data.Sum
 open import Data.Sum.Properties
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
-open import Function.Core
+open import Function.Base
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
 import Function.Related as Related