aboutsummaryrefslogtreecommitdiff
path: root/Preorder/Monoidal.agda
diff options
context:
space:
mode:
Diffstat (limited to 'Preorder/Monoidal.agda')
-rw-r--r--Preorder/Monoidal.agda2
1 files changed, 1 insertions, 1 deletions
diff --git a/Preorder/Monoidal.agda b/Preorder/Monoidal.agda
index 705c359..02c6d88 100644
--- a/Preorder/Monoidal.agda
+++ b/Preorder/Monoidal.agda
@@ -83,7 +83,7 @@ record MonoidalMonotone
field
F : PreorderHomomorphism P.U Q.U
- open PreorderHomomorphism F
+ open PreorderHomomorphism F public
field
ε : Q.unit Q.≲ ⟦ P.unit ⟧