From d7fb0a54d661f82282cb7175ba3b133aa74024ed Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Wed, 15 Oct 2025 21:15:41 -0500 Subject: Improve terminology in comment --- Functor/Instance/Decorate.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3