diff --git a/src/Cat/Displayed/Instances/Subobjects.lagda.md b/src/Cat/Displayed/Instances/Subobjects.lagda.md
index d3dbc6f31..15dc8eb30 100644
--- a/src/Cat/Displayed/Instances/Subobjects.lagda.md
+++ b/src/Cat/Displayed/Instances/Subobjects.lagda.md
@@ -350,8 +350,8 @@ Sub-products {y} pb a b = prod where
   prod .Product.apex .domain = it .apex
   prod .Product.apex .map = a .map ∘ it .p₁
   prod .Product.apex .monic = monic-∘
-    (is-monic→pullback-is-monic (b .monic) (rotate-pullback (it .has-is-pb)))
     (a .monic)
+    (is-monic→pullback-is-monic (b .monic) (rotate-pullback (it .has-is-pb)))
 
   prod .Product.π₁ .map = it .p₁
   prod .Product.π₁ .sq  = idl _