diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 10:12:13 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2026-01-07 10:12:13 -0600 |
| commit | 8ec259bb32b4339b27560f5ea13afa81b9b8febc (patch) | |
| tree | f8b860c07c3da42f7ad078413700c347adbfd9d5 /Functor/Free/Instance/Preorder.agda | |
| parent | aecb9a5862a9082909c902307974e7ca85463bb9 (diff) | |
Differentiate lax and strong monoidal monotones
Diffstat (limited to 'Functor/Free/Instance/Preorder.agda')
| -rw-r--r-- | Functor/Free/Instance/Preorder.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Functor/Free/Instance/Preorder.agda b/Functor/Free/Instance/Preorder.agda index 27be24e..18583e9 100644 --- a/Functor/Free/Instance/Preorder.agda +++ b/Functor/Free/Instance/Preorder.agda @@ -7,7 +7,7 @@ open import Categories.Category.Instance.Cats using (Cats) open import Function using (flip) open import Categories.Functor using (Functor; _∘F_) open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism) -open import Category.Instance.Preorders.Primitive using (Preorders) +open import Category.Instance.Preorder.Primitive.Preorders using (Preorders) open import Level using (Level; _⊔_; suc) open import Preorder.Primitive using (Preorder; module Isomorphism) open import Preorder.Primitive.MonotoneMap using (MonotoneMap; _≃_; module ≃) |