fix: missed renamed ∘-is-monic

the1lab · Jul 17, 2023 · e87f0e4 · e87f0e4
1 parent 1f591f0
commit e87f0e4
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
@@ -349,7 +349,7 @@ Sub-products {y} pb a b = prod where
   prod : Product (Sub y) a b
   prod .Product.apex .domain = it .apex
   prod .Product.apex .map = a .map ∘ it .p₁
-  prod .Product.apex .monic = ∘-is-monic
+  prod .Product.apex .monic = monic-∘
     (is-monic→pullback-is-monic (b .monic) (rotate-pullback (it .has-is-pb)))
     (a .monic)