{-# OPTIONS --cubical-compatible #-}
module Class.Traversable.Core where
 
open import Class.Prelude
open import Class.Core
open import Class.Functor.Core
open import Class.Applicative.Core
open import Class.Monad.Core
 
record TraversableA (F : Type↑) ⦃ _ : Functor F ⦄ : Typeω where
  field sequenceA : ⦃ Applicative M ⦄ → F (M A) → M (F A)
 
  traverseA : ⦃ Applicative M ⦄ → (A → M B) → F A → M (F B)
  traverseA f = sequenceA ∘ fmap f
open TraversableA ⦃...⦄ public
 
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