forgot to add syntax level

maxsnew · May 25, 2024 · b368f01 · b368f01
1 parent 20830c0
commit b368f01
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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' ]