A monad(ic) failure

Stream: new members

[Jeremy Tan]

The following code fails at the second line of the Monad definition:

import Mathlib.CategoryTheory.Functor.Category
import Mathlib.CategoryTheory.Functor.FullyFaithful
import Mathlib.CategoryTheory.Functor.ReflectsIso

universe v₁ u₁

variable (C : Type u₁) [Category.{v₁} C]

structure Monad extends C ⥤ C where
  η' : 𝟭 C ⟶ to_functor -- this is OK
  μ' : to_functor ⋙ to_functor ⟶ to_functor -- how can this line fail?
  assoc' : ∀ X, to_functor.map (NatTrans.app μ' X) ≫ μ'.app _ = μ'.app _ ≫ μ'.app _ := by aesop_cat
  left_unit' : ∀ X : C, η'.app (to_functor.obj X) ≫ μ'.app _ = 𝟙 _ := by aesop_cat
  right_unit' : ∀ X : C, to_functor.map (η'.app X) ≫ μ'.app _ = 𝟙 _ := by aesop_cat

I can't seem to get the second line to work; how can I do so?

[Jeremy Tan]

This is the error

typeclass instance problem is stuck, it is often due to metavariables
  Category ?m.654

[Jeremy Tan]

Is this the best solution?

structure Monad extends C ⥤ C where
  to_functor : C ⥤ C
  η' : 𝟭 _ ⟶ to_functor
  μ' : to_functor ⋙ to_functor ⟶ to_functor
  assoc' : ∀ X, to_functor.map (NatTrans.app μ' X) ≫ μ'.app _ = μ'.app _ ≫ μ'.app _ := by aesop_cat
  left_unit' : ∀ X : C, η'.app (to_functor.obj X) ≫ μ'.app _ = 𝟙 _ := by aesop_cat
  right_unit' : ∀ X : C, to_functor.map (η'.app X) ≫ μ'.app _ = 𝟙 _ := by aesop_cat

[Jeremy Tan]

nvm, found an ideal fix

structure Monad extends C ⥤ C where
  η' : 𝟭 _ ⟶ toFunctor
  μ' : toFunctor ⋙ toFunctor ⟶ toFunctor
  assoc' : ∀ X, toFunctor.map (NatTrans.app μ' X) ≫ μ'.app _ = μ'.app _ ≫ μ'.app _ := by aesop_cat
  left_unit' : ∀ X : C, η'.app (toFunctor.obj X) ≫ μ'.app _ = 𝟙 _ := by aesop_cat
  right_unit' : ∀ X : C, toFunctor.map (η'.app X) ≫ μ'.app _ = 𝟙 _ := by aesop_cat