diff --git a/src/Algebra/FunctionProperties/Consequences.agda b/src/Algebra/FunctionProperties/Consequences.agda
deleted file mode 100644
index e77b0b6d4e..0000000000
--- a/src/Algebra/FunctionProperties/Consequences.agda
+++ /dev/null
@@ -1,22 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- This module is DEPRECATED.
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Definitions
-  using (Substitutive; Symmetric; Total)
-
-module Algebra.FunctionProperties.Consequences
-  {a ℓ} (S : Setoid a ℓ) where
-
-{-# WARNING_ON_IMPORT
-"Algebra.FunctionProperties.Consequences was deprecated in v1.3.
-Use Algebra.Consequences.Setoid instead."
-#-}
-
-open import Algebra.Consequences.Setoid S public
diff --git a/src/Algebra/FunctionProperties/Consequences/Core.agda b/src/Algebra/FunctionProperties/Consequences/Core.agda
deleted file mode 100644
index 58c1c0afa9..0000000000
--- a/src/Algebra/FunctionProperties/Consequences/Core.agda
+++ /dev/null
@@ -1,17 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- This module is DEPRECATED.
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module Algebra.FunctionProperties.Consequences.Core
-  {a} {A : Set a} where
-
-{-# WARNING_ON_IMPORT
-"Algebra.FunctionProperties.Consequences.Core was deprecated in v1.3.
-Use Algebra.Consequences.Base instead."
-#-}
-
-open import Algebra.Consequences.Base public
diff --git a/src/Algebra/FunctionProperties/Consequences/Propositional.agda b/src/Algebra/FunctionProperties/Consequences/Propositional.agda
deleted file mode 100644
index b1f2d383cb..0000000000
--- a/src/Algebra/FunctionProperties/Consequences/Propositional.agda
+++ /dev/null
@@ -1,17 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- This module is DEPRECATED.
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
-module Algebra.FunctionProperties.Consequences.Propositional
-  {a} {A : Set a} where
-
-{-# WARNING_ON_IMPORT
-"Algebra.FunctionProperties.Consequences.Propositional was deprecated in v1.3.
-Use Algebra.Consequences.Propositional instead."
-#-}
-
-open import Algebra.Consequences.Propositional {A = A} public
diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda
index 45b7a46a1d..33db54d0ed 100644
--- a/src/Algebra/Morphism.agda
+++ b/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
diff --git a/src/Algebra/Morphism/Definitions.agda b/src/Algebra/Morphism/Definitions.agda
index bf83e51e31..38c7b73d40 100644
--- a/src/Algebra/Morphism/Definitions.agda
+++ b/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."
-#-}
diff --git a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda b/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
index 4c33c7b337..c5b0219575 100644
--- a/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
+++ b/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.-_
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index 769c20ce06..7e0bdd29e5 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/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."
-#-}
diff --git a/src/Data/Integer.agda b/src/Data/Integer.agda
index 66c8100242..187084c425 100644
--- a/src/Data/Integer.agda
+++ b/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
 
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index a36a07f3b1..594a8f9b8a 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/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
diff --git a/src/Data/List/Solver.agda b/src/Data/List/Solver.agda
deleted file mode 100644
index 8b17b3ef9e..0000000000
--- a/src/Data/List/Solver.agda
+++ /dev/null
@@ -1,27 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- This module is DEPRECATED.
-------------------------------------------------------------------------
-
-{-# OPTIONS --cubical-compatible --safe #-}
-
--- Disabled to prevent warnings from deprecated monoid solver
-{-# OPTIONS --warn=noUserWarning #-}
-
-module Data.List.Solver where
-
-{-# WARNING_ON_IMPORT
-"Data.List.Solver was deprecated in v1.3.
-Use the new reflective Tactic.MonoidSolver instead."
-#-}
-
-import Algebra.Solver.Monoid as Solver
-open import Data.List.Properties using (++-monoid)
-
-------------------------------------------------------------------------
--- A module for automatically solving propositional equivalences
--- containing _++_
-
-module ++-Solver {a} {A : Set a} =
-  Solver (++-monoid A) renaming (id to nil)
diff --git a/src/Data/Nat.agda b/src/Data/Nat.agda
index 8811565c11..1de39f5cd8 100644
--- a/src/Data/Nat.agda
+++ b/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`
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b09b46db7d..7ee567cab2 100644
--- a/src/Data/Nat/Properties.agda
+++ b/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
diff --git a/src/Data/Rational.agda b/src/Data/Rational.agda
index 2345466dcb..b49fc451cf 100644
--- a/src/Data/Rational.agda
+++ b/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 ℤ
diff --git a/src/Induction/WellFounded.agda b/src/Induction/WellFounded.agda
index 1dac16c059..7e6c54f4b7 100644
--- a/src/Induction/WellFounded.agda
+++ b/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
diff --git a/src/Reflection.agda b/src/Reflection.agda
index fd3476cebb..c94a8a9c71 100644
--- a/src/Reflection.agda
+++ b/src/Reflection.agda
@@ -16,170 +16,3 @@ open import Reflection.TCM public
 open import Reflection.TCM.Syntax public
   using (_>>=_; _>>_)
 
-
-------------------------------------------------------------------------
--- DEPRECATED NAMES
-------------------------------------------------------------------------
--- Please use the new names as continuing support for the old names is
--- not guaranteed.
-
-import Reflection.AST.Abstraction as Abstraction
-import Reflection.AST.Argument as Argument
-import Reflection.AST.Definition as Definition
-import Reflection.AST.Meta as Meta
-import Reflection.AST.Name as Name
-import Reflection.AST.Literal as Literal
-import Reflection.AST.Pattern as Pattern
-import Reflection.AST.Term as Term
-import Reflection.AST.Argument.Modality as Modality
-import Reflection.AST.Argument.Quantity as Quantity
-import Reflection.AST.Argument.Relevance as Relevance
-import Reflection.AST.Argument.Visibility as Visibility
-import Reflection.AST.Argument.Information as Information
-
--- Version 1.3
-
-Arg-info = Information.ArgInfo
-{-# WARNING_ON_USAGE Arg-info
-"Warning: Arg-info was deprecated in v1.3.
-Please use Reflection.AST.Argument.Information's ArgInfo instead."
-#-}
-
-infix 4 _≟-Lit_ _≟-Name_ _≟-Meta_ _≟-Visibility_ _≟-Relevance_ _≟-Arg-info_
-        _≟-Pattern_ _≟-ArgPatterns_
-
-_≟-Lit_ = Literal._≟_
-{-# WARNING_ON_USAGE _≟-Lit_
-"Warning: _≟-Lit_ was deprecated in v1.3.
-Please use Reflection.AST.Literal's _≟_ instead."
-#-}
-
-_≟-Name_ = Name._≟_
-{-# WARNING_ON_USAGE _≟-Name_
-"Warning: _≟-Name_ was deprecated in v1.3.
-Please use Reflection.AST.Name's _≟_ instead."
-#-}
-
-_≟-Meta_ = Meta._≟_
-{-# WARNING_ON_USAGE _≟-Meta_
-"Warning: _≟-Meta_ was deprecated in v1.3.
-Please use Reflection.AST.Meta's _≟_ instead."
-#-}
-
-_≟-Visibility_ = Visibility._≟_
-{-# WARNING_ON_USAGE _≟-Visibility_
-"Warning: _≟-Visibility_ was deprecated in v1.3.
-Please use Reflection.AST.Argument.Visibility's _≟_ instead."
-#-}
-
-_≟-Relevance_ = Relevance._≟_
-{-# WARNING_ON_USAGE _≟-Relevance_
-"Warning: _≟-Relevance_ was deprecated in v1.3.
-Please use Reflection.AST.Argument.Relevance's _≟_ instead."
-#-}
-
-_≟-Arg-info_ = Information._≟_
-{-# WARNING_ON_USAGE _≟-Arg-info_
-"Warning: _≟-Arg-info_ was deprecated in v1.3.
-Please use Reflection.AST.Argument.Information's _≟_ instead."
-#-}
-
-_≟-Pattern_ = Pattern._≟_
-{-# WARNING_ON_USAGE _≟-Pattern_
-"Warning: _≟-Pattern_ was deprecated in v1.3.
-Please use Reflection.AST.Pattern's _≟_ instead."
-#-}
-
-_≟-ArgPatterns_ = Pattern._≟s_
-{-# WARNING_ON_USAGE _≟-ArgPatterns_
-"Warning: _≟-ArgPatterns_ was deprecated in v1.3.
-Please use Reflection.AST.Pattern's _≟s_ instead."
-#-}
-
-map-Abs = Abstraction.map
-{-# WARNING_ON_USAGE map-Abs
-"Warning: map-Abs was deprecated in v1.3.
-Please use Reflection.AST.Abstraction's map instead."
-#-}
-
-map-Arg = Argument.map
-{-# WARNING_ON_USAGE map-Arg
-"Warning: map-Arg was deprecated in v1.3.
-Please use Reflection.AST.Argument's map instead."
-#-}
-
-map-Args = Argument.map-Args
-{-# WARNING_ON_USAGE map-Args
-"Warning: map-Args was deprecated in v1.3.
-Please use Reflection.AST.Argument's map-Args instead."
-#-}
-
-visibility = Information.visibility
-{-# WARNING_ON_USAGE visibility
-"Warning: visibility was deprecated in v1.3.
-Please use Reflection.AST.Argument.Information's visibility instead."
-#-}
-
-relevance = Modality.relevance
-{-# WARNING_ON_USAGE relevance
-"Warning: relevance was deprecated in v1.3.
-Please use Reflection.AST.Argument.Modality's relevance instead."
-#-}
-
-infix 4 _≟-AbsTerm_ _≟-AbsType_ _≟-ArgTerm_ _≟-ArgType_ _≟-Args_
-        _≟-Clause_ _≟-Clauses_ _≟_
-        _≟-Sort_
-
-_≟-AbsTerm_ = Term._≟-AbsTerm_
-{-# WARNING_ON_USAGE _≟-AbsTerm_
-"Warning: _≟-AbsTerm_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-AbsTerm_ instead."
-#-}
-
-_≟-AbsType_ = Term._≟-AbsType_
-{-# WARNING_ON_USAGE _≟-AbsType_
-"Warning: _≟-AbsType_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-AbsType_ instead."
-#-}
-
-_≟-ArgTerm_ = Term._≟-ArgTerm_
-{-# WARNING_ON_USAGE _≟-ArgTerm_
-"Warning: _≟-ArgTerm_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-ArgTerm_ instead."
-#-}
-
-_≟-ArgType_ = Term._≟-ArgType_
-{-# WARNING_ON_USAGE _≟-ArgType_
-"Warning: _≟-ArgType_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-ArgType_ instead."
-#-}
-
-_≟-Args_    = Term._≟-Args_
-{-# WARNING_ON_USAGE _≟-Args_
-"Warning: _≟-Args_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-Args_ instead."
-#-}
-
-_≟-Clause_  = Term._≟-Clause_
-{-# WARNING_ON_USAGE _≟-Clause_
-"Warning: _≟-Clause_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-Clause_ instead."
-#-}
-
-_≟-Clauses_ = Term._≟-Clauses_
-{-# WARNING_ON_USAGE _≟-Clauses_
-"Warning: _≟-Clauses_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-Clauses_ instead."
-#-}
-
-_≟_         = Term._≟_
-{-# WARNING_ON_USAGE _≟_
-"Warning: _≟_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟_ instead."
-#-}
-
-_≟-Sort_    = Term._≟-Sort_
-{-# WARNING_ON_USAGE _≟-Sort_
-"Warning: _≟-Sort_ was deprecated in v1.3.
-Please use Reflection.AST.Term's _≟-Sort_ instead."
-#-}
diff --git a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda
index 5ed5b8f4ff..f3f5443dd1 100644
--- a/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda
+++ b/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda
@@ -94,7 +94,7 @@ record _-Raw-AlmostCommutative⟶_
     module T = AlmostCommutativeRing To
   open Morphism.Definitions F.Carrier T.Carrier T._≈_
   field
-    ⟦_⟧    : Morphism
+    ⟦_⟧    : F.Carrier → T.Carrier
     +-homo : Homomorphic₂ ⟦_⟧ F._+_ T._+_
     *-homo : Homomorphic₂ ⟦_⟧ F._*_ T._*_
     -‿homo : Homomorphic₁ ⟦_⟧ (F.-_)  (T.-_)