aboutsummaryrefslogtreecommitdiff
path: root/Category/Instance
diff options
context:
space:
mode:
Diffstat (limited to 'Category/Instance')
-rw-r--r--Category/Instance/Properties/FinitelyCocompletes.agda4
1 files changed, 3 insertions, 1 deletions
diff --git a/Category/Instance/Properties/FinitelyCocompletes.agda b/Category/Instance/Properties/FinitelyCocompletes.agda
index 9f848f4..dedfa16 100644
--- a/Category/Instance/Properties/FinitelyCocompletes.agda
+++ b/Category/Instance/Properties/FinitelyCocompletes.agda
@@ -36,7 +36,9 @@ module _ (π’ž : FinitelyCocompleteCategory o β„“ e) where
openΒ π’ž using ([_,_]; +-unique; i₁; iβ‚‚; _∘_; _+_; module Equiv; _β‡’_; _+₁_; -+-)
open Equiv
- module -+- = Functor -+-
+
+ private
+ module -+- = Functor -+-
+-resp-βŠ₯
: {(A , B) : π’žΓ—π’ž.Obj}