diff --git a/src/Mugen/Cat/HierarchyTheory.agda b/src/Mugen/Cat/HierarchyTheory.agda
index 7b0aa96..0c424c3 100644
--- a/src/Mugen/Cat/HierarchyTheory.agda
+++ b/src/Mugen/Cat/HierarchyTheory.agda
@@ -36,7 +36,7 @@ Hierarchy-theory o r = Monad (Strict-orders o r)
   open Displacement-algebra 𝒟
 
   M : Functor (Strict-orders o o) (Strict-orders o o)
-  M .F₀ L = L ⋉ strict-order [ ε ]
+  M .F₀ L = L ⋉[ ε ] strict-order
   M .F₁ f .hom (l , d) = (f .hom l) , d
   M .F₁ f .strict-mono x<y =
     ⋉-elim (λ a1≡a2 b1<b2 → biased (ap (f .hom) a1≡a2) b1<b2)
diff --git a/src/Mugen/Order/LeftInvariantRightCentered.agda b/src/Mugen/Order/LeftInvariantRightCentered.agda
index 1c73e52..6dd3b49 100644
--- a/src/Mugen/Order/LeftInvariantRightCentered.agda
+++ b/src/Mugen/Order/LeftInvariantRightCentered.agda
@@ -75,8 +75,8 @@ module _ {o r} {A B : Strict-order o r} {b : ⌞ B ⌟} where
     centred (A.<-thin a1<a2 a1<a2′ i) (B.≤-thin ≤b ≤b′ i) (B.≤-thin b≤ b≤′ i)
 
 
-_⋉_[_] : ∀ {o} → (A B : Strict-order o o) → ⌞ B ⌟ → Strict-order o o
-A ⋉ B [ b ] = to-strict-order order where
+LeftInvariantRightCentered : ∀ {o} → (A B : Strict-order o o) → ⌞ B ⌟ → Strict-order o o
+LeftInvariantRightCentered A B b = to-strict-order order where
   module A = Strict-order A
   module B = Strict-order B
 
@@ -86,3 +86,5 @@ A ⋉ B [ b ] = to-strict-order order where
   order .make-strict-order.<-trans {x} {y} {z} = ⋉-trans x y z
   order .make-strict-order.<-thin = ⋉-thin _ _
   order .make-strict-order.has-is-set = ×-is-hlevel 2 A.has-is-set B.has-is-set
+
+syntax LeftInvariantRightCentered A B b = A ⋉[ b ] B