More random DaoFP stuff

Changes

1 changed files (+5/-0)

• Dao.lean
  • @@ -71,3 +71,8 @@ def yoneda' {α} (m : Type u → Type v) [Functor m] (y : m α) : {β : Type u}
    -- else by -- simp [map_to_T, h] -- exact x + + + def ap [Monad m] (fs : m (α → β)) (as : m α) : m β := do + -- fs >>= (λ f ↦ as >>= λ a ↦ pure (f a)) + return (← fs) (← as)