More random DaoFP experiments

Changes

1 changed files (+7/-1)

• Dao.lean
  • @@ -1,6 +1,8 @@
    + -- https://github.com/BartoszMilewski/DaoFP + -- import Mathlib - universe u + -- universe u def absurd' {C : Sort u} : Empty → C := Empty.rec #check absurd'
  • @@ -76,3 +78,7 @@ def yoneda' {α} (m : Type u → Type v) [Functor m] (y : m α) : {β : Type u}
    def ap [Monad m] (fs : m (α → β)) (as : m α) : m β := do -- fs >>= (λ f ↦ as >>= λ a ↦ pure (f a)) return (← fs) (← as) + + class Monad' (m : Type → Type) where + fish : (β → m γ) → (α → m β) → (α → m γ) + join : (a : m (m α)) → m α := fish id id