fix: flip monic-∘ args

the1lab · Jul 17, 2023 · 8348e41 · 8348e41
1 parent e87f0e4
commit 8348e41
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 _