Wild Monads !!

Cubical/WildCat/Functor.agda

@@ -55,6 +55,10 @@ open WildNatTrans
 open WildNatIso
 open wildIsIso
 
+idWildNatTrans : {C : WildCat ℓC ℓC'} {D : WildCat ℓD ℓD'} {F : WildFunctor C D} → WildNatTrans _ _ F F
+idWildNatTrans {D = D} .N-ob x = D .id
+idWildNatTrans {D = D} .N-hom f = D .⋆IdR _ ∙ sym (D .⋆IdL _)
+
 module _
   {C : WildCat ℓC ℓC'} {D : WildCat ℓD ℓD'}
   (F G H : WildFunctor C D) where

Cubical/WildCat/Monad.agda

@@ -0,0 +1,30 @@
+module Cubical.WildCat.Monad where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.WildCat.Base
+open import Cubical.WildCat.Functor
+
+private variable
+  ℓ ℓ' : Level
+
+module _ {C : WildCat ℓ ℓ'} (M : WildFunctor C C) where
+  open WildCat C
+  open WildFunctor
+  open WildNatTrans
+
+  IsPointed : Type (ℓ-max ℓ ℓ')
+  IsPointed = WildNatTrans C C (idWildFunctor C) M
+
+  record IsMonad : Type (ℓ-max ℓ ℓ') where
+    field
+      η : IsPointed
+      μ : WildNatTrans _ _ (comp-WildFunctor M M) M
+      idl-μ : {X : ob} → μ .N-ob X ∘ η .N-ob (M .F-ob X) ≡ id
+      idr-μ : {X : ob} → μ .N-ob X ∘ M .F-hom (η .N-ob X) ≡ id
+      assoc-μ : {X : ob} → μ .N-ob X ∘ M .F-hom (μ .N-ob X) ≡ μ .N-ob X ∘ μ .N-ob (M .F-ob X)
+
+    bind : {X Y : ob} → Hom[ X , M .F-ob Y ] → Hom[ M .F-ob X , M .F-ob Y ]
+    bind f = μ .N-ob _ ∘ M .F-hom f
+
+WildMonad : WildCat ℓ ℓ' → Type (ℓ-max ℓ ℓ')
+WildMonad C = Σ[ M ∈ WildFunctor C C ] IsMonad M