remove everything deprecated from v1.3 (and before)

src/Algebra/Morphism.agda

@@ -49,7 +49,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     module T = Semigroup To
   open Definitions F.Carrier T.Carrier T._≈_
 
-  record IsSemigroupMorphism (⟦_⟧ : Morphism) :
+  record IsSemigroupMorphism (⟦_⟧ : F.Carrier → T.Carrier) :
          Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
     field
       ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
@@ -67,7 +67,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     module T = Monoid To
   open Definitions F.Carrier T.Carrier T._≈_
 
-  record IsMonoidMorphism (⟦_⟧ : Morphism) :
+  record IsMonoidMorphism (⟦_⟧ : F.Carrier → T.Carrier) :
          Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
     field
       sm-homo : IsSemigroupMorphism F.semigroup T.semigroup ⟦_⟧
@@ -87,7 +87,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     module T = CommutativeMonoid To
   open Definitions F.Carrier T.Carrier T._≈_
 
-  record IsCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
+  record IsCommutativeMonoidMorphism (⟦_⟧ : F.Carrier → T.Carrier) :
          Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
     field
       mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
@@ -106,7 +106,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     module T = IdempotentCommutativeMonoid To
   open Definitions F.Carrier T.Carrier T._≈_
 
-  record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : Morphism) :
+  record IsIdempotentCommutativeMonoidMorphism (⟦_⟧ : F.Carrier → T.Carrier) :
          Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
     field
       mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
@@ -129,7 +129,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     module T = Group To
   open Definitions F.Carrier T.Carrier T._≈_
 
-  record IsGroupMorphism (⟦_⟧ : Morphism) :
+  record IsGroupMorphism (⟦_⟧ : F.Carrier → T.Carrier) :
          Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
     field
       mn-homo : IsMonoidMorphism F.monoid T.monoid ⟦_⟧
@@ -155,7 +155,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     module T = AbelianGroup To
   open Definitions F.Carrier T.Carrier T._≈_
 
-  record IsAbelianGroupMorphism (⟦_⟧ : Morphism) :
+  record IsAbelianGroupMorphism (⟦_⟧ : F.Carrier → T.Carrier) :
          Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
     field
       gp-homo : IsGroupMorphism F.group T.group ⟦_⟧
@@ -174,7 +174,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     module T = Ring To
   open Definitions F.Carrier T.Carrier T._≈_
 
-  record IsRingMorphism (⟦_⟧ : Morphism) :
+  record IsRingMorphism (⟦_⟧ : F.Carrier → T.Carrier) :
          Set (c₁ ⊔ ℓ₁ ⊔ c₂ ⊔ ℓ₂) where
     field
       +-abgp-homo : ⟦_⟧ Is F.+-abelianGroup -AbelianGroup⟶ T.+-abelianGroup

src/Algebra/Morphism/Definitions.agda

@@ -28,19 +28,3 @@ Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ (∘ ⟦ x ⟧)
 
 Homomorphic₂ : (A → B) → Op₂ A → Op₂ B → Set _
 Homomorphic₂ ⟦_⟧ _∙_ _∘_ = ∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 1.3
-
-Morphism : Set _
-Morphism = A → B
-
-{-# WARNING_ON_USAGE Morphism
-"Warning: Morphism was deprecated in v1.3.
-Please use the standard function notation (e.g. A → B) instead."
-#-}

src/Algebra/Solver/Ring/AlmostCommutativeRing.agda

@@ -85,7 +85,7 @@ record _-Raw-AlmostCommutative⟶_
     module T = AlmostCommutativeRing To
   open MorphismDefinitions F.Carrier T.Carrier T._≈_
   field
-    ⟦_⟧    : Morphism
+    ⟦_⟧    : F.Carrier → T.Carrier
     +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
     *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
     -‿homo : Homomorphic₁ ⟦_⟧ F.-_  T.-_

src/Data/Fin/Subset/Properties.agda

@@ -859,19 +859,3 @@ anySubset? : ∀ {P : Pred (Subset n) ℓ} → Decidable P → Dec ∃⟨ P ⟩
 anySubset? {n = zero}  P? = Dec.map ∃-Subset-[]-⇔ (P? [])
 anySubset? {n = suc n} P? = Dec.map ∃-Subset-∷-⇔
   (anySubset? (P? ∘ (inside ∷_)) ⊎-dec anySubset? (P? ∘ (outside ∷_)))
-
-
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 1.3
-
-p⊆q⇒∣p∣<∣q∣ = p⊆q⇒∣p∣≤∣q∣
-{-# WARNING_ON_USAGE p⊆q⇒∣p∣<∣q∣
-"Warning: p⊆q⇒∣p∣<∣q∣ was deprecated in v1.3.
-Please use p⊆q⇒∣p∣≤∣q∣ instead."
-#-}

src/Data/Integer.agda

@@ -21,12 +21,6 @@ open import Data.Integer.Properties public
 ------------------------------------------------------------------------
 -- Deprecated
 
--- Version 0.17
-
-open import Data.Integer.Properties public
-  using (◃-cong; drop‿+≤+; drop‿-≤-)
-  renaming (◃-inverse to ◃-left-inverse)
-
 -- Version 1.5
 -- Show
 

src/Data/List/Relation/Unary/All/Properties.agda

@@ -755,14 +755,6 @@ module _ (S : Setoid c ℓ) where
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
 
--- Version 1.3
-
-Any¬→¬All = Any¬⇒¬All
-{-# WARNING_ON_USAGE Any¬→¬All
-"Warning: Any¬→¬All was deprecated in v1.3.
-Please use Any¬⇒¬All instead."
-#-}
-
 -- Version 2.0
 
 updateAt-id-relative = updateAt-id-local

src/Data/Nat.agda

@@ -40,8 +40,6 @@ open import Data.Nat.Properties public
 ------------------------------------------------------------------------
 -- Deprecated
 
--- Version 0.17
-
 -- Version 2.0
 
 -- solely for the re-export of this name, formerly in `Data.Nat.Properties.Core`

src/Data/Nat/Properties.agda

@@ -2255,21 +2255,6 @@ module _ {p} {P : Pred ℕ p} (P? : U.Decidable P) where
 -- Please use the new names as continuing support for the old names is
 -- not guaranteed.
 
--- Version 1.3
-
-∀[m≤n⇒m≢o]⇒o<n : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
-∀[m≤n⇒m≢o]⇒o<n = ∀[m≤n⇒m≢o]⇒n<o
-{-# WARNING_ON_USAGE ∀[m≤n⇒m≢o]⇒o<n
-"Warning: ∀[m≤n⇒m≢o]⇒o<n was deprecated in v1.3.
-Please use ∀[m≤n⇒m≢o]⇒n<o instead."
-#-}
-∀[m<n⇒m≢o]⇒o≤n : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
-∀[m<n⇒m≢o]⇒o≤n = ∀[m<n⇒m≢o]⇒n≤o
-{-# WARNING_ON_USAGE ∀[m<n⇒m≢o]⇒o≤n
-"Warning: ∀[m<n⇒m≢o]⇒o≤n was deprecated in v1.3.
-Please use ∀[m<n⇒m≢o]⇒n≤o instead."
-#-}
-
 -- Version 1.4
 
 *-+-isSemiring = +-*-isSemiring

src/Data/Rational.agda

@@ -18,11 +18,6 @@ open import Data.Rational.Properties public
 ------------------------------------------------------------------------
 -- Deprecated
 
--- Version 1.0
-
-open import Data.Rational.Properties public
-  using (drop-*≤*; ≃⇒≡; ≡⇒≃)
-
 -- Version 1.5
 
 import Data.Integer.Show as ℤ

src/Induction/WellFounded.agda

@@ -201,65 +201,3 @@ module TransitiveClosure {A : Set a} (_<_ : Rel A ℓ) where
   "Warning: _<⁺_ was deprecated in v1.5.
 \ \Please use TransClosure from Relation.Binary.Construct.Closure.Transitive instead."
   #-}
-
-
--- DEPRECATED in v1.3.
--- Please use `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict` instead.
-module Lexicographic {A : Set a} {B : A → Set b}
-                     (RelA : Rel A ℓ₁)
-                     (RelB : ∀ x → Rel (B x) ℓ₂) where
-
-  infix 4 _<_
-  data _<_ : Rel (Σ A B) (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
-    left  : ∀ {x₁ y₁ x₂ y₂} (x₁<x₂ : RelA   x₁ x₂) → (x₁ , y₁) < (x₂ , y₂)
-    right : ∀ {x y₁ y₂}     (y₁<y₂ : RelB x y₁ y₂) → (x  , y₁) < (x  , y₂)
-
-  mutual
-
-    accessible : ∀ {x y} →
-                 Acc RelA x → (∀ {x} → WellFounded (RelB x)) →
-                 Acc _<_ (x , y)
-    accessible accA wfB = acc (accessible′ accA (wfB _) wfB)
-
-
-    accessible′ :
-      ∀ {x y} →
-      Acc RelA x → Acc (RelB x) y → (∀ {x} → WellFounded (RelB x)) →
-      WfRec _<_ (Acc _<_) (x , y)
-    accessible′ (acc rsA) _    wfB (left  x′<x) = accessible (rsA x′<x) wfB
-    accessible′ accA (acc rsB) wfB (right y′<y) =
-      acc (accessible′ accA (rsB y′<y) wfB)
-
-  wellFounded : WellFounded RelA → (∀ {x} → WellFounded (RelB x)) →
-                WellFounded _<_
-  wellFounded wfA wfB p = accessible (wfA (proj₁ p)) wfB
-
-  well-founded = wellFounded
-
-  {-# WARNING_ON_USAGE _<_
-  "Warning: _<_ was deprecated in v1.3.
-\ \Please use `×-Lex` from `Data.Product.Relation.Binary.Lex.Strict` instead."
-  #-}
-  {-# WARNING_ON_USAGE accessible
-  "Warning: accessible was deprecated in v1.3."
-  #-}
-  {-# WARNING_ON_USAGE accessible′
-  "Warning: accessible′ was deprecated in v1.3."
-  #-}
-  {-# WARNING_ON_USAGE wellFounded
-  "Warning: wellFounded was deprecated in v1.3.
-\ \Please use `×-wellFounded` from `Data.Product.Relation.Binary.Lex.Strict` instead."
-  #-}
-
-
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
--- Version 1.0
-
-module Inverse-image = InverseImage
-module Transitive-closure = TransitiveClosure