diff options
| -rw-r--r-- | Functor/Instance/Decorate.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Functor/Instance/Decorate.agda b/Functor/Instance/Decorate.agda index e87f20c..30cec87 100644 --- a/Functor/Instance/Decorate.agda +++ b/Functor/Instance/Decorate.agda @@ -40,7 +40,7 @@ module DecoratedCospans = Category DecoratedCospans module mc𝒞 = CocartesianMonoidal 𝒞.U 𝒞.cocartesian -- For every cospan there exists a free decorated cospan --- i.e. the original cospan with the empty decoration +-- i.e. the original cospan with the discrete decoration private variable |