diff --git a/src/1Lab/Membership.agda b/src/1Lab/Membership.agda
index 7fedf95f5..273c92808 100644
--- a/src/1Lab/Membership.agda
+++ b/src/1Lab/Membership.agda
@@ -21,7 +21,7 @@ record Membership {ℓ ℓe} (A : Type ℓe) (ℙA : Type ℓ) ℓm : Type (ℓ
   infix 30 _∈_
 
 open Membership ⦃ ... ⦄ using (_∈_) public
-{-# DISPLAY Membership._∈_ i a b = a ∈ b #-}
+{-# DISPLAY Membership._∈_ _ a b = a ∈ b #-}
 
 -- The prototypical instance is given by functions into a universe:
 
@@ -65,7 +65,7 @@ record Inclusion {ℓ} (ℙA : Type ℓ) ℓi : Type (ℓ ⊔ lsuc (ℓi)) where
   infix 30 _⊆_
 
 open Inclusion ⦃ ... ⦄ using (_⊆_) public
-{-# DISPLAY Inclusion._⊆_ i a b = a ⊆ b #-}
+{-# DISPLAY Inclusion._⊆_ _ a b = a ⊆ b #-}
 
 instance
   Inclusion-default
diff --git a/src/1Lab/Underlying.agda b/src/1Lab/Underlying.agda
index d6a4fc8eb..d963f9d38 100644
--- a/src/1Lab/Underlying.agda
+++ b/src/1Lab/Underlying.agda
@@ -23,7 +23,7 @@ open Underlying using (ℓ-underlying)
 -- Workaround for Agda bug https://github.com/agda/agda/issues/6588 —
 -- the principal (instance) argument is reified as visible, so we can
 -- drop it using a display form.
-{-# DISPLAY Underlying.⌞_⌟ f x = ⌞ x ⌟ #-}
+{-# DISPLAY Underlying.⌞_⌟ _ x = ⌞ x ⌟ #-}
 
 instance
 -- For universes, we use the standard notion of "underlying type".
@@ -79,7 +79,7 @@ record Funlike {ℓ ℓ' ℓ''} (A : Type ℓ) (arg : Type ℓ') (out : arg →
   infixl 999 _#_
 
 open Funlike ⦃ ... ⦄ using (_#_) public
-{-# DISPLAY Funlike._#_ p f x = f # x #-}
+{-# DISPLAY Funlike._#_ _ f x = f # x #-}
 
 -- Sections of the _#_ operator tend to be badly-behaved since they
 -- introduce an argument x : ⌞ ?0 ⌟ whose Underlying instance meta
diff --git a/src/Data/Rational/Base.lagda.md b/src/Data/Rational/Base.lagda.md
index f2e953eb0..317167932 100644
--- a/src/Data/Rational/Base.lagda.md
+++ b/src/Data/Rational/Base.lagda.md
@@ -207,7 +207,7 @@ _/_ x y ⦃ p ⦄ = toℚ (x / y [ p ])
 
 infix 11 _/_
 
-{-# DISPLAY ℚ.inc (Coeq.inc (_/_[_] x y p)) = x / y #-}
+{-# DISPLAY ℚ.inc (Coeq.inc (_/_[_] x y _)) = x / y #-}
 {-# DISPLAY _/_ x (Int.pos 1) = x #-}
 
 _/1 : Int → ℚ
diff --git a/src/Homotopy/Space/Delooping.lagda.md b/src/Homotopy/Space/Delooping.lagda.md
index fc218d3e1..ae6b1c802 100644
--- a/src/Homotopy/Space/Delooping.lagda.md
+++ b/src/Homotopy/Space/Delooping.lagda.md
@@ -432,7 +432,7 @@ again. That finishes the construction:
           (λ i j → go (α i j)) (λ i j → go (β i j))
           (squash x y p q α β) i j k
 
-  {-# DISPLAY windingⁱ.go x p = winding p #-}
+  {-# DISPLAY windingⁱ.go _ p = winding p #-}
 ```
 -->
 
diff --git a/src/Meta/Brackets.lagda.md b/src/Meta/Brackets.lagda.md
index c12e87fb2..c9741b48c 100644
--- a/src/Meta/Brackets.lagda.md
+++ b/src/Meta/Brackets.lagda.md
@@ -25,5 +25,5 @@ record ⟦⟧-notation {ℓ} (A : Type ℓ) : Typeω where
     ⟦_⟧ : A → Sem
 
 open ⟦⟧-notation ⦃...⦄ using (⟦_⟧) public
-{-# DISPLAY ⟦⟧-notation.⟦_⟧ f x = ⟦ x ⟧ #-}
+{-# DISPLAY ⟦⟧-notation.⟦_⟧ _ x = ⟦ x ⟧ #-}
 ```
diff --git a/support/nix/dep/Agda/github.json b/support/nix/dep/Agda/github.json
index 9e12fabc2..f45eb3b2c 100644
--- a/support/nix/dep/Agda/github.json
+++ b/support/nix/dep/Agda/github.json
@@ -3,6 +3,6 @@
   "repo": "agda",
   "branch": "master",
   "private": false,
-  "rev": "11e54c0e0229996c22ed7b53a50694933de84b09",
-  "sha256": "12avpyxdlh7w7p9gsv5p4499c01qk3k1mklwfp8shljmb8z8cwd4"
+  "rev": "14099b47e5cb2afb31cdbe511615501147e4b23a",
+  "sha256": "009k829zqyp4yg4xz8a6syhibpgnwprl605icrs4dgxppi6cw5z2"
 }