diff --git a/src/Cat/Displayed/Bifibration.lagda.md b/src/Cat/Displayed/Bifibration.lagda.md
index b8c6200b3..c220095ed 100644
--- a/src/Cat/Displayed/Bifibration.lagda.md
+++ b/src/Cat/Displayed/Bifibration.lagda.md
@@ -121,7 +121,7 @@ module _ (fib : Cartesian-fibration) where
 With some repackaging, we can see that this yields a bifibration.
 
 ```agda
-  left-adjoint-reindexing→bifibration
+  left-adjoint-base-change→bifibration
     : (L : ∀ {x y} → (f : Hom x y) → Functor (Fibre ℰ x) (Fibre ℰ y))
     → (∀ {x y} → (f : Hom x y) → (L f ⊣ base-change f))
     → is-bifibration