∀ (m : Type u_2 → Type u_1) [inst : Monad m],
  (∀ {α β : Type u_2} (f : α → β) (x : m α),
      (do
          let a ← x
          pure (f a)) =
        f <$> x) →
    (∀ {α β : Type u_2} (f : m (α → β)) (x : m α),
        (do
            let x_1 ← f
            x_1 <$> x) =
          f <*> x) →
      (∀ {α β : Type u_2} (x : α) (f : α → m β), pure x >>= f = f x) →
        (∀ {α β γ : Type u_2} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
          ∀ {α β γ : Type u_2} (x : m α) (g : m (α → β)) (h : m (β → γ)),
            h <*> (g <*> x) = Function.comp <$> h <*> g <*> x