diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 15:53:23 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-04 15:53:23 -0600 |
| commit | 3d7c5574124d3384ff942489feaa093618c309b9 (patch) | |
| tree | d39033498bb1b84ff2f516a29a78bd1dd1ee151a /Preorder/Monoidal.agda | |
| parent | a2225e97e0bb4de0d9ed9516e1a5515edb140e48 (diff) | |
Add category of monoidal preorders
Diffstat (limited to 'Preorder/Monoidal.agda')
| -rw-r--r-- | Preorder/Monoidal.agda | 2 |
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 ⟧ |
