diff --git a/Cubical/Categories/Bifunctor/Base.agda b/Cubical/Categories/Bifunctor/Base.agda
index d5015c7d..f4b5f9e2 100644
--- a/Cubical/Categories/Bifunctor/Base.agda
+++ b/Cubical/Categories/Bifunctor/Base.agda
@@ -77,6 +77,9 @@ infix 30 _⟪_⟫l
 infix 30 _⟪_⟫r
 -- same infix level as on objects since these will
 -- never be used in the same context
+infix 30 _⟪_,_⟫lr
+-- same infix level as on objects since these will
+-- never be used in the same context
 _⟪_⟫l : (F : Bifunctor C D E)
      → ∀ {c c' d}
      → C [ c , c' ]