diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-15 21:15:41 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-10-15 21:15:41 -0500 |
| commit | d7fb0a54d661f82282cb7175ba3b133aa74024ed (patch) | |
| tree | a99999ae84c4853c847d38d439e30e4701347909 | |
| parent | fe6496cc72b9b6371937148b7822f2e847fc1b9a (diff) | |
Improve terminology in comment
| -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 |