+Commutative monads #402
+Commutative monads #402
Conversation
|
Sorry for the silence, it's been a crazy term for me - why did you close this PR? |
| open import Categories.Monad | ||
|
|
||
| private | ||
| variable | ||
| o ℓ e : Level | ||
|
|
||
| record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where | ||
| record Strength {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where |
There was a problem hiding this comment.
Isn't it the case that there are different concepts of Strength depending on whether the underlying category is Symmetric or not? So there should be two notions of Strength rather than requiring Symmetric V?
There was a problem hiding this comment.
Yes, that was too crude. We can have left-strong monads over non-symmetric V.
| open M using (F) | ||
| open Functor F | ||
|
|
||
| record Commutative : Set (o ⊔ ℓ ⊔ e) where |
There was a problem hiding this comment.
I wonder if Commutative should be a simple property rather than a record ? There are certainly times where a one-field record is much nicer (both to help Agda with inference, and to get a nice projector name), I'm not sure here?
There was a problem hiding this comment.
I just copycatted /src/Categories/Monad/Idempotent.agda
There was a problem hiding this comment.
Which was the right thing to do. I didn't think of asking the question about that one - such are the vagaries of code reviews done by humans, you don't catch everything every time.
I thought, if I delete it, it counts as withdrawn. Should I have done something different? I did not see other options. I wanted to add this definition initially, but Leon (@Reijix) already implemented it in his fork (together with many other things). He kind of convinced me that his implementation is better. |
|
If you wanted to withdraw it from consideration, then closing it is the right thing to do - I just expected a message to go along, saying why you were closing it. So is Leon (@Reijix ) going to be submitting some PRs? |
now he must:-) since he protested about my PR. |
I wanted to hold it back until I can figure out the missing proof, but it seems that I wont be able to do it any time soon, so I've created the PR now (#404) in hope that someone else is able to. |
strengthen' : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗))SwapFG≅FGSwapto src/Categories/Category/Product/Properties.agda