{-# OPTIONS --without-K #-}
module Class.Traversable.Core where
 
open import Class.Prelude
open import Class.Core
open import Class.Functor.Core
open import Class.Monad
 
record Traversable (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
  field sequence : ⦃ Monad M ⦄ → F (M A) → M (F A)
 
  traverse : ⦃ Monad M ⦄ → (A → M B) → F A → M (F B)
  traverse f = sequence ∘ fmap f
open Traversable ⦃...⦄ public