We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 9aaa7bc commit 462899fCopy full SHA for 462899f
src/Categories/Bicategory/Monad/Properties.agda
@@ -14,8 +14,6 @@ import Categories.Morphism.Reasoning as MR
14
--------------------------------------------------------------------------------
15
-- Bicategorical Monads in Cat are the same as the more elementary
16
-- definition of Monads.
17
---
18
--- NOTE:
19
20
CatMonad⇒Monad : ∀ {o ℓ e} → (T : BicatMonad.Monad (Cats o ℓ e)) → ElemMonad.Monad (BicatMonad.Monad.C T)
21
CatMonad⇒Monad T = record
0 commit comments